Some orN lemmas and proof of orN_resolution

Smt/Reconstruct/Prop/Lemmas.lean

@@ -2,7 +2,7 @@
 Copyright (c) 2021-2023 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: Tomaz Gomes Mascarenhas
+Authors: Tomaz Gomes Mascarenhas, Harun Khan
 -/
 
 import Lean
@@ -575,4 +575,109 @@ syntax "smtIte" (term)? (term)? (term)? (term)? : term
 macro_rules
 | `(smtIte $cond $t $e $type) => `(term| @ite $type $cond (propDecidable $cond) $t $e)
 
+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
+  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
+
 end Smt.Reconstruct.Prop