Shell.lean — FrcCore

1import FrcCore.Nat23/-!4# FrcCore.Shell — the residues of a shell, from first principles56`Shell p` is the set of residues mod `p`, carried by their canonical representatives `val < p` — no7quotient type, so no `Quot.sound`; every identity below is an identity of representatives, decided by8`Nat` arithmetic. The operations reduce by `%`, so `decide` computes on any concrete shell through the9kernel's accelerated `Nat` arithmetic, and every theorem is checked to depend on no axiom.1011The ring laws are derived from `FrcCore.Nat`'s division algorithm (`mod_unique`); negation is12characterised by `add_neg : a + -a = 0`, and everything about `-` follows from the uniqueness of13additive inverses (`neg_unique`), never from `Nat` subtraction.1415Since the ledger migration (task LM17) it also holds `mul_mul_mul_comm` (from 14-entropy and 3-causality).16-/1718namespace FRC1920/-- A residue mod `p`: its representative and the bound. -/21structure Shell (p : Nat) where22  val : Nat23  lt : val < p2425/-- `Pos p`: the modulus is positive. Instances for literals `n + 1` are found automatically. -/26class Pos (p : Nat) : Prop where27  pos : 0 < p2829instance (n : Nat) : Pos (n + 1) := ⟨Nat.zero_lt_succ n⟩3031namespace Shell3233variable {p : Nat}3435theorem ext {a b : Shell p} (h : a.val = b.val) : a = b := by36  cases a; cases b; cases h; rfl3738theorem val_injective {a b : Shell p} (h : a = b) : a.val = b.val := by cases h; rfl3940instance : DecidableEq (Shell p) := fun a b =>41  if h : a.val = b.val then isTrue (ext h) else isFalse (fun e => h (val_injective e))4243section ops44variable [Pos p]4546/-- The residue of a natural number. -/47def ofNat (n : Nat) : Shell p := ⟨n % p, Nat.mod_lt n Pos.pos⟩4849instance (n : Nat) : OfNat (Shell p) n := ⟨ofNat n⟩50instance : Add (Shell p) := ⟨fun a b => ofNat (a.val + b.val)⟩51instance : Mul (Shell p) := ⟨fun a b => ofNat (a.val * b.val)⟩52instance : Neg (Shell p) := ⟨fun a => ofNat (p - a.val)⟩5354/-- Powers by structural recursion (`a ^ 0 = 1`, `a ^ (n+1) = a ^ n * a`). -/55def pow (a : Shell p) : Nat → Shell p56  | 0 => 157  | n + 1 => pow a n * a5859instance : Pow (Shell p) Nat := ⟨pow⟩6061theorem hp : 0 < p := Pos.pos6263@[simp] theorem val_ofNat (n : Nat) : (ofNat n : Shell p).val = n % p := rfl64theorem val_add (a b : Shell p) : (a + b).val = (a.val + b.val) % p := rfl65theorem val_mul (a b : Shell p) : (a * b).val = (a.val * b.val) % p := rfl66theorem val_neg (a : Shell p) : (-a).val = (p - a.val) % p := rfl67theorem val_lit (n : Nat) : (OfNat.ofNat n : Shell p).val = n % p := rfl68theorem val_zero : (0 : Shell p).val = 0 := rfl69theorem val_one : (1 : Shell p).val = 1 % p := rfl70theorem pow_zero (a : Shell p) : a ^ 0 = 1 := rfl71theorem pow_succ (a : Shell p) (n : Nat) : a ^ (n + 1) = a ^ n * a := rfl7273theorem ofNat_val (a : Shell p) : ofNat a.val = a :=74  ext (FRC.Nat.mod_eq_of_lt a.lt)7576theorem ofNat_mod (n : Nat) : (ofNat (n % p) : Shell p) = ofNat n :=77  ext (FRC.Nat.mod_mod n p hp)7879/-! ### The additive laws -/8081theorem add_comm (a b : Shell p) : a + b = b + a :=82  ext (by rw [val_add, val_add, Nat.add_comm])8384theorem add_assoc (a b c : Shell p) : a + b + c = a + (b + c) :=85  ext (by86    rw [val_add, val_add, val_add, val_add, FRC.Nat.mod_add_mod _ _ _ hp, FRC.Nat.add_mod_mod _ _ _ hp,87      Nat.add_assoc])8889theorem zero_add (a : Shell p) : 0 + a = a :=90  ext (by rw [val_add, val_zero, Nat.zero_add]; exact FRC.Nat.mod_eq_of_lt a.lt)9192theorem add_zero (a : Shell p) : a + 0 = a := by rw [add_comm]; exact zero_add a9394theorem add_left_comm (a b c : Shell p) : a + (b + c) = b + (a + c) := by95  rw [← add_assoc, add_comm a b, add_assoc]9697theorem add_add_add_comm (a b c d : Shell p) : a + b + (c + d) = a + c + (b + d) := by98  rw [add_assoc, add_assoc, add_left_comm b]99100/-! ### The multiplicative laws -/101102theorem mul_comm (a b : Shell p) : a * b = b * a :=103  ext (by rw [val_mul, val_mul, Nat.mul_comm])104105theorem mul_assoc (a b c : Shell p) : a * b * c = a * (b * c) :=106  ext (by107    rw [val_mul, val_mul, val_mul, val_mul, FRC.Nat.mod_mul_mod _ _ _ hp, FRC.Nat.mul_mod_mod _ _ _ hp,108      FRC.Nat.mul_assoc])109110theorem one_mul (a : Shell p) : 1 * a = a :=111  ext (by rw [val_mul, val_one, FRC.Nat.mod_mul_mod _ _ _ hp, Nat.one_mul]; exact FRC.Nat.mod_eq_of_lt a.lt)112113theorem mul_one (a : Shell p) : a * 1 = a := by rw [mul_comm]; exact one_mul a114115theorem zero_mul (a : Shell p) : 0 * a = 0 :=116  ext (by rw [val_mul, val_zero, Nat.zero_mul]; rfl)117118theorem mul_zero (a : Shell p) : a * 0 = 0 := by rw [mul_comm]; exact zero_mul a119120theorem mul_left_comm (a b c : Shell p) : a * (b * c) = b * (a * c) := by121  rw [← mul_assoc, mul_comm a b, mul_assoc]122123theorem left_distrib (a b c : Shell p) : a * (b + c) = a * b + a * c :=124  ext (by125    rw [val_mul, val_add, val_add, val_mul, val_mul, FRC.Nat.mul_mod_mod _ _ _ hp,126      FRC.Nat.add_mod _ _ _ hp, FRC.Nat.mod_mod _ _ hp, FRC.Nat.mod_mod _ _ hp, ← FRC.Nat.add_mod _ _ _ hp,127      Nat.left_distrib])128129theorem right_distrib (a b c : Shell p) : (a + b) * c = a * c + b * c := by130  rw [mul_comm, left_distrib, mul_comm c a, mul_comm c b]131132/-! ### Negation, characterised by `add_neg` -/133134theorem add_neg (a : Shell p) : a + -a = 0 :=135  ext (by136    rw [val_add, val_neg, FRC.Nat.add_mod_mod _ _ _ hp, FRC.Nat.add_sub_of_le (Nat.le_of_lt a.lt),137      FRC.Nat.mod_self p hp]; rfl)138139theorem neg_add (a : Shell p) : -a + a = 0 := by rw [add_comm]; exact add_neg a140141/-- Additive inverses are unique. -/142theorem neg_unique {a x y : Shell p} (hx : a + x = 0) (hy : a + y = 0) : x = y := by143  calc x = x + 0 := (add_zero x).symm144    _ = x + (a + y) := by rw [hy]145    _ = (x + a) + y := (add_assoc _ _ _).symm146    _ = (a + x) + y := by rw [add_comm x a]147    _ = 0 + y := by rw [hx]148    _ = y := zero_add y149150theorem neg_eq_of_add_eq_zero {a b : Shell p} (h : a + b = 0) : -a = b :=151  neg_unique (add_neg a) h152153theorem neg_neg (a : Shell p) : - -a = a :=154  neg_eq_of_add_eq_zero (neg_add a)155156theorem neg_zero : (-0 : Shell p) = 0 :=157  neg_eq_of_add_eq_zero (add_zero 0)158159theorem neg_mul (a b : Shell p) : -(a * b) = -a * b :=160  neg_eq_of_add_eq_zero (by rw [← right_distrib, add_neg, zero_mul])161162theorem mul_neg (a b : Shell p) : -(a * b) = a * -b := by163  rw [mul_comm, neg_mul, mul_comm]164165theorem neg_mul_neg (a b : Shell p) : -a * -b = a * b := by166  rw [← neg_mul, ← mul_neg, neg_neg]167168theorem neg_add_rev (a b : Shell p) : -(a + b) = -a + -b :=169  neg_eq_of_add_eq_zero (by170    rw [add_assoc, add_left_comm b, ← add_assoc, add_neg, zero_add, add_neg])171172theorem add_right_cancel {a b c : Shell p} (h : a + c = b + c) : a = b := by173  have : a + c + -c = b + c + -c := by rw [h]174  rw [add_assoc, add_neg, add_zero, add_assoc, add_neg, add_zero] at this175  exact this176177theorem eq_neg_of_add_eq_zero {a b : Shell p} (h : a + b = 0) : a = -b := by178  rw [← neg_neg a, neg_eq_of_add_eq_zero h]179180theorem neg_one_mul (a : Shell p) : -1 * a = -a := by rw [← neg_mul, one_mul]181182/-! ### Powers -/183184theorem pow_one (a : Shell p) : a ^ 1 = a := by rw [pow_succ, pow_zero, one_mul]185186theorem one_pow (n : Nat) : (1 : Shell p) ^ n = 1 := by187  induction n with188  | zero => rfl189  | succ n ih => rw [pow_succ, ih, mul_one]190191theorem pow_add (a : Shell p) (m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by192  induction n with193  | zero => rw [Nat.add_zero, pow_zero, mul_one]194  | succ n ih => rw [Nat.add_succ, pow_succ, ih, pow_succ, mul_assoc]195196theorem pow_mul (a : Shell p) (m n : Nat) : a ^ (m * n) = (a ^ m) ^ n := by197  induction n with198  | zero => rw [Nat.mul_zero, pow_zero, pow_zero]199  | succ n ih => rw [Nat.mul_succ, pow_add, ih, pow_succ]200201theorem pow_mul_comm (a : Shell p) (m n : Nat) : (a ^ m) ^ n = (a ^ n) ^ m := by202  rw [← pow_mul, Nat.mul_comm, pow_mul]203204theorem mul_pow (a b : Shell p) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by205  induction n with206  | zero => rw [pow_zero, pow_zero, pow_zero, mul_one]207  | succ n ih =>208    rw [pow_succ, pow_succ, pow_succ, ih, mul_assoc, mul_assoc, mul_left_comm (b ^ n) a b]209210theorem pow_two (a : Shell p) : a ^ 2 = a * a := by rw [pow_succ, pow_one]211212theorem neg_pow_two (a : Shell p) : (-a) ^ 2 = a ^ 2 := by rw [pow_two, pow_two, neg_mul_neg]213214/-- `(-1)^n` by the parity of `n`. -/215theorem neg_one_pow (n : Nat) : (-1 : Shell p) ^ n = if n % 2 = 0 then 1 else -1 := by216  induction n with217  | zero => rfl218  | succ n ih =>219    rw [pow_succ, ih]220    exact match Nat.decEq (n % 2) 0 with221      | .isTrue h => by222          rw [ite_eq_left h, one_mul]223          have : (n + 1) % 2 = 1 := by224            rw [← FRC.Nat.mod_add_mod _ _ _ (Nat.zero_lt_succ 1), h]225          rw [ite_eq_right (by rw [this]; exact fun e => Nat.noConfusion e)]226      | .isFalse h => by227          rw [ite_eq_right h, neg_mul_neg, one_mul]228          have h1 : n % 2 = 1 := by229            have := Nat.mod_lt n (Nat.zero_lt_succ 1)230            exact match n % 2, this, h with231              | 0, _, h => absurd rfl h232              | 1, _, _ => rfl233              | k + 2, hk, _ => absurd hk (Nat.not_lt_of_le (Nat.le_add_left 2 k))234          have : (n + 1) % 2 = 0 := by235            rw [← FRC.Nat.mod_add_mod _ _ _ (Nat.zero_lt_succ 1), h1]236          rw [ite_eq_left this]237238/-- `a b (c d) = a c (b d)` on every shell (14-entropy and 3-causality's lemma, moved by task LM17). -/239theorem mul_mul_mul_comm (a b c d : Shell p) : a * b * (c * d) = a * c * (b * d) := by240  rw [mul_assoc, mul_left_comm b c d, ← mul_assoc]241242end ops243244end Shell245end FRC246