From eb670925cd95ae23a9cd0826c570944f042ee0b9 Mon Sep 17 00:00:00 2001
From: Harun Khan <58151072+mhk119@users.noreply.github.com>
Date: Thu, 6 Jun 2024 17:43:04 -0700
Subject: [PATCH] orN-resolution proof (#109)

* orN-proof

* re-adjustment

* small change

* fixed
---
 Smt/Reconstruct/Prop.lean        |   2 +-
 Smt/Reconstruct/Prop/Lemmas.lean | 112 ++++++++++++++++++++++++++++---
 2 files changed, 103 insertions(+), 11 deletions(-)

diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean
index 07489083..0278d9c6 100644
--- a/Smt/Reconstruct/Prop.lean
+++ b/Smt/Reconstruct/Prop.lean
@@ -233,7 +233,7 @@ def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (hps
       else .app q(@Eq.refl Prop) q($ps[$i])
     addThm (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) q(Prop.orN_resolution $hps $hqs $hi $hj $hij)
   else
-    addThm (← rightAssocOp q(Or) (c₁ ++ c₂)) q(Prop.orN_concat $hps $hqs)
+    addThm (← rightAssocOp q(Or) (c₁ ++ c₂)) q(@Prop.orN_append_left $ps $qs $hps)
 where
   rightAssocOp (op : Expr) (ts : Array cvc5.Term) : ReconstructM Expr := do
     if ts.isEmpty then
diff --git a/Smt/Reconstruct/Prop/Lemmas.lean b/Smt/Reconstruct/Prop/Lemmas.lean
index 33fc83a7..501af1b5 100644
--- a/Smt/Reconstruct/Prop/Lemmas.lean
+++ b/Smt/Reconstruct/Prop/Lemmas.lean
@@ -567,18 +567,110 @@ theorem negSymm {α : Type u} {a b : α} : a ≠ b → b ≠ a := λ h f => h (E
 
 theorem eq_not_not (p : Prop) : p = ¬¬p := propext (not_not.symm)
 
-theorem orN_concat (hps : orN ps) (hqs : orN qs) : orN (ps ++ qs) :=
-  match ps with
-  | []          => hqs
-  | [_]         => match qs with
-    | []     => hps
-    | _ :: _ => Or.inl hps
-  | _ :: _ :: _ => match hps with
-    | Or.inl hp  => Or.inl hp
-    | Or.inr hps => Or.inr (orN_concat hps hqs)
+theorem orN_cons : orN (t :: l) = (t ∨ orN l) := by
+  cases l with
+  | nil => simp [orN]
+  | cons t' l => simp [orN]
+
+theorem orN_eraseIdx (hj : j < qs.length) : (orN (qs.eraseIdx j) ∨ qs[j]) = (orN qs) := by
+  revert j
+  induction qs with
+  | nil =>
+    intro j hj
+    simp at hj; exfalso
+    exact not_succ_le_zero j hj
+  | cons t l ih =>
+    intro j hj
+    cases j with
+    | zero =>
+      simp only [eraseIdx_cons_zero, cons_getElem_zero, orN_cons, eraseIdx_cons_succ, cons_getElem_succ]
+      rw [or_comm]
+    | succ j =>
+      simp only [eraseIdx_cons_succ, cons_getElem_succ, orN_cons, eraseIdx, or_assoc]
+      congr
+      rw [@ih j (by rw [length_cons, succ_lt_succ_iff] at hj; exact hj)]
+
+def subList' (xs : List α) (i j : Nat) : List α :=
+  List.drop i (xs.take j)
+
+theorem orN_subList (hps : orN ps) (hpq : ps = subList' qs i j): orN qs := by
+  revert i j ps
+  induction qs with
+  | nil =>
+    intro ps i j hp hps
+    simp [subList', *] at *; assumption
+  | cons t l ih =>
+    simp only [subList'] at *
+    intro ps i j hp hps
+    rw [orN_cons]
+    cases j with
+    | zero =>
+      simp [*, orN] at *
+    | succ j =>
+      simp only [take_cons_succ] at hps
+      cases i with
+      | zero =>
+        simp only [hps, orN_cons, drop_zero] at hp
+        exact congOrLeft (fun hp => @ih (drop 0 (take j l)) 0 j (by simp [hp]) rfl) hp
+      | succ i =>
+        apply Or.inr
+        apply @ih ps i j hp
+        simp [hps]
+
+theorem length_take (h : n ≤ l.length) : (take n l).length = n := by
+  revert n
+  induction l with
+  | nil => intro n h; simp at h; simp [h]
+  | cons t l ih =>
+    intro n h
+    cases n with
+    | zero => simp
+    | succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
+
+theorem length_eraseIdx (h : i < l.length) : (eraseIdx l i).length = l.length -1 := by
+  revert i
+  induction l with
+  | nil => simp
+  | cons t l ih =>
+    intro i hi
+    cases i with
+    | zero => simp
+    | succ i =>
+      simp
+      rw [length_cons, succ_lt_succ_iff] at hi
+      rw [ih hi, Nat.succ_eq_add_one, Nat.sub_add_cancel (zero_lt_of_lt hi)]
+
+theorem take_append (a b : List α) : take a.length (a ++ b) = a := by
+  have H3:= take_append_drop a.length (a ++ b)
+  apply (append_inj H3 _).1
+  rw [length_take]
+  rw [length_append]
+  apply le_add_right
+
+theorem drop_append (a b : List α): drop a.length (a ++ b) = b := by
+  have H3:= take_append_drop a.length (a ++ b)
+  apply (append_inj H3 _).2
+  rw [length_take]
+  rw [length_append]
+  apply le_add_right
+
+theorem orN_append_left (hps : orN ps) : orN (ps ++ qs) := by
+  apply @orN_subList ps (ps ++ qs) 0 ps.length hps
+  simp [subList', take_append]
+
+theorem orN_append_right (hqs : orN qs) : orN (ps ++ qs) := by
+  apply @orN_subList qs (ps ++ qs) ps.length (ps.length + qs.length) hqs
+  simp only [←length_append, subList', take_length, drop_append]
 
 theorem orN_resolution (hps : orN ps) (hqs : orN qs) (hi : i < ps.length) (hj : j < qs.length) (hij : ps[i] = ¬qs[j]) : orN (ps.eraseIdx i ++ qs.eraseIdx j) := by
-  sorry
+  have H1 := orN_eraseIdx hj
+  have H2 := orN_eraseIdx hi
+  by_cases h : ps[i]
+  · simp only [eq_iff_iff, true_iff, iff_true, h, hqs, hij, hps] at *
+    apply orN_append_right (by simp [*] at *; exact H1)
+  · simp only [hps, hqs, h, eq_iff_iff, false_iff, not_not, iff_true, or_false,
+    not_false_eq_true] at *
+    apply orN_append_left H2
 
 theorem implies_of_not_and : ¬(andN' ps ¬q) → impliesN ps q := by
   induction ps with