Smt rw tac: Added the import to Smt.Reconstruction.Certifying

Smt/Reconstruction/Certifying.lean

@@ -11,3 +11,4 @@ import Smt.Reconstruction.Certifying.Arith
 import Smt.Reconstruction.Rewrites.Arith
 import Smt.Reconstruction.Rewrites.Builtin
 import Smt.Reconstruction.Rewrites.Prop
+import Smt.Reconstruction.Rewrites.Tactic

Smt/Reconstruction/Rewrites/Tactic.lean

@@ -31,11 +31,18 @@ theorem bool_and_dup : (xs ∧ b ∧ ys ∧ b ∧ zs) = (xs ∧ b ∧ ys ∧ zs)
 
 theorem bool_or_dup : (xs ∨ b ∨ ys ∨ b ∨ zs) = (xs ∨ b ∨ ys ∨ zs) := by aesop
 
-def smtRw (mv : MVarId) (assoc : Expr) (null : Expr) (rule : Expr) (arr : Array (Array Expr)) : MetaM Unit := do
+def opsAssocNull : Name → Array Expr
+|  ``or => #[Expr.const ``or_assoc_eq [], Expr.const ``or_false []]
+| ``and => #[Expr.const ``and_assoc_eq [], Expr.const ``and_true []]
+| _ => #[]
+
+def smtRw (mv : MVarId) (op : Name) (rule : Expr) (arr : Array (Array Expr)) : MetaM Unit := do
   let n := arr.size
   let mut mv' := mv
+  let assoc := (opsAssocNull op)[0]!
+  let null := (opsAssocNull op)[1]!
   for i in [: n] do
-    let mut m := arr[i]!.size
+    let m := arr[i]!.size
     if m > 1 then
       for j in [: m-1] do
         let r ← mv'.rewrite (← mv'.getType) (mkAppN assoc #[arr[i]![m-j-2]!]) true
@@ -45,7 +52,7 @@ def smtRw (mv : MVarId) (assoc : Expr) (null : Expr) (rule : Expr) (arr : Array
   if let some r ← observing? (mv'.rewrite (← mv'.getType) null) then
     mv' ← mv'.replaceTargetEq r.eNew r.eqProof
   for i in [: n] do
-    let mut m := arr[i]!.size
+    let m := arr[i]!.size
     for j in [: m-1] do
       let some r ← observing? (mv'.rewrite (← mv'.getType) (.app assoc arr[i]![j]!)) | break
       mv' ← mv'.replaceTargetEq r.eNew r.eqProof
@@ -54,7 +61,7 @@ def smtRw (mv : MVarId) (assoc : Expr) (null : Expr) (rule : Expr) (arr : Array
 syntax inner := "[" term,* "]"
 syntax outer := "[" inner,* "]"
 
-syntax (name := smt_rw) "smt_rw" ident ident ident outer : tactic
+syntax (name := smt_rw) "smt_rw" ident ident outer : tactic
 
 def parseInner : TSyntax ``inner → TacticM (Array Expr)
   | `(inner| [$ts,*]) => ts.getElems.mapM (elabTerm · none)
@@ -66,24 +73,22 @@ def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr))
 
 @[tactic smt_rw] def evalSMTRw : Tactic := fun stx => do
   let mv : MVarId ← getMainGoal
-  let rr ← elabTerm stx[3] none
-  let xs ← parseOuter ⟨stx[4]⟩
-  let op  ← elabTermForApply stx[1]
-  let nu  ← elabTermForApply stx[2]
-  smtRw mv op nu rr xs
-  replaceMainGoal [mv]
+  let rr ← elabTerm stx[2] none
+  let xs ← parseOuter ⟨stx[3]⟩
+  let op := stx[1].getId
+  smtRw mv op rr xs
 
 example : (x1 ∧ x2 ∧ x3 ∧ (b ∧ y1 ∧ y2 ∧ True) ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]]
+  smt_rw and bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]]
 
 example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_dup [[x1, x2, x3], [y1, y2], [z1, z2]]
+  smt_rw and bool_and_dup[[x1, x2, x3], [y1, y2], [z1, z2]]
 
 example : (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ b ∨ z1 ∨ z2 ∨ False) = (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ z1 ∨ z2 ∨ False) := by
-  smt_rw or_assoc_eq or_false bool_or_dup [[x1, x2, x3], [y1, y2], [z1, z2]]
+  smt_rw or bool_or_dup [[x1, x2, x3], [y1, y2], [z1, z2]]
 
 example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by
-  smt_rw and_assoc_eq and_true bool_and_dup [[x1, x2, x3], [y1, y2], [z1, z2]]
+  smt_rw and bool_and_dup [[x1, x2, x3], [y1, y2], [z1, z2]]
 
-example : (x1 ∨ x2 ∨ x3 ∨ (b ∨  y1 ∨ False) ∨ z1 ∨ False) = (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ z1 ∨ False) := by
-  smt_rw or_assoc_eq or_false bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]]
+example : (x1 ∨ x2 ∨ x3 ∨ (b ∨  y1 ∨ False) ∨ z1 ∨ False)= (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ z1 ∨ False) := by
+  smt_rw or bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]]