Polynorm proofs

Smt/Reconstruct/Int/Polynorm.lean

@@ -2,7 +2,7 @@
 Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
 institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Abdalrhman Mohamed
+Authors: Abdalrhman Mohamed, Harun Khan
 -/
 
 import Lean
@@ -60,8 +60,52 @@ def denote (ctx : Context) (m : Monomial) : Int :=
 theorem denote_neg {m : Monomial} : m.neg.denote ctx = -m.denote ctx := by
   simp only [neg, denote, Int.neg_mul_eq_neg_mul]
 
-theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx :=
-  sorry
+section
+
+variable {op : α → α → α} (assoc : ∀ a b c, op (op a b) c = op a (op b c))
+
+-- Can be generalized to `List.foldl_assoc`.
+theorem foldl_assoc {g : β → α} (z1 z2 : α) :
+  List.foldl (fun z a => op z (g a)) (op z1 z2) l =
+  op z1 (List.foldl (fun z a => op z (g a)) z2 l) := by
+  induction l generalizing z1 z2 with
+  | nil => rfl
+  | cons y ys ih =>
+    simp only [List.foldl_cons, ih, assoc]
+
+theorem foldr_assoc {g : β → α} (z1 z2 : α) :
+  List.foldr (fun z a => op a (g z)) (op z1 z2) l =
+  op z1 (List.foldr (fun z a => op a (g z)) z2 l) := by
+  induction l generalizing z1 z2 with
+  | nil => rfl
+  | cons y ys ih =>
+    simp only [List.foldr_cons, ih, assoc]
+
+end
+-- Can be generazlized.
+theorem foldl_mul_insert {ctx : Context} :
+  List.foldl (fun z a => z * (ctx a)) 1 (mul.insert y ys) =
+  (ctx y) * List.foldl (fun z a => z * (ctx a)) 1 ys := by
+  induction ys with
+  | nil => simp [List.foldl]
+  | cons x ys ih =>
+    by_cases h : y ≤ x
+    · simp [mul.insert, h, foldl_assoc Int.mul_assoc (ctx y) (ctx x), Int.mul_assoc]
+    · simp only [mul.insert, h, List.foldl_cons, ite_false, Int.mul_comm,
+                 foldl_assoc Int.mul_assoc, ih]
+      rw [←Int.mul_assoc, Int.mul_comm (ctx x) (ctx y), Int.mul_assoc]
+
+theorem denote_add {m n : Monomial} (h : m.vars = n.vars) :
+  (m.add n h).denote ctx = m.denote ctx + n.denote ctx := by
+  simp only [add, denote, Int.add_mul, h]
+
+theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.denote ctx * m₂.denote ctx := by
+  simp only [denote, mul, Int.mul_assoc]; congr 1
+  rw [← Int.mul_assoc, Int.mul_comm _ m₂.coeff, Int.mul_assoc]; congr 1
+  induction m₁.vars with
+  | nil => simp [Int.mul_assoc]
+  | cons y ys ih =>
+    simp [foldl_mul_insert, ←foldl_assoc Int.mul_assoc, ih]
 
 end Monomial
 
@@ -111,20 +155,83 @@ def mul (p q : Polynomial) : Polynomial :=
 def denote (ctx : Context) (p : Polynomial) : Int :=
   p.foldl (fun acc m => acc + m.denote ctx) 0
 
-theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx :=
-  sorry
+theorem foldl_add_insert (ctx : Context) :
+  List.foldl (fun z a => z + (Monomial.denote ctx a)) 0 (add.insert m p) =
+  (Monomial.denote ctx m) + List.foldl (fun z a => z + (Monomial.denote ctx a)) 0 p := by
+  induction p with
+  | nil => simp [add.insert]
+  | cons n p ih =>
+    simp only [add.insert]
+    split <;> rename_i hlt <;> simp only [List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc]
+    · split <;> rename_i heq
+      · split <;> rename_i hneq
+        · rw [←Int.add_assoc, Int.add_comm, ←Monomial.denote_add heq]
+          simp [Monomial.denote, hneq]
+        · simp [-Int.add_zero, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Monomial.denote_add, heq, Int.add_assoc]
+      · simp only [List.foldl_cons, Int.add_comm 0, ih, Monomial.foldl_assoc Int.add_assoc]
+        rw [←Int.add_assoc, Int.add_comm (Monomial.denote ctx n), Int.add_assoc]
+
+theorem denote_neg {p : Polynomial} : p.neg.denote ctx = -p.denote ctx := by
+  simp only [denote, neg]
+  induction p with
+  | nil => simp
+  | cons m p ih =>
+    simp only [List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc,Int.neg_add, ←ih, List.map, Monomial.denote_neg]
+
+theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx := by
+  simp only [denote, add]
+  induction p with
+  | nil => simp [add.insert]
+  | cons x ys ih =>
+    simp only [List.foldr_cons, List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Int.add_assoc]
+    rw [← ih, foldl_add_insert]
 
-theorem denote_add {p q : Polynomial} : (p.add q).denote ctx = p.denote ctx + q.denote ctx :=
-  sorry
 
 theorem denote_sub {p q : Polynomial} : (p.sub q).denote ctx = p.denote ctx - q.denote ctx := by
   simp only [sub, denote_neg, denote_add, Int.sub_eq_add_neg]
 
-theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx :=
-  sorry
-
-theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx :=
-  sorry
+theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.denote ctx * p.denote ctx := by
+  simp only [denote, mulMonomial, add]
+  induction p with
+  | nil => simp
+  | cons n p ih =>
+    simp only [List.foldl_cons, List.foldr_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Int.mul_add, ←ih]
+    simp [foldl_add_insert, Monomial.denote_mul]
+
+theorem denote_cons {p : List Monomial} {ctx : Context} : denote ctx (m :: p) = m.denote ctx + denote ctx p := by
+  simp only [denote, List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc]
+
+theorem denote_nil_add : denote ctx (p.add []) = denote ctx p := by
+  induction p with
+  | nil => simp [add]
+  | cons n p ih =>
+    simp [denote_add, List.foldr_cons, denote_cons, ih, show denote ctx [] = 0 by rfl]
+
+theorem denote_add_insert {g : Monomial → Polynomial} :
+  denote ctx (List.foldl (fun acc m => (g m).add acc) n p) = denote ctx n + denote ctx (List.foldl (fun acc m => (g m).add acc) [] p) := by
+  revert n
+  induction p with
+  | nil => simp [denote]
+  | cons k p ih =>
+    intro n
+    simp only [List.foldl_cons, List.foldr, @ih n]
+    rw [ih, @ih ((g k).add []), ← Int.add_assoc, denote_nil_add, denote_add, Int.add_comm _ (denote ctx n)]
+
+theorem denote_foldl {g : Monomial → Polynomial} :
+  denote ctx (List.foldl (fun acc m => ((g m).add (acc))) [] p) = List.foldl (fun acc m => (g m).denote ctx + acc) 0 p := by
+  induction p with
+  | nil => simp [denote]
+  | cons n p ih =>
+    simp only [List.foldl_cons, Int.add_comm, List.foldr] at *
+    rw [Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, ←ih, denote_add_insert, denote_nil_add]
+
+theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := by
+  simp only [mul]
+  induction p with
+  | nil => simp [denote]
+  | cons n p ih =>
+    simp only [List.foldl_cons, denote_cons, Int.add_mul, ← ih]
+    rw [denote_foldl, denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl]
 
 end Polynomial