Utilize FFI to reconstruct cvc5 proofs in Lean.

Smt/Reconstruct.lean

@@ -5,11 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
-import Smt.Reconstruct.Arith
+-- import Smt.Reconstruct.Arith
 import Smt.Reconstruct.Builtin
 import Smt.Reconstruct.Options
 import Smt.Reconstruct.Prop
 import Smt.Reconstruct.Quant
+import Smt.Reconstruct.Reconstruct
 import Smt.Reconstruct.Rewrite
 import Smt.Reconstruct.Timed
 import Smt.Reconstruct.UF

Smt/Reconstruct/Builtin/Rewrites.lean

@@ -13,7 +13,7 @@ namespace Smt.Reconstruct.Builtin
 
 theorem ite_true_cond : ite True x y = x := rfl
 theorem ite_false_cond : ite False x y = y := rfl
-theorem ite_not_cond [h : Decidable c] : ite (Not c) x y = ite c y x :=
+theorem ite_not_cond [h : Decidable c] : ite (¬c) x y = ite c y x :=
   h.byCases (fun hc => if_pos hc ▸ if_neg (not_not_intro hc) ▸ rfl)
             (fun hnc => if_pos hnc ▸ if_neg hnc ▸ rfl)
 theorem ite_eq_branch [h : Decidable c] : ite c x x = x :=
@@ -25,10 +25,10 @@ theorem ite_then_lookahead [h : Decidable c] : ite c (ite c x y) z = ite c x z :
 theorem ite_else_lookahead [h : Decidable c] : ite c x (ite c y z) = ite c x z :=
   h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
             (fun hc => if_neg hc ▸ if_neg hc ▸ if_neg hc ▸ rfl)
-theorem ite_then_neg_lookahead [h : Decidable c] : ite c (ite (Not c) x y) z = ite c y z :=
+theorem ite_then_neg_lookahead [h : Decidable c] : ite c (ite (¬c) x y) z = ite c y z :=
   h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ ite_not_cond (c := c) ▸ if_pos hc ▸ rfl)
             (fun hc => if_neg hc ▸ if_neg hc ▸ rfl)
-theorem ite_else_neg_lookahead [h : Decidable c] : ite c x (ite (Not c) y z) = ite c x y :=
+theorem ite_else_neg_lookahead [h : Decidable c] : ite c x (ite (¬c) y z) = ite c x y :=
   h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
             (fun hc => if_neg hc ▸ if_neg hc ▸ ite_not_cond (c := c) ▸ if_neg hc ▸ rfl)
 

Smt/Reconstruct/Prop/Core.lean

@@ -0,0 +1,39 @@
+/-
+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
+-/
+
+import Std.Logic
+
+/- abbrev Implies (p q : Prop) := p → q -/
+
+inductive XOr (p q : Prop) : Prop where
+  | inl : p → ¬q → XOr p q
+  | inr : ¬p → q → XOr p q
+
+theorem XOr.elim {p q r : Prop} (h : XOr p q) (h₁ : p → ¬q → r) (h₂ : ¬p → q → r) : r := match h with
+  | inl hp hnq => h₁ hp hnq
+  | inr hnp hq => h₂ hnp hq
+
+theorem XOr.symm (h : XOr p q) : XOr q p := h.elim (flip inr) (flip inl)
+
+@[macro_inline] instance [dp : Decidable p] [dq : Decidable q] : Decidable (XOr p q) :=
+  match dp with
+  | isTrue   hp =>
+    match dq with
+    | isTrue   hq => isFalse (·.elim (fun _ hnq => hnq hq) (fun hnp _ => hnp hp))
+    | isFalse hnq => isTrue (.inl hp hnq)
+  | isFalse hnp =>
+    match dq with
+    | isTrue   hq => isTrue (.inr hnp hq)
+    | isFalse hnq => isFalse (·.elim (fun hp _ => hnp hp) (fun _ hq => hnq hq))
+
+namespace Smt.Reconstruct.Prop
+
+theorem and_assoc_eq : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)) := by simp [and_assoc]
+
+theorem or_assoc_eq : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c)) := by simp [or_assoc]
+
+end Smt.Reconstruct.Prop

Smt/Reconstruct/Prop/Lemmas.lean

@@ -8,6 +8,7 @@ Authors: Tomaz Gomes Mascarenhas
 import Lean
 import Std
 
