Ring.lean — FrcCore

1import FrcCore.Shell23/-!4# FrcCore.Ring — a normaliser for ring identities on the shell (the base theme)56An identity between two polynomial expressions over the shell is decided by expanding each side into a positive and a7negative list of monomials, sorting, and comparing; `RE.sound` turns a successful comparison, a kernel computation8(`decide +kernel`), into the equation on the shell. Moved by the ledger migration (task LM24) from9`Theme/Extension.lean`, where the quaternion norm uses it, every name unchanged (`FRC.Shell.Frame.RE`, `look`,10`RE.sound`, `RE.check`), so that every theme can decide its ring identities. No axioms.11-/1213namespace FRC14namespace Shell15namespace Frame1617variable {p : Nat} [Pos p]1819/-! ## A normaliser for ring identities on the shell (no axioms)2021An identity between two polynomial expressions is decided by expanding each side into a positive and a negative22list of monomials, sorting, and comparing `P_l ++ N_r` with `P_r ++ N_l`; `RE.sound` turns a successful comparison23(a kernel computation, `decide`) into the equation on the shell. -/2425inductive RE where26  | var : Nat → RE27  | zero : RE28  | one : RE29  | add : RE → RE → RE30  | mul : RE → RE → RE31  | neg : RE → RE3233def RE.eval (env : Nat → Shell p) : RE → Shell p34  | .var i => env i35  | .zero => 036  | .one => 137  | .add a b => a.eval env + b.eval env38  | .mul a b => a.eval env * b.eval env39  | .neg a => -(a.eval env)4041/-- The assignment of shell values to the variables `0, 1, 2, …` of an expression. -/42def look : List (Shell p) → Nat → Shell p43  | [], _ => 044  | x :: _, 0 => x45  | _ :: l, n + 1 => look l n4647def mEval (env : Nat → Shell p) : List Nat → Shell p48  | [] => 149  | i :: m => env i * mEval env m5051def pEval (env : Nat → Shell p) : List (List Nat) → Shell p52  | [] => 053  | m :: P => mEval env m + pEval env P5455def pRow (m : List Nat) : List (List Nat) → List (List Nat)56  | [] => []57  | n :: Q => (m ++ n) :: pRow m Q5859def pMul : List (List Nat) → List (List Nat) → List (List Nat)60  | [], _ => []61  | m :: P, Q => pRow m Q ++ pMul P Q6263def RE.toP : RE → List (List Nat) × List (List Nat)64  | .var i => ([[i]], [])65  | .zero => ([], [])66  | .one => ([[]], [])67  | .add a b => (a.toP.1 ++ b.toP.1, a.toP.2 ++ b.toP.2)68  | .mul a b => (pMul a.toP.1 b.toP.1 ++ pMul a.toP.2 b.toP.2, pMul a.toP.1 b.toP.2 ++ pMul a.toP.2 b.toP.1)69  | .neg a => (a.toP.2, a.toP.1)7071def insM (i : Nat) : List Nat → List Nat72  | [] => [i]73  | j :: m => if Nat.ble i j then i :: j :: m else j :: insM i m7475def sortM : List Nat → List Nat76  | [] => []77  | i :: m => insM i (sortM m)7879def lexLe : List Nat → List Nat → Bool80  | [], _ => true81  | _ :: _, [] => false82  | i :: m, j :: n => if i = j then lexLe m n else Nat.ble i j8384def insP (m : List Nat) : List (List Nat) → List (List Nat)85  | [] => [m]86  | n :: P => if lexLe m n then m :: n :: P else n :: insP m P8788def sortP : List (List Nat) → List (List Nat)89  | [] => []90  | m :: P => insP m (sortP P)9192def nfP : List (List Nat) → List (List Nat)93  | [] => []94  | m :: P => insP (sortM m) (nfP P)9596theorem mEval_append (env : Nat → Shell p) (m n : List Nat) : mEval env (m ++ n) = mEval env m * mEval env n := by97  induction m with98  | nil => exact (one_mul _).symm99  | cons i m ih => show env i * mEval env (m ++ n) = env i * mEval env m * mEval env n; rw [ih, mul_assoc]100101theorem pEval_append (env : Nat → Shell p) (P Q : List (List Nat)) : pEval env (P ++ Q) = pEval env P + pEval env Q := by102  induction P with103  | nil => exact (zero_add _).symm104  | cons m P ih => show mEval env m + pEval env (P ++ Q) = mEval env m + pEval env P + pEval env Q; rw [ih, add_assoc]105106theorem pEval_row (env : Nat → Shell p) (m : List Nat) (Q : List (List Nat)) : pEval env (pRow m Q) = mEval env m * pEval env Q := by107  induction Q with108  | nil => exact (mul_zero _).symm109  | cons n Q ih =>110    show mEval env (m ++ n) + pEval env (pRow m Q) = mEval env m * (mEval env n + pEval env Q)111    rw [ih, mEval_append, left_distrib]112113theorem pEval_mul (env : Nat → Shell p) (P Q : List (List Nat)) : pEval env (pMul P Q) = pEval env P * pEval env Q := by114  induction P with115  | nil => exact (zero_mul _).symm116  | cons m P ih =>117    show pEval env (pRow m Q ++ pMul P Q) = (mEval env m + pEval env P) * pEval env Q118    rw [pEval_append, pEval_row, ih, right_distrib]119120theorem ring_add (A B C D : Shell p) : A + -B + (C + -D) = A + C + -(B + D) := by121  rw [neg_add_rev, add_assoc, add_assoc, add_left_comm (-B) C (-D)]122123theorem ring_mul (A B C D : Shell p) : (A + -B) * (C + -D) = A * C + B * D + -(A * D + B * C) := by124  rw [right_distrib, left_distrib, left_distrib, ← mul_neg, ← neg_mul, neg_mul_neg, neg_add_rev, add_assoc, add_assoc]125  refine congrArg (A * C + ·) ?_126  rw [add_comm (-(B * C)) (B * D), add_left_comm]127128theorem ring_neg (A B : Shell p) : -(A + -B) = B + -A := by rw [neg_add_rev, neg_neg, add_comm]129130theorem RE.toP_eval (env : Nat → Shell p) (e : RE) : e.eval env = pEval env e.toP.1 + -(pEval env e.toP.2) := by131  induction e with132  | var i =>133    show env i = (env i * 1 + 0) + -(0 : Shell p)134    rw [mul_one, add_zero, neg_zero, add_zero]135  | zero => show (0 : Shell p) = 0 + -0; rw [neg_zero, add_zero]136  | one => show (1 : Shell p) = (1 + 0) + -(0 : Shell p); rw [add_zero, neg_zero, add_zero]137  | add a b iha ihb =>138    show a.eval env + b.eval env = pEval env (a.toP.1 ++ b.toP.1) + -(pEval env (a.toP.2 ++ b.toP.2))139    rw [iha, ihb, pEval_append, pEval_append, ring_add]140  | mul a b iha ihb =>141    show a.eval env * b.eval env = pEval env (pMul a.toP.1 b.toP.1 ++ pMul a.toP.2 b.toP.2) +142      -(pEval env (pMul a.toP.1 b.toP.2 ++ pMul a.toP.2 b.toP.1))143    rw [iha, ihb, pEval_append, pEval_append, pEval_mul, pEval_mul, pEval_mul, pEval_mul, ring_mul]144  | neg a iha =>145    show -(a.eval env) = pEval env a.toP.2 + -(pEval env a.toP.1)146    rw [iha, ring_neg]147148theorem mEval_insM (env : Nat → Shell p) (i : Nat) (m : List Nat) : mEval env (insM i m) = env i * mEval env m := by149  induction m with150  | nil => rfl151  | cons j m ih =>152    show mEval env (if Nat.ble i j then i :: j :: m else j :: insM i m) = env i * (env j * mEval env m)153    cases Nat.ble i j with154    | true => rfl155    | false => show env j * mEval env (insM i m) = _; rw [ih, mul_left_comm]156157theorem mEval_sortM (env : Nat → Shell p) (m : List Nat) : mEval env (sortM m) = mEval env m := by158  induction m with159  | nil => rfl160  | cons i m ih => show mEval env (insM i (sortM m)) = env i * mEval env m; rw [mEval_insM, ih]161162theorem pEval_insP (env : Nat → Shell p) (m : List Nat) (P : List (List Nat)) : pEval env (insP m P) = mEval env m + pEval env P := by163  induction P with164  | nil => rfl165  | cons n P ih =>166    show pEval env (if lexLe m n then m :: n :: P else n :: insP m P) = mEval env m + (mEval env n + pEval env P)167    cases lexLe m n with168    | true => rfl169    | false => show mEval env n + pEval env (insP m P) = _; rw [ih, add_left_comm]170171theorem pEval_nfP (env : Nat → Shell p) (P : List (List Nat)) : pEval env (nfP P) = pEval env P := by172  induction P with173  | nil => rfl174  | cons m P ih => show pEval env (insP (sortM m) (nfP P)) = mEval env m + pEval env P; rw [pEval_insP, ih, mEval_sortM]175176def nbeq : List Nat → List Nat → Bool177  | [], [] => true178  | [], _ :: _ => false179  | _ :: _, [] => false180  | i :: m, j :: n => Nat.beq i j && nbeq m n181182def pbeq : List (List Nat) → List (List Nat) → Bool183  | [], [] => true184  | [], _ :: _ => false185  | _ :: _, [] => false186  | m :: P, n :: Q => nbeq m n && pbeq P Q187188theorem and_true_left {a b : Bool} (h : (a && b) = true) : a = true := by189  cases a with190  | false => exact absurd h (fun h' => Bool.noConfusion h')191  | true => rfl192193theorem and_true_right {a b : Bool} (h : (a && b) = true) : b = true := by194  cases a with195  | false => exact absurd h (fun h' => Bool.noConfusion h')196  | true => exact h197198theorem nbeq_eq : ∀ {m n : List Nat}, nbeq m n = true → m = n199  | [], [], _ => rfl200  | i :: m, j :: n, h => by201    have e1 : i = j := Nat.eq_of_beq_eq_true (and_true_left h)202    have e2 : m = n := nbeq_eq (and_true_right h)203    rw [e1, e2]204  | [], _ :: _, h => Bool.noConfusion h205  | _ :: _, [], h => Bool.noConfusion h206207theorem pbeq_eq : ∀ {P Q : List (List Nat)}, pbeq P Q = true → P = Q208  | [], [], _ => rfl209  | m :: P, n :: Q, h => by210    have e1 : m = n := nbeq_eq (and_true_left h)211    have e2 : P = Q := pbeq_eq (and_true_right h)212    rw [e1, e2]213  | [], _ :: _, h => Bool.noConfusion h214  | _ :: _, [], h => Bool.noConfusion h215216/-- The normaliser's soundness: if the two cross lists agree after normalisation, the two sides are equal on217every assignment of shell values to the variables. -/218theorem RE.sound (env : Nat → Shell p) (l r : RE) (hb : pbeq (nfP (l.toP.1 ++ r.toP.2)) (nfP (r.toP.1 ++ l.toP.2)) = true) :219    l.eval env = r.eval env := by220  have h := pbeq_eq hb221  have h1 : pEval env l.toP.1 + pEval env r.toP.2 = pEval env r.toP.1 + pEval env l.toP.2 := by222    rw [← pEval_append, ← pEval_append, ← pEval_nfP env (l.toP.1 ++ r.toP.2), ← pEval_nfP env (r.toP.1 ++ l.toP.2), h]223  rw [RE.toP_eval env l, RE.toP_eval env r]224  apply add_right_cancel (c := pEval env l.toP.2 + pEval env r.toP.2)225  rw [← add_assoc, add_assoc (pEval env l.toP.1), neg_add, add_zero,226      ← add_assoc, add_comm (pEval env r.toP.1 + -(pEval env r.toP.2)) (pEval env l.toP.2), ← add_assoc,227      add_comm (pEval env l.toP.2) (pEval env r.toP.1), add_assoc, neg_add, add_zero, h1]228229/-- The normaliser's test: the two cross lists agree after normalisation. -/230def RE.check (l r : RE) : Bool := pbeq (nfP (l.toP.1 ++ r.toP.2)) (nfP (r.toP.1 ++ l.toP.2))231232end Frame233end Shell234end FRC235