Grace/Cumulus/Algebra/Restriction.g17

Open in Workbench Download source

Imports

Ring.Core · Set.Function

Declarations

Source

1-- Restrict operation graphs to closed subcarriers.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Restriction8import Ring.Core9import Set.Function1011predicate ClosedBinary (S op : Set) := ∀ x ∈ S, ∀ y ∈ S, op(x, y) ∈ S12predicate ClosedUnary (S op : Set) := ∀ x ∈ S, op(x) ∈ S1314theorem ClosedBinary.mem (S op x y : Set)15  requires closed : ClosedBinary(S, op)16  requires hx : x ∈ S17  requires hy : y ∈ S18  shows op(x, y) ∈ S19proof20  exact closed with x, hx, y, hy2122theorem ClosedUnary.mem (S op x : Set)23  requires closed : ClosedUnary(S, op)24  requires hx : x ∈ S25  shows op(x) ∈ S26proof27  exact closed with x, hx2829theorem restrictBinary.function (A S op : Set)30  requires function : IsMagma(A, op)31  requires subset : S ⊆ A32  requires closed : ClosedBinary(S, op)33  shows restrict(op, S × S) : S × S → S34proof35  have bounded := product.monotone with subset, subset36  have values : ∀ p ∈ S × S, op(p) ∈ S37    intros p hp38    obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with hp39    have output := ClosedBinary.mem with hx, hy40    unfold call2 at output41    rwa shape42  exact restrict.function at op, A × A, A, S × S, S with *4344theorem restrictBinary.value (A S op x y : Set)45  requires function : IsMagma(A, op)46  requires subset : S ⊆ A47  requires closed : ClosedBinary(S, op)48  requires hx : x ∈ S49  requires hy : y ∈ S50  shows (restrict(op, S × S))(x, y) = op(x, y)51proof52  have bounded := product.monotone with subset, subset53  have values : ∀ p ∈ S × S, op(p) ∈ S54    intros p hp55    obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with hp56    have output := ClosedBinary.mem with hu, hv57    unfold call2 at output58    rwa shape59  have pair := product.pair at x, y, S, S with *60  unfold call261  exact restrict.apply at op, A × A, A, S × S, S, (x, y) with *6263-- Agreement of operation graphs does not require closure of the smaller carrier.64theorem restrictBinary.value_on_subset (A S op x y : Set)65  requires function : IsMagma(A, op)66  requires subset : S ⊆ A67  requires hx : x ∈ S68  requires hy : y ∈ S69  shows (restrict(op, S × S))(x, y) = op(x, y)70proof71  have bounded := product.monotone with subset, subset72  unfold IsMagma at function73  have values : ∀ p ∈ S × S, op(p) ∈ A74    intros p hp75    have member : p ∈ A × A by simp [Subset]76    exact FunctionBetween.apply_closed with function, member77  have pair := product.pair at x, y, S, S with *78  unfold call279  exact restrict.apply with *8081theorem restrictUnary.function (A S op : Set)82  requires function : op : A → A83  requires subset : S ⊆ A84  requires closed : ClosedUnary(S, op)85  shows restrict(op, S) : S → S86proof87  have values : ∀ x ∈ S, op(x) ∈ S88    intros x hx89    exact ClosedUnary.mem with *90  exact restrict.function with *9192theorem restrictUnary.value (A S op x : Set)93  requires function : op : A → A94  requires subset : S ⊆ A95  requires closed : ClosedUnary(S, op)96  requires hx : x ∈ S97  shows (restrict(op, S))(x) = op(x)98proof99  have values : ∀ y ∈ S, op(y) ∈ S100    intros y hy101    exact ClosedUnary.mem with hy102  exact restrict.apply with *103104theorem restrictBinary.associative (A S op : Set)105  requires function : IsMagma(A, op)106  requires subset : S ⊆ A107  requires closed : ClosedBinary(S, op)108  requires law : Associative(A, op)109  shows Associative(S, restrict(op, S × S))110proof111  intros x hx y hy z hz112  have included := subset113  have xIn := included with x, hx114  have yIn := included with y, hy115  have zIn := included with z, hz116  have closed0 := ClosedBinary.mem at S, op, x, y with *117  have value0 := restrictBinary.value at A, S, op, x, y with *118  have closed1 := ClosedBinary.mem at S, op, op(x, y), z with *119  have value1 := restrictBinary.value at A, S, op, op(x, y), z with *120  have closed2 := ClosedBinary.mem at S, op, y, z with *121  have value2 := restrictBinary.value at A, S, op, y, z with *122  have closed3 := ClosedBinary.mem at S, op, x, op(y, z) with *123  have value3 := restrictBinary.value at A, S, op, x, op(y, z) with *124  have original := law with x, xIn, y, yIn, z, zIn125  cc126127theorem restrictBinary.commutative (A S op : Set)128  requires function : IsMagma(A, op)129  requires subset : S ⊆ A130  requires closed : ClosedBinary(S, op)131  requires law : Commutative(A, op)132  shows Commutative(S, restrict(op, S × S))133proof134  intros x hx y hy135  have included := subset136  have xIn := included with x, hx137  have yIn := included with y, hy138  have closed0 := ClosedBinary.mem with hx, hy139  have value0 := restrictBinary.value with hx, hy140  have closed1 := ClosedBinary.mem with hy, hx141  have value1 := restrictBinary.value with hy, hx142  have original := law with x, xIn, y, yIn143  cc144145theorem restrictBinary.identity (A S op unit : Set)146  requires function : IsMagma(A, op)147  requires subset : S ⊆ A148  requires closed : ClosedBinary(S, op)149  requires law : Identity(A, op, unit)150  requires member : unit ∈ S151  shows Identity(S, restrict(op, S × S), unit)152proof153  unfold Identity154  refine ⟨member, ?_⟩155  intros x hx156  have included := subset157  have xIn := included with x, hx158  have original := law.right with x, xIn159  have left := restrictBinary.value at A, S, op, unit, x with *160  have right := restrictBinary.value at A, S, op, x, unit with *161  constructor162  . cc163  . cc164165theorem restrictUnary.inverse (A S add zero neg : Set)166  requires addition : IsMagma(A, add)167  requires negation : neg : A → A168  requires subset : S ⊆ A169  requires addClosed : ClosedBinary(S, add)170  requires negClosed : ClosedUnary(S, neg)171  requires law : Inverse(A, add, zero, neg)172  shows Inverse(S, restrict(add, S × S), zero, restrict(neg, S))173proof174  have function := restrictUnary.function with *175  unfold Inverse176  refine ⟨function, ?_⟩177  intros x hx178  have included := subset179  have xIn := included with x, hx180  have closed0 := ClosedUnary.mem with *181  have value0 := restrictUnary.value with hx182  have closed1 := ClosedBinary.mem at S, add, neg(x), x with *183  have value1 := restrictBinary.value at A, S, add, neg(x), x with *184  have closed2 := ClosedBinary.mem at S, add, x, neg(x) with *185  have value2 := restrictBinary.value at A, S, add, x, neg(x) with *186  have original := law.right with x, xIn187  constructor188  . cc189  . cc190191theorem restrictBinary.distributive (A S add mul : Set)192  requires addition : IsMagma(A, add)193  requires multiplication : IsMagma(A, mul)194  requires subset : S ⊆ A195  requires addClosed : ClosedBinary(S, add)196  requires mulClosed : ClosedBinary(S, mul)197  requires law : Distributive(A, add, mul)198  shows Distributive(S, restrict(add, S × S), restrict(mul, S × S))199proof200  intros x hx y hy z hz201  have included := subset202  have xIn := included with x, hx203  have yIn := included with y, hy204  have zIn := included with z, hz205  have closed0 := ClosedBinary.mem at S, add, y, z with *206  have value0 := restrictBinary.value at A, S, add, y, z with *207  have closed1 := ClosedBinary.mem at S, mul, x, call2(add, y, z) with *208  have value1 := restrictBinary.value at A, S, mul, x, call2(add, y, z) with *209  have closed2 := ClosedBinary.mem at S, mul, x, y with *210  have value2 := restrictBinary.value at A, S, mul, x, y with *211  have closed3 := ClosedBinary.mem at S, mul, x, z with *212  have value3 := restrictBinary.value at A, S, mul, x, z with *213  have closed4 := ClosedBinary.mem at S, add, call2(mul, x, y), call2(mul, x, z) with *214  have value4 := restrictBinary.value at A, S, add, call2(mul, x, y), call2(mul, x, z) with *215  have closed5 := ClosedBinary.mem at S, add, x, y with *216  have value5 := restrictBinary.value at A, S, add, x, y with *217  have closed6 := ClosedBinary.mem at S, mul, call2(add, x, y), z with *218  have value6 := restrictBinary.value at A, S, mul, call2(add, x, y), z with *219  have closed7 := ClosedBinary.mem at S, mul, y, z with *220  have value7 := restrictBinary.value at A, S, mul, y, z with *221  have closed8 := ClosedBinary.mem at S, add, call2(mul, x, z), call2(mul, y, z) with *222  have value8 := restrictBinary.value at A, S, add, call2(mul, x, z), call2(mul, y, z) with *223  have original := law with x, xIn, y, yIn, z, zIn224  constructor225  . cc226  . cc227