+import Smt.Reconstruct.Prop.Core
 import Smt.Reconstruct.Options
 import Smt.Reconstruct.Util
 
@@ -16,8 +17,6 @@ namespace Smt.Reconstruct.Prop
 open Lean Elab.Tactic Meta Expr Syntax
 open Nat List Classical
 
-/- abbrev Implies (p q : Prop) := p → q -/
-
 theorem notImplies1 : ∀ {P Q : Prop}, ¬ (P → Q) → P := by
   intros P Q h
   cases Classical.em P with
@@ -63,37 +62,53 @@ theorem notEquivElim2 : ∀ {P Q : Prop}, ¬ (Eq P Q) → ¬ P ∨ ¬ Q := by
   | Or.inl p, Or.inl q =>
     absurd (propext (Iff.intro (λ _ => q) (λ _ => p))) h
 
-theorem iteElim1 : ∀ {c a b : Prop}, ite c a b → ¬ c ∨ a := by
-  intros c a b h
-  cases Classical.em c with
-  | inl hc => have r: ite c a b = a := if_pos hc
-              rewrite [r] at h
-              exact Or.inr h
-  | inr hnc => exact Or.inl hnc
-
-theorem iteElim2 : ∀ {c a b : Prop}, ite c a b → c ∨ b := by
-  intros c a b h
-  cases Classical.em c with
-  | inl hc => exact Or.inl hc
-  | inr hnc => have r: ite c a b = b := if_neg hnc
-               rewrite [r] at h
-               exact Or.inr h
-
-theorem notIteElim1 : ∀ {c a b : Prop}, ¬ ite c a b → ¬ c ∨ ¬ a := by
-  intros c a b h
-  cases Classical.em c with
-  | inl hc  => have r : ite c a b = a := if_pos hc
-               rewrite [r] at h
-               exact Or.inr h
-  | inr hnc => exact Or.inl hnc
-
-theorem notIteElim2 : ∀ {c a b : Prop}, ¬ ite c a b → c ∨ ¬ b := by
-  intros c a b h
-  cases Classical.em c with
-  | inl hc => exact Or.inl hc
-  | inr hnc => have r : ite c a b = b := if_neg hnc
-               rewrite [r] at h
-               exact Or.inr h
+theorem xorElim1 (h : XOr p q) : p ∨ q :=
+  match h with
+  | .inl hp _ => Or.inl hp
+  | .inr _ hq => Or.inr hq
+
+theorem xorElim2 (h : XOr p q) : ¬p ∨ ¬q :=
+  match h with
+  | .inl _ hnq => Or.inr hnq
+  | .inr hnp _ => Or.inl hnp
+
+theorem notXorElim1 (h : ¬XOr p q) : p ∨ ¬q :=
+  match Classical.em p, Classical.em q with
+  | Or.inl hp, _ => Or.inl hp
+  | _, Or.inr hnq => Or.inr hnq
+  | Or.inr hnp, Or.inl hq =>
+    absurd (.inr hnp hq) h
+
+theorem notXorElim2 (h : ¬XOr p q) : ¬p ∨ q :=
+  match Classical.em p, Classical.em q with
+  | Or.inr hnp, _ => Or.inl hnp
+  | _, Or.inl hq => Or.inr hq
+  | Or.inl hp, Or.inr hnq =>
+    absurd (.inl hp hnq) h
+
+theorem iteElim1 [hc : Decidable c] : ite c a b → ¬ c ∨ a := by
+  intros h
+  cases hc with
+  | isTrue hc   => exact Or.inr h
+  | isFalse hnc => exact Or.inl hnc
+
+theorem iteElim2 [hc : Decidable c] : ite c a b → c ∨ b := by
+  intros h
+  cases hc with
+  | isTrue hc   => exact Or.inl hc
+  | isFalse hnc => exact Or.inr h
+
+theorem notIteElim1 [hc : Decidable c] : ¬ ite c a b → ¬ c ∨ ¬ a := by
+  intros h
+  cases hc with
+  | isTrue hc   => exact Or.inr h
+  | isFalse hnc => exact Or.inl hnc
+
+theorem notIteElim2 [hc : Decidable c] : ¬ ite c a b → c ∨ ¬ b := by
+  intros h
+  cases hc with
+  | isTrue hc   => exact Or.inl hc
+  | isFalse hnc => exact Or.inr h
 
 theorem contradiction : ∀ {P : Prop}, P → ¬ P → False := λ p np => np p
 
