From c237ed2a141d7cbf06f6d780c2f5d91966621871 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Wed, 10 Jul 2024 11:40:19 -0700 Subject: [PATCH 01/15] lemmas --- Smt/Reconstruct/Int/Polynorm.lean | 248 ++++++++++++++++++++++++++++-- 1 file changed, 238 insertions(+), 10 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 4673a41c..586d0b80 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.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,104 @@ 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] + +theorem foldl_ite {m : Monomial} (g : Var → Int) (hi : i ∈ m.vars) : + ∃ k : Nat, List.foldl (fun acc v => acc * (if v = i then (g i) else 1)) z m.vars = z * (g i)^k := by + revert z hi + induction m.vars with + | nil => intro z hi; simp at hi + | cons v l ih => + intro z hi + cases hi with + | head => + simp [foldl_assoc Int.mul_assoc] + sorry + | tail _ ha => + simp only [List.foldl_cons, Int.one_mul] + have ⟨k, hk⟩ := @ih (z * if v = i then g i else 1) ha + rw [hk] + split + case inl hv => rw [Int.mul_assoc, Int.mul_comm (g i), ←Int.pow_succ] + exact ⟨k + 1, rfl⟩ + case inr _ => rw [Int.mul_one] + exact ⟨k, rfl⟩ + + +-- theorem denote_eq {m n : Monomial} (h : ∀ ctx : Context, m.denote ctx = n.denote ctx) : m = n := by +-- apply eq +-- · sorry +-- · induction m.vars, n.vars using List.rec with +-- | nil nil => sorry +-- | nil cons a b => sorry +-- | cons a b nil => sorry +-- | cons a b ih cons c d ih1 => sorry + + + + + -- · sorry + -- · apply List.ext_get + -- · sorry + -- · intro i h1 h2; + -- have h3 := h (fun j => if i = j then i else 1) + -- simp [denote] at h3 + -- sorry end Monomial @@ -97,6 +194,10 @@ where else n :: insert m ns +#eval add [⟨5, [0, 1]⟩, ⟨7, [0, 1, 1]⟩] [⟨3, [0, 1, 1]⟩, ⟨2, [0, 1]⟩] +#eval add [⟨3, [0, 1, 1]⟩, ⟨2, [0, 1]⟩] [⟨5, [0, 1]⟩, ⟨7, [0, 1, 1]⟩] + + def sub (p q : Polynomial) : Polynomial := p.add q.neg @@ -111,20 +212,147 @@ 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_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_add_insert {g : Monomial → Polynomial} : + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) (g n) p) = denote ctx (g n) + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) [] p) := by + induction p with + | nil => simp [denote] + | cons k p ih => + simp only [List.foldl_cons, List.foldr] + sorry + + + +theorem denote_foldl {g : Monomial → Polynomial} : + denote ctx (List.foldl (fun acc m => (acc.add (g m))) [] 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, add, Int.add_comm, List.foldr] at * + rw [Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, ←ih] + + sorry + +-- #check Fin.mk +-- theorem denote_cast {p : List Monomial} : +-- denote ctx (List.foldl f [] p) = List.foldl (fun acc m => denote ctx (f [m] ⟨acc, []⟩)) 0 p := by +-- induction p with +-- | nil => simp [denote] +-- | cons n p ih => +-- simp only [List.foldl_cons] +-- rw [← Int.add_zero (denote ctx (f [n] ⟨0, []⟩)), Monomial.foldl_assoc Int.add_assoc] + +theorem denote_ite {p : Polynomial} : denote (fun j => if j = i then 1 else 0) p = if h : i < p.length then Monomial.denote (fun _ => 1) (p.get ⟨i, h⟩) else 0:= by + induction p with + | nil => sorry + | cons n p ih => + split + case cons.inl h1 => + simp only [denote, List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Monomial.denote] + sorry + sorry + + +#check List.ext_get + +theorem denote_eq {p q : Polynomial} (h : ∀ ctx, p.denote ctx = q.denote ctx) : p = q := by + apply List.ext_get + · sorry + · intro i h1 h2 + have h' := h (fun j => if j = i then 1 else 0) + rw [denote_ite, denote_ite] at h' + simp [h1, h2, Monomial.denote] at h' + apply Monomial.eq + · sorry + · sorry + +theorem add_assoc :∀ (p q r : Polynomial), add (add p q) r = add p (add q r) := by + intro p q r; simp only [add]; revert p q + induction r with + | nil => sorry + | cons n r ih => + intro p q + simp only [add, add.insert, List.foldr_cons, ih p q] + induction q with + | nil => simp + | cons => sorry + +theorem add_comm : ∀ (p q : Polynomial), add p q = add q p := by + intro p; simp only [add] + induction p with + | nil => sorry + | cons n p ih => + intro q + simp only [add, add.insert, List.foldr_cons, ih q] + induction q with + | nil => unfold add.insert + simp + sorryAx + | cons => sorry + + + +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, add_comm] + rw [add_comm, Monomial.foldl_assoc add_assoc] + simp [denote_add, denote_mulMonomial] -theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := - sorry end Polynomial From 6394a9a81bfa76f0438fec7d5446a7320ae24ad6 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Thu, 11 Jul 2024 13:14:19 -0700 Subject: [PATCH 02/15] sorries --- Smt/Reconstruct/Int/Polynorm.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 586d0b80..09640c2c 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -324,9 +324,8 @@ theorem add_assoc :∀ (p q r : Polynomial), add (add p q) r = add p (add q r) : | nil => sorry | cons n r ih => intro p q - simp only [add, add.insert, List.foldr_cons, ih p q] induction q with - | nil => simp + | nil => sorry | cons => sorry theorem add_comm : ∀ (p q : Polynomial), add p q = add q p := by @@ -339,7 +338,7 @@ theorem add_comm : ∀ (p q : Polynomial), add p q = add q p := by induction q with | nil => unfold add.insert simp - sorryAx + sorry | cons => sorry From 36e03aa0e2d4a2c1ef844241462db84eb562070c Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Thu, 25 Jul 2024 12:50:11 -0700 Subject: [PATCH 03/15] progress --- Smt/Reconstruct/Int/Polynorm.lean | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 09640c2c..e9248bd0 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -266,12 +266,18 @@ theorem denote_cons {p : List Monomial} {ctx : Context} : denote ctx (m :: p) = theorem denote_add_insert {g : Monomial → Polynomial} : - denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) (g n) p) = denote ctx (g n) + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) [] p) := by + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) n p) = denote ctx n + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) [] p) := by + revert n induction p with | nil => simp [denote] | cons k p ih => - simp only [List.foldl_cons, List.foldr] - sorry + intro n + simp only [List.foldl_cons, List.foldr, @ih n] + rw [ih, @ih (g k), ← Int.add_assoc] + congr 1 + have := @denote_add ctx n (g k) + simp only [add] at this; exact this + @@ -281,9 +287,7 @@ theorem denote_foldl {g : Monomial → Polynomial} : | nil => simp [denote] | cons n p ih => simp only [List.foldl_cons, add, Int.add_comm, List.foldr] at * - rw [Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, ←ih] - - sorry + rw [Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, ←ih, denote_add_insert] -- #check Fin.mk -- theorem denote_cast {p : List Monomial} : @@ -349,8 +353,12 @@ theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q. | nil => simp [denote] | cons n p ih => simp only [List.foldl_cons, denote_cons, Int.add_mul, ← ih, add_comm] - rw [add_comm, Monomial.foldl_assoc add_assoc] - simp [denote_add, denote_mulMonomial] + rw [denote_foldl] + simp only [add, Polynomial.add] + sorry + -- rw [denote_add_insert, denote_add_insert, ←denote_mulMonomial, mulMonomial] + -- rw [add_comm, Monomial.foldl_assoc add_assoc] + -- simp [denote_add, denote_mulMonomial] end Polynomial From d9323105a85d10bf9e5eabb96ed9095672a238fa Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 29 Jul 2024 04:01:08 -0700 Subject: [PATCH 04/15] no sorries --- Smt/Reconstruct/Int/Polynorm.lean | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index e9248bd0..62c12e14 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -264,30 +264,32 @@ theorem denote_mulMonomial {p : Polynomial} : (p.mulMonomial m).denote ctx = m.d 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 => List.foldr add.insert (g m) acc) n p) = denote ctx n + denote ctx (List.foldl (fun acc m => List.foldr add.insert (g m) acc) [] p) := by + 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), ← Int.add_assoc] - congr 1 - have := @denote_add ctx n (g k) - simp only [add] at this; exact this + 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 => (acc.add (g m))) [] p) = List.foldl (fun acc m => (g m).denote ctx + acc) 0 p := by + 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, add, Int.add_comm, List.foldr] at * - rw [Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, ←ih, denote_add_insert] + 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] -- #check Fin.mk -- theorem denote_cast {p : List Monomial} : @@ -352,14 +354,9 @@ theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q. induction p with | nil => simp [denote] | cons n p ih => - simp only [List.foldl_cons, denote_cons, Int.add_mul, ← ih, add_comm] + simp only [List.foldl_cons, denote_cons, Int.add_mul, ← ih] rw [denote_foldl] - simp only [add, Polynomial.add] - sorry - -- rw [denote_add_insert, denote_add_insert, ←denote_mulMonomial, mulMonomial] - -- rw [add_comm, Monomial.foldl_assoc add_assoc] - -- simp [denote_add, denote_mulMonomial] - + rw [denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl] end Polynomial From 7ab8e701a50777505b0232d0e7efdd939b754481 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 29 Jul 2024 04:02:36 -0700 Subject: [PATCH 05/15] small changes --- Smt/Reconstruct/Int/Polynorm.lean | 106 +----------------------------- 1 file changed, 1 insertion(+), 105 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 62c12e14..eda537db 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/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 @@ -118,48 +118,6 @@ theorem denote_mul {m₁ m₂ : Monomial} : (m₁.mul m₂).denote ctx = m₁.de | cons y ys ih => simp [foldl_mul_insert, ←foldl_assoc Int.mul_assoc, ih] -theorem foldl_ite {m : Monomial} (g : Var → Int) (hi : i ∈ m.vars) : - ∃ k : Nat, List.foldl (fun acc v => acc * (if v = i then (g i) else 1)) z m.vars = z * (g i)^k := by - revert z hi - induction m.vars with - | nil => intro z hi; simp at hi - | cons v l ih => - intro z hi - cases hi with - | head => - simp [foldl_assoc Int.mul_assoc] - sorry - | tail _ ha => - simp only [List.foldl_cons, Int.one_mul] - have ⟨k, hk⟩ := @ih (z * if v = i then g i else 1) ha - rw [hk] - split - case inl hv => rw [Int.mul_assoc, Int.mul_comm (g i), ←Int.pow_succ] - exact ⟨k + 1, rfl⟩ - case inr _ => rw [Int.mul_one] - exact ⟨k, rfl⟩ - - --- theorem denote_eq {m n : Monomial} (h : ∀ ctx : Context, m.denote ctx = n.denote ctx) : m = n := by --- apply eq --- · sorry --- · induction m.vars, n.vars using List.rec with --- | nil nil => sorry --- | nil cons a b => sorry --- | cons a b nil => sorry --- | cons a b ih cons c d ih1 => sorry - - - - - -- · sorry - -- · apply List.ext_get - -- · sorry - -- · intro i h1 h2; - -- have h3 := h (fun j => if i = j then i else 1) - -- simp [denote] at h3 - -- sorry - end Monomial abbrev Polynomial := List Monomial @@ -194,10 +152,6 @@ where else n :: insert m ns -#eval add [⟨5, [0, 1]⟩, ⟨7, [0, 1, 1]⟩] [⟨3, [0, 1, 1]⟩, ⟨2, [0, 1]⟩] -#eval add [⟨3, [0, 1, 1]⟩, ⟨2, [0, 1]⟩] [⟨5, [0, 1]⟩, ⟨7, [0, 1, 1]⟩] - - def sub (p q : Polynomial) : Polynomial := p.add q.neg @@ -291,64 +245,6 @@ theorem denote_foldl {g : Monomial → Polynomial} : 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] --- #check Fin.mk --- theorem denote_cast {p : List Monomial} : --- denote ctx (List.foldl f [] p) = List.foldl (fun acc m => denote ctx (f [m] ⟨acc, []⟩)) 0 p := by --- induction p with --- | nil => simp [denote] --- | cons n p ih => --- simp only [List.foldl_cons] --- rw [← Int.add_zero (denote ctx (f [n] ⟨0, []⟩)), Monomial.foldl_assoc Int.add_assoc] - -theorem denote_ite {p : Polynomial} : denote (fun j => if j = i then 1 else 0) p = if h : i < p.length then Monomial.denote (fun _ => 1) (p.get ⟨i, h⟩) else 0:= by - induction p with - | nil => sorry - | cons n p ih => - split - case cons.inl h1 => - simp only [denote, List.foldl_cons, Int.add_comm 0, Monomial.foldl_assoc Int.add_assoc, Monomial.denote] - sorry - sorry - - -#check List.ext_get - -theorem denote_eq {p q : Polynomial} (h : ∀ ctx, p.denote ctx = q.denote ctx) : p = q := by - apply List.ext_get - · sorry - · intro i h1 h2 - have h' := h (fun j => if j = i then 1 else 0) - rw [denote_ite, denote_ite] at h' - simp [h1, h2, Monomial.denote] at h' - apply Monomial.eq - · sorry - · sorry - -theorem add_assoc :∀ (p q r : Polynomial), add (add p q) r = add p (add q r) := by - intro p q r; simp only [add]; revert p q - induction r with - | nil => sorry - | cons n r ih => - intro p q - induction q with - | nil => sorry - | cons => sorry - -theorem add_comm : ∀ (p q : Polynomial), add p q = add q p := by - intro p; simp only [add] - induction p with - | nil => sorry - | cons n p ih => - intro q - simp only [add, add.insert, List.foldr_cons, ih q] - induction q with - | nil => unfold add.insert - simp - sorry - | cons => sorry - - - theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q.denote ctx := by simp only [mul] induction p with From 42e616d2a765c0e0354beb088b60adfd8671a298 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:42:29 -0700 Subject: [PATCH 06/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index eda537db..37d87524 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -15,7 +15,6 @@ abbrev Var := Nat def Context := Var → Int structure Monomial where - mk :: coeff : Int vars : List Var deriving Inhabited, Repr From 5b92d622cccca47b86747a2bc1cc5edfcbb3a8b7 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:42:52 -0700 Subject: [PATCH 07/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 37d87524..80e3cb2d 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -97,7 +97,7 @@ 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] + | nil => rfl | 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] From c52b300e82de146c11f5e3750fedd37504513001 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:43:05 -0700 Subject: [PATCH 08/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 80e3cb2d..bfd911ed 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -233,9 +233,6 @@ theorem denote_add_insert {g : Monomial → Polynomial} : 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 From 1188519f6fe9cd6ecdc9f26e6c68a58209f35a94 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:43:28 -0700 Subject: [PATCH 09/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index bfd911ed..c755b0fe 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -247,8 +247,7 @@ theorem denote_mul {p q : Polynomial} : (p.mul q).denote ctx = p.denote ctx * q. | 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] + rw [denote_foldl, denote_add_insert, ←denote_mulMonomial, denote_nil_add, denote_foldl] end Polynomial From 69967d4657e6ba3fe4206c986fdca56629969855 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:44:19 -0700 Subject: [PATCH 10/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index c755b0fe..3d7698cc 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -83,11 +83,9 @@ theorem foldl_assoc {g : β → α} (z1 z2 : α) : 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 + induction l generalizing z1 z2 with + | nil => rfl | cons y ys ih => - intro z1 z2 simp only [List.foldr_cons, ih, assoc] From d87b0ddcb9bbaa2c5fb1e43cfc8e4920a77c92d2 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:44:34 -0700 Subject: [PATCH 11/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 3d7698cc..ff398f06 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -67,6 +67,7 @@ theorem eq : ∀ {m n : Monomial}, m.coeff = n.coeff → m.vars = n.vars → m = section + variable {op : α → α → α} (assoc : ∀ a b c, op (op a b) c = op a (op b c)) -- Can be generalized to `List.foldl_assoc`. From 0e9566dfe2c9c3ef36a217b3b89a58b90b7b5f8d Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:44:42 -0700 Subject: [PATCH 12/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index ff398f06..4285f437 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -60,12 +60,6 @@ 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 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)) From a91c734bf884965f974d98bb2c95fd13b77e1c26 Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 12 Aug 2024 16:44:51 -0700 Subject: [PATCH 13/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index 4285f437..b90bae26 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -68,11 +68,9 @@ variable {op : α → α → α} (assoc : ∀ a b c, op (op a b) c = op a (op b 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 + induction l generalizing z1 z2 with + | nil => rfl | cons y ys ih => - intro z1 z2 simp only [List.foldl_cons, ih, assoc] theorem foldr_assoc {g : β → α} (z1 z2 : α) : From 18c0649c11bad922cb8d65b185ac5bc7eb87955c Mon Sep 17 00:00:00 2001 From: Harun Khan <58151072+mhk119@users.noreply.github.com> Date: Mon, 30 Sep 2024 11:04:59 -0700 Subject: [PATCH 14/15] Update Smt/Reconstruct/Int/Polynorm.lean Co-authored-by: Abdalrhman Mohamed --- Smt/Reconstruct/Int/Polynorm.lean | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index b90bae26..fb6ea3dc 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -163,19 +163,13 @@ theorem foldl_add_insert (ctx : Context) : | 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] + 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 From 70d894d1148d3aefc0cf5d5e46cdef274c641a64 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 30 Sep 2024 11:27:22 -0700 Subject: [PATCH 15/15] requested changes --- Smt/Reconstruct/Int/Polynorm.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index fb6ea3dc..c612097f 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -81,20 +81,19 @@ theorem foldr_assoc {g : β → α} (z1 z2 : α) : | 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 => rfl + | 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] + 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