Grace/Cumulus/Nat/CyclicShift.g17
Imports
Mod · Order · Set.Function
Declarations
- rotation defgraph
- rotation.step theorem derivation
- rotation.wrap theorem derivation
- rotation.cancel theorem derivation
- rotation.injective theorem derivation
- rotation.surjective theorem derivation
- rotation.bijective theorem derivation
Source
1-- The cyclic shift on a natural number n: successor on its members, wrapping2-- n − 1 to 0, as a function graph on n; it is a bijection of n.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Nat.CyclicShift9import Mod10import Order11import Set.Function1213-- The cyclic shift l ↦ l + 1 on n, wrapping n − 1 to 0.14defgraph rotation (n : Set) (l ∈ n) : n := chooseNat(equalNat(succ(l), n), 0, succ(l))15requires nNat : Nat(n)16proof17 have lNat := natural.member at n with member18 have less := Less.of_membership with member19 have alternatives : succ(l) = n ∨ succ(l) ≠ n20 tauto21 cases alternatives with wrap | step22 . have flag := equalNat.true_iff.backward with wrap23 rw flag24 simp [chooseNat]25 have positive : 0 < n by arith26 exact membership.of_Less with positive27 . have flag := equalNat.false_iff.backward with step28 rw flag29 simp [chooseNat]30 have separated : n ≠ succ(l)31 intro same32 apply step33 symm34 exact same35 have below := Less.successor_lower_of_ne with less, separated36 exact membership.of_Less with below3738theorem rotation.step (n : Nat) (l : Set)39 requires hl : l ∈ n40 requires hs : succ(l) ∈ n41 shows rotation(n)(l) = succ(l)42proof43 have lNat := natural.member at n with hl44 have different : succ(l) ≠ n45 intro same46 rw same at hs47 exact membership.irreflexive with hs48 have flag := equalNat.false_iff.backward with different49 have value := rotation.value at n, l with *50 rw [value, flag]51 simp [chooseNat]5253theorem rotation.wrap (n : Nat) (l : Set)54 requires hl : l ∈ n55 requires top : succ(l) = n56 shows rotation(n)(l) = 057proof58 have lNat := natural.member at n with hl59 have flag := equalNat.true_iff.backward with top60 have value := rotation.value at n, l with *61 rw [value, flag]62 simp [chooseNat]6364theorem rotation.cancel (n : Nat) (x y : Set)65 requires hx : x ∈ n66 requires hy : y ∈ n67 requires same : rotation(n)(x) = rotation(n)(y)68 shows x = y69proof70 have xNat := natural.member at n with hx71 have yNat := natural.member at n with hy72 have xLess := Less.of_membership with hx73 have yLess := Less.of_membership with hy74 have xAlternatives : succ(x) = n ∨ succ(x) ≠ n by tauto75 have yAlternatives : succ(y) = n ∨ succ(y) ≠ n by tauto76 cases xAlternatives with xWrap | xStep77 . have xValue := rotation.wrap with hx, xWrap78 cases yAlternatives with yWrap | yStep79 . have both : succ(x) = succ(y)80 rw [xWrap, yWrap]81 rfl82 have forward : x ≤ y by arith83 have backward : y ≤ x by arith84 exact LessEqual.antisymmetric with forward, backward85 . have ySeparated : n ≠ succ(y)86 intro equal87 apply yStep88 symm89 exact equal90 have yIn := membership.of_Less91 with (Less.successor_lower_of_ne with yLess, ySeparated)92 have yValue := rotation.step with hy, yIn93 rw [xValue, yValue] at same94 arith95 . have xSeparated : n ≠ succ(x)96 intro equal97 apply xStep98 symm99 exact equal100 have xIn := membership.of_Less101 with (Less.successor_lower_of_ne with xLess, xSeparated)102 have xValue := rotation.step with hx, xIn103 cases yAlternatives with yWrap | yStep104 . have yValue := rotation.wrap with hy, yWrap105 rw [xValue, yValue] at same106 arith107 . have ySeparated : n ≠ succ(y)108 intro equal109 apply yStep110 symm111 exact equal112 have yIn := membership.of_Less113 with (Less.successor_lower_of_ne with yLess, ySeparated)114 have yValue := rotation.step with hy, yIn115 rw [xValue, yValue] at same116 have forward : x ≤ y by arith117 have backward : y ≤ x by arith118 exact LessEqual.antisymmetric with forward, backward119120theorem rotation.injective (n : Nat)121 shows InjectiveBetween(rotation(n), n, n)122proof123 have function := rotation.function at n with *124 constructor125 . exact function126 . intros x hx y hy z hz hxz hyz127 have xValue := FunctionBetween.apply_value with function, hx, hxz128 have yValue := FunctionBetween.apply_value with function, hy, hyz129 have same : rotation(n)(x) = rotation(n)(y)130 rw [xValue, yValue]131 rfl132 exact rotation.cancel with hx, hy, same133134theorem rotation.surjective (n : Nat)135 shows SurjectiveBetween(rotation(n), n, n)136proof137 have function := rotation.function at n with *138 constructor139 . exact function140 . intros y hy141 have yNat := natural.member at n with hy142 have yLess := Less.of_membership with hy143 have shape := natural.zero_or_successor with yNat144 cases shape with zero | successor145 . have nShape := natural.zero_or_successor at n with *146 cases nShape with nZero | nSuccessor147 . exfalso148 rw nZero at yLess149 arith150 . obtain ⟨m, mNat, nEq⟩ := nSuccessor151 have top : succ(m) = n152 symm153 exact nEq154 have mIn : m ∈ n155 rw nEq156 exact bootstrap.succ.self157 have value := rotation.wrap with mIn, top158 have edge := FunctionBetween.relates_apply with function, mIn159 rw value at edge160 witness m161 constructor162 . exact mIn163 . rw zero164 exact edge165 . obtain ⟨k, kNat, yEq⟩ := successor166 have kLess : k < n167 rw yEq at yLess168 arith169 have kIn := membership.of_Less with kLess170 have sIn : succ(k) ∈ n by rwa ← yEq171 have value := rotation.step with kIn, sIn172 have edge := FunctionBetween.relates_apply with function, kIn173 rw value at edge174 witness k175 constructor176 . exact kIn177 . rw yEq178 exact edge179180theorem rotation.bijective (n : Nat)181 shows BijectiveBetween(rotation(n), n, n)182proof183 constructor184 . exact rotation.injective at n185 . exact rotation.surjective at n186