@@ -314,102 +329,92 @@ theorem cnfImpliesNeg2 : ∀ {p q : Prop}, (p → q) ∨ ¬ q := by
   intros hnnq _
   exact notNotElim hnnq
 
-theorem cnfEquivPos1 : ∀ {p q : Prop}, ¬ (Eq p q) ∨ ¬ p ∨ q := by
+theorem cnfEquivPos1 : ∀ {p q : Prop}, p ≠ q ∨ ¬ p ∨ q := by
   intros _ _
   apply orImplies
   exact equivElim1 ∘ notNotElim
 
-theorem cnfEquivPos2 : ∀ {p q : Prop}, ¬ (Eq p q) ∨ p ∨ ¬ q := by
+theorem cnfEquivPos2 : ∀ {p q : Prop}, p ≠ q ∨ p ∨ ¬ q := by
   intros _ _
   apply orImplies
   exact equivElim2 ∘ notNotElim
 
-theorem cnfEquivNeg1 : ∀ {p q : Prop}, Eq p q ∨ p ∨ q := by
+theorem cnfEquivNeg1 : ∀ {p q : Prop}, p = q ∨ p ∨ q := by
   intros _ _
   apply orImplies
   exact notEquivElim1
 
-theorem cnfEquivNeg2 : ∀ {p q : Prop}, Eq p q ∨ ¬ p ∨ ¬ q := by
+theorem cnfEquivNeg2 : ∀ {p q : Prop}, p = q ∨ ¬ p ∨ ¬ q := by
   intros _ _
   apply orImplies
   exact notEquivElim2
 
-theorem cnfItePos1 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ ¬ c ∨ a := by
-  intros c a b
+theorem cnfXorPos1 : ¬(XOr p q) ∨ p ∨ q :=
+  orImplies (xorElim1 ∘ notNotElim)
+
+theorem cnfXorPos2 : ¬(XOr p q) ∨ ¬p ∨ ¬q :=
+  orImplies (xorElim2 ∘ notNotElim)
+
+theorem cnfXorNeg1 : (XOr p q) ∨ ¬p ∨ q :=
+  orImplies notXorElim2
+
+theorem cnfXorNeg2 : (XOr p q) ∨ p ∨ ¬q :=
+  orImplies notXorElim1
+
+theorem cnfItePos1 [h : Decidable c] : ¬ (ite c a b) ∨ ¬ c ∨ a := by
   apply orImplies
   intro hite
   have hite' := notNotElim hite
-  match Classical.em c with
-  | Or.inl hc  => have r: (if c then a else b) = a := if_pos hc
-                  rewrite [r] at hite'
-                  exact Or.inr hite'
-  | Or.inr hnc => exact Or.inl hnc
+  match h with
+  | isTrue _    => exact Or.inr hite'
+  | isFalse hnc => exact Or.inl hnc
 
-theorem cnfItePos2 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ c ∨ b   := by
-  intros c a b
+theorem cnfItePos2 [h : Decidable c] : ¬ (ite c a b) ∨ c ∨ b := by
   apply orImplies
   intro hite
   have hite' := notNotElim hite
-  match Classical.em c with
-  | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc
-                  rewrite [r] at hite'
-                  exact Or.inr hite'
-  | Or.inl hc  => exact Or.inl hc
+  match h with
+  | isFalse _ => exact Or.inr hite'
+  | isTrue hc => exact Or.inl hc
 
-theorem cnfItePos3 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ a ∨ b   := by
-  intros c a b
+theorem cnfItePos3 [h : Decidable c] : ¬ (ite c a b) ∨ a ∨ b := by
   apply orImplies
   intro hite
   have hite' := notNotElim hite
-  match Classical.em c with
-  | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc
-                  rewrite [r] at hite'
-                  exact Or.inr hite'
-  | Or.inl hc  => have r: (if c then a else b) = a := if_pos hc
-                  rewrite [r] at hite'
-                  exact Or.inl hite'
-
-theorem cnfIteNeg1 : ∀ {c a b : Prop}, (ite c a b) ∨ ¬ c ∨ ¬ a := by
-  intros c a b
+  match h with
+  | isFalse _ => exact Or.inr hite'
+  | isTrue _  => exact Or.inl hite'
+
+theorem cnfIteNeg1 [h : Decidable c] : (ite c a b) ∨ ¬ c ∨ ¬ a := by
   apply orImplies
   intro hnite
