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
@@ -15,6 +15,7 @@ abbrev Var := Nat
 def Context := Var → Int
 
 structure Monomial where
+  mk ::
   coeff : Int
   vars : List Var
 deriving Inhabited, Repr
@@ -60,8 +61,62 @@ 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
+theorem eq : ∀ {m n : Monomial}, m.coeff = n.coeff → m.vars = n.vars → m = n
+  | ⟨_, _⟩, ⟨_, _⟩, rfl, rfl => rfl
+
+
+
+
+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
+  revert z1 z2
+  induction l with
+  | nil => simp
+  | cons y ys ih =>
+    intro z1 z2
+    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
+  revert z1 z2
+  induction l with
+  | nil => simp
+  | cons y ys ih =>
+    intro z1 z2
+    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 [mul.insert]
+  | 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 +166,93 @@ 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
+    <;> simp only [List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc]
+    case cons.inr h =>
+      split
+      case inl h1 =>
+        split
+        case inl h2 =>
+          rw [←Int.add_assoc, Int.add_comm, ←Monomial.denote_add h1]
+          simp [Monomial.denote, h2]
+        case inr h2 =>
+          simp [-Int.add_zero, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Monomial.denote_add h1, Int.add_assoc]
+      case inr h1 =>
+        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]
+    rw [denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl]
 
 end Polynomial