From f66ca17b65bf485d3d42ad5267803556a308fa28 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Thu, 24 Aug 2023 11:08:45 +0300 Subject: [PATCH 1/7] tactic finished --- Smt/Reconstruction/Rewrites/Tactic.lean | 89 +++++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 Smt/Reconstruction/Rewrites/Tactic.lean diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean new file mode 100644 index 00000000..99c420bb --- /dev/null +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -0,0 +1,89 @@ +/- +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: Harun Khan +-/ + +import Lean +import Std +import Aesop + +open Lean Elab.Tactic Meta Expr Syntax + +namespace Smt.Data.tactic + +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] + +theorem bool_and_flatten : (xs ∧ (b ∧ ys) ∧ zs) = (xs ∧ b ∧ ys ∧ zs) := by + rw [← @and_assoc b ys zs] + +theorem bool_or_flatten : (xs ∨ (b ∨ ys) ∨ zs) = (xs ∨ b ∨ ys ∨ zs) := by + rw [← @or_assoc b ys zs] + +theorem bool_and_false : (xs ∧ False ∧ ys) = False := by rw [false_and, and_false] + +theorem bool_and_true : (xs ∧ True ∧ ys) = (xs ∧ ys) := by rw [true_and] + +theorem bool_and_dup : (xs ∧ b ∧ ys ∧ b ∧ zs) = (xs ∧ b ∧ ys ∧ zs) := by aesop + +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 + let n := arr.size + let mut mv' := mv + for i in [: n] do + let mut 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 + mv' ← mv'.replaceTargetEq r.eNew r.eqProof + let r ← mv'.rewrite (← mv'.getType) rule + mv' ← mv'.replaceTargetEq r.eNew r.eqProof + 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 + 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 + mv'.refl + +syntax inner := "[" term,* "]" +syntax outer := "[" inner,* "]" + +syntax (name := smt_rw) "smt_rw" ident ident ident outer : tactic + +def parseInner : TSyntax ``inner → TacticM (Array Expr) + | `(inner| [$ts,*]) => ts.getElems.mapM (elabTerm · none) + | _ => throwError "[inner]: wrong usage" + +def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr)) + | `(outer| [$is,*]) => is.getElems.mapM parseInner + | _ => throwError "[outer]: wrong usage" + +@[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] + +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]] + +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]] + +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]] + +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]] + +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]] From 9609de427e1028e0a04292aef4641b0a8bb2f61e Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Sun, 27 Aug 2023 14:17:41 +0300 Subject: [PATCH 2/7] included a hashmap --- Smt/Reconstruction/Rewrites/Tactic.lean | 30 +++++++++++++++---------- 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index 99c420bb..f35a5187 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -31,9 +31,16 @@ 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 if m > 1 then @@ -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,23 @@ 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 + let rr ← elabTerm stx[2] none + let xs ← parseOuter ⟨stx[3]⟩ + let op := stx[1].getId + smtRw mv op rr xs replaceMainGoal [mv] 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]] + smt_rw or bool_or_flatten [[x1, x2, x3], [b], [y1], [z1]] From 8035a9efe5e1bc3aecc5accafafc98f2643d4ee0 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 28 Aug 2023 22:19:15 +0300 Subject: [PATCH 3/7] added import --- Smt/Reconstruction/Certifying.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Smt/Reconstruction/Certifying.lean b/Smt/Reconstruction/Certifying.lean index 15831517..675859e1 100644 --- a/Smt/Reconstruction/Certifying.lean +++ b/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 From 23f2ee1fd11ee26cd54ac921a9094378b8e9efc5 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Mon, 28 Aug 2023 22:21:36 +0300 Subject: [PATCH 4/7] added the import --- Smt/Reconstruction/Rewrites/Tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index f35a5187..004be8b9 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -91,5 +91,5 @@ example : (x1 ∨ x2 ∨ x3 ∨ b ∨ y1 ∨ y2 ∨ b ∨ z1 ∨ z2 ∨ False) = example : (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ b ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by 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 +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]] From 6682d3e5b0441be142e7ef1524506768efc22ccc Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Sun, 3 Sep 2023 20:22:51 +0300 Subject: [PATCH 5/7] small suggested changes --- Smt/Reconstruction/Rewrites/Tactic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index 004be8b9..0aec3ddd 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -42,7 +42,7 @@ def smtRw (mv : MVarId) (op : Name) (rule : Expr) (arr : Array (Array Expr)) : M 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 @@ -52,7 +52,7 @@ def smtRw (mv : MVarId) (op : Name) (rule : Expr) (arr : Array (Array Expr)) : M 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 @@ -77,7 +77,6 @@ def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr)) let xs ← parseOuter ⟨stx[3]⟩ let op := stx[1].getId smtRw mv op rr xs - replaceMainGoal [mv] example : (x1 ∧ x2 ∧ x3 ∧ (b ∧ y1 ∧ y2 ∧ True) ∧ z1 ∧ z2 ∧ True) = (x1 ∧ x2 ∧ x3 ∧ b ∧ y1 ∧ y2 ∧ z1 ∧ z2 ∧ True) := by smt_rw and bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]] From e68f5f464db7422d5d4eb2e5f66ce34093722990 Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Sun, 3 Sep 2023 20:26:50 +0300 Subject: [PATCH 6/7] small suggested changes --- Smt/Reconstruction/Rewrites/Tactic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index 0aec3ddd..14b4a04e 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -78,6 +78,7 @@ def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr)) 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 bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]] From 1d5d0b99ed9553f3e22ce356e1775add408e1ecd Mon Sep 17 00:00:00 2001 From: Harun Khan Date: Sun, 3 Sep 2023 20:27:34 +0300 Subject: [PATCH 7/7] remove space --- Smt/Reconstruction/Rewrites/Tactic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Smt/Reconstruction/Rewrites/Tactic.lean b/Smt/Reconstruction/Rewrites/Tactic.lean index 14b4a04e..0aec3ddd 100644 --- a/Smt/Reconstruction/Rewrites/Tactic.lean +++ b/Smt/Reconstruction/Rewrites/Tactic.lean @@ -78,7 +78,6 @@ def parseOuter : TSyntax ``outer → TacticM (Array (Array Expr)) 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 bool_and_flatten [[x1, x2], [b], [y1, y2], [z1, z2]]