-  match Classical.em c with
-  | Or.inl hc  => have r: (if c then a else b) = a := if_pos hc
-                  rewrite [r] at hnite
-                  exact Or.inr hnite
-  | Or.inr hnc => exact Or.inl hnc
+  match h with
+  | isTrue _    => exact Or.inr hnite
+  | isFalse hnc => exact Or.inl hnc
 
-theorem cnfIteNeg2 : ∀ {c a b : Prop}, (ite c a b) ∨ c ∨ ¬ b   := by
-  intros c a b
+theorem cnfIteNeg2 [h : Decidable c] : (ite c a b) ∨ c ∨ ¬ b   := by
   apply orImplies
   intro hnite
-  match Classical.em c with
-  | Or.inr hnc  => have r: (if c then a else b) = b := if_neg hnc
-                   rewrite [r] at hnite
-                   exact Or.inr hnite
-  | Or.inl hc => exact Or.inl hc
+  match h with
+  | isFalse _ => exact Or.inr hnite
+  | isTrue hc => exact Or.inl hc
 
-theorem cnfIteNeg3 : ∀ {c a b : Prop}, (ite c a b) ∨ ¬ a ∨ ¬ b := by
-  intros c a b
+theorem cnfIteNeg3 [h : Decidable c] : (ite c a b) ∨ ¬ a ∨ ¬ b := by
   apply orImplies
   intro hnite
-  match Classical.em c with
-  | Or.inr hnc  => have r: (if c then a else b) = b := if_neg hnc
-                   rewrite [r] at hnite
-                   exact Or.inr hnite
-  | Or.inl hc => have r: (if c then a else b) = a := if_pos hc
-                 rewrite [r] at hnite
-                 exact Or.inl hnite
+  match h with
+  | isFalse _ => exact Or.inr hnite
+  | isTrue _  => exact Or.inl hnite
 
 theorem iteIntro {α : Type u} {c : Prop} {t e : α} : ite c ((ite c t e) = t) ((ite c t e) = e) := by
   match Classical.em c with
   | Or.inl hc  => rw [if_pos hc, if_pos hc]
   | Or.inr hnc => rw [if_neg hnc, if_neg hnc]
 
-theorem congrIte {α : Type u} : ∀ {c₁ c₂ : Prop} {t₁ t₂ e₁ e₂ : α} ,
+theorem congrIte [Decidable c₁] [Decidable c₂] {t₁ t₂ e₁ e₂ : α} :
     c₁ = c₂ → t₁ = t₂ → e₁ = e₂ → ite c₁ t₁ e₁ = ite c₂ t₂ e₂ := by
-  intros c₁ c₂ t₁ t₂ e₁ e₂ h₁ h₂ h₃
-  rw [h₁, h₂, h₃]
+  intros h₁ h₂ h₃
+  simp only [h₁, h₂, h₃]
 
 theorem congrHAdd {α β γ : Type} [HAdd α β γ] : ∀ {a₁ a₂ : α} {b₁ b₂ : β},
     a₁ = a₂ → b₁ = b₂ → a₁ + b₁ = a₂ + b₂ := by

Smt/Reconstruct/Prop/Resolution.lean

@@ -73,15 +73,12 @@ def resolutionCoreMeta (val₁ val₂ pivot : Expr) (sufIdx₁' sufIdx₂' : Opt
   let len₂ := sufIdx₂ + 1
   let lenGoal := len₁ + len₂ - 2
   let prefixLength := len₁ - 2
-
   if flipped then
     let tmp := pivot
     pivot := notPivot
     notPivot := tmp
-
   let pulled₁ ← pullCore pivot val₁ type₁ sufIdx₁'
   let pulled₂ ← pullCore notPivot val₂ type₂ sufIdx₂'
-
   let props₁ ← collectPropsInOrChain' sufIdx₁ type₁
   let props₁ := props₁.erase pivot
   let props₂ ← collectPropsInOrChain' sufIdx₂ type₂