feat: proof terms for grind ac (#10189)
This PR implements the proof terms for the new `grind ac` module.
Examples:
```lean
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
: op a (op b b) = op c d → op c (op d c) = op (op a b) (op b c) := by
grind only
example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d : α)
: op a (op b b) = op d c → op (op b a) (op b c) = op c (op d c) := by
grind only
example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op]
(one : α) [Std.LawfulIdentity op one] (a b c d : α)
: op a (op (op b one) b) = op d c → op (op b a) (op (op b one) c) = op (op c one) (op d c) := by
grind only
```
The `grind ac` module is not complete yet, we still need to implement
critical pair computation and fix the support for idempotent operators.
This commit is contained in:
Leonardo de Moura
GitHub
parent
f376fd87d0
commit
c4e5f57512
5 changed files with 224 additions and 39 deletions
|
|
@ -299,35 +299,82 @@ theorem Seq.denote_concat {α} (ctx : Context α) {inst₁ : Std.Associative ctx
|
|||
|
||||
attribute [local simp] Seq.denote_concat
|
||||
|
||||
theorem eq_orient {α} (ctx : Context α) (lhs rhs : Seq)
|
||||
: lhs.denote ctx = rhs.denote ctx → rhs.denote ctx = lhs.denote ctx := by
|
||||
simp_all
|
||||
|
||||
theorem eq_simp_lhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq)
|
||||
: lhs₁.denote ctx = rhs₁.denote ctx → lhs₁.denote ctx = rhs₂.denote ctx → rhs₁.denote ctx = rhs₂.denote ctx := by
|
||||
simp_all
|
||||
|
||||
theorem eq_simp_rhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq)
|
||||
: lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = lhs₁.denote ctx → lhs₂.denote ctx = rhs₁.denote ctx := by
|
||||
simp_all
|
||||
|
||||
theorem diseq_simp_lhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq)
|
||||
: lhs₁.denote ctx = rhs₁.denote ctx → lhs₁.denote ctx ≠ rhs₂.denote ctx → rhs₁.denote ctx ≠ rhs₂.denote ctx := by
|
||||
simp_all
|
||||
|
||||
theorem diseq_simp_rhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq)
|
||||
: lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ lhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₁.denote ctx := by
|
||||
simp_all
|
||||
|
||||
noncomputable def simp_prefix_cert (lhs rhs tail s s' : Seq) : Bool :=
|
||||
s.beq' (lhs.concat_k tail) |>.and' (s'.beq' (rhs.concat_k tail))
|
||||
|
||||
/--
|
||||
Given `lhs = rhs`, and a term `s := lhs * tail`, rewrite it to `s' := rhs * tail`
|
||||
-/
|
||||
theorem simp_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs tail s s' : Seq)
|
||||
: simp_prefix_cert lhs rhs tail s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
|
||||
simp [simp_prefix_cert]; intro _ _ h; subst s s'; simp [h]
|
||||
theorem eq_simp_lhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
|
||||
simp [simp_prefix_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem eq_simp_rhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
|
||||
simp [simp_prefix_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_lhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
|
||||
simp [simp_prefix_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_rhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
|
||||
simp [simp_prefix_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
noncomputable def simp_suffix_cert (lhs rhs head s s' : Seq) : Bool :=
|
||||
s.beq' (head.concat_k lhs) |>.and' (s'.beq' (head.concat_k rhs))
|
||||
|
||||
/--
|
||||
Given `lhs = rhs`, and a term `s := head * lhs`, rewrite it to `s' := head * rhs`
|
||||
-/
|
||||
theorem simp_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs head s s' : Seq)
|
||||
: simp_suffix_cert lhs rhs head s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
|
||||
simp [simp_suffix_cert]; intro _ _ h; subst s s'; simp [h]
|
||||
theorem eq_simp_lhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
|
||||
simp [simp_suffix_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem eq_simp_rhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
|
||||
simp [simp_suffix_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_lhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
|
||||
simp [simp_suffix_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_rhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
|
||||
simp [simp_suffix_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
noncomputable def simp_middle_cert (lhs rhs head tail s s' : Seq) : Bool :=
|
||||
s.beq' (head.concat_k (lhs.concat_k tail)) |>.and' (s'.beq' (head.concat_k (rhs.concat_k tail)))
|
||||
|
||||
/--
|
||||
Given `lhs = rhs`, and a term `s := head * lhs * tail`, rewrite it to `s' := head * rhs * tail`
|
||||
-/
|
||||
theorem simp_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs head tail s s' : Seq)
|
||||
: simp_middle_cert lhs rhs head tail s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
|
||||
simp [simp_middle_cert]; intro _ _ h; subst s s'; simp [h]
|
||||
theorem eq_simp_lhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
|
||||
simp [simp_middle_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem eq_simp_rhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
|
||||
simp [simp_middle_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_lhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
|
||||
simp [simp_middle_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_rhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
|
||||
simp [simp_middle_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
noncomputable def superpose_prefix_suffix_cert (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
|
||||
lhs₁.beq' (p.concat_k c) |>.and'
|
||||
|
|
@ -422,6 +469,22 @@ theorem simp_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst
|
|||
: simp_ac_cert c lhs rhs s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
|
||||
simp [simp_ac_cert]; intro _ _; subst s s'; simp; intro h; rw [h]
|
||||
|
||||
theorem eq_simp_lhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
|
||||
simp [simp_ac_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem eq_simp_rhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
|
||||
simp [simp_ac_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_lhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq)
|
||||
: simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
|
||||
simp [simp_ac_cert]; intros; subst lhs₂ lhs₂'; simp_all
|
||||
|
||||
theorem diseq_simp_rhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq)
|
||||
: simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
|
||||
simp [simp_ac_cert]; intros; subst rhs₂ rhs₂'; simp_all
|
||||
|
||||
noncomputable def superpose_ac_cert (a b c lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
|
||||
lhs₁.beq' (c.union_k a) |>.and'
|
||||
(lhs₂.beq' (c.union_k b)) |>.and'
|
||||
|
|
@ -505,6 +568,10 @@ theorem diseq_erase_dup {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_
|
|||
(lhs rhs lhs' rhs' : Seq) : eq_erase_dup_cert lhs rhs lhs' rhs' → lhs.denote ctx ≠ rhs.denote ctx → lhs'.denote ctx ≠ rhs'.denote ctx := by
|
||||
simp [eq_erase_dup_cert]; intro _ _; subst lhs' rhs'; simp
|
||||
|
||||
theorem diseq_erase0 {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)}
|
||||
(lhs rhs lhs' rhs' : Seq) : eq_erase0_cert lhs rhs lhs' rhs' → lhs.denote ctx ≠ rhs.denote ctx → lhs'.denote ctx ≠ rhs'.denote ctx := by
|
||||
simp [eq_erase0_cert]; intro _ _; subst lhs' rhs'; simp
|
||||
|
||||
noncomputable def diseq_unsat_cert (lhs rhs : Seq) : Bool :=
|
||||
lhs.beq' rhs
|
||||
|
||||
|
|
|
|||
|
|
@ -91,18 +91,18 @@ local macro "gen_cnstr_fns " cnstr:ident : command =>
|
|||
|
||||
private def $(mkId `simplifyLhsWithA) (c : $cnstr) (c' : EqCnstr) (r : AC.SubseqResult) : $cnstr :=
|
||||
match r with
|
||||
| .exact => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c c' }
|
||||
| .prefix s => { c with lhs := c'.rhs ++ s, h := .simp_prefix (lhs := true) s c c' }
|
||||
| .suffix s => { c with lhs := s ++ c'.rhs, h := .simp_suffix (lhs := true) s c c' }
|
||||
| .middle p s => { c with lhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := true) p s c c' }
|
||||
| .exact => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c' c }
|
||||
| .prefix s => { c with lhs := c'.rhs ++ s, h := .simp_prefix (lhs := true) s c' c }
|
||||
| .suffix s => { c with lhs := s ++ c'.rhs, h := .simp_suffix (lhs := true) s c' c }
|
||||
| .middle p s => { c with lhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := true) p s c' c }
|
||||
| .false => c
|
||||
|
||||
private def $(mkId `simplifyRhsWithA) (c : $cnstr) (c' : EqCnstr) (r : AC.SubseqResult) : $cnstr :=
|
||||
match r with
|
||||
| .exact => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c c' }
|
||||
| .prefix s => { c with rhs := c'.rhs ++ s, h := .simp_prefix (lhs := false) s c c' }
|
||||
| .suffix s => { c with rhs := s ++ c'.rhs, h := .simp_suffix (lhs := false) s c c' }
|
||||
| .middle p s => { c with rhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := false) p s c c' }
|
||||
| .exact => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c' c }
|
||||
| .prefix s => { c with rhs := c'.rhs ++ s, h := .simp_prefix (lhs := false) s c' c }
|
||||
| .suffix s => { c with rhs := s ++ c'.rhs, h := .simp_suffix (lhs := false) s c' c }
|
||||
| .middle p s => { c with rhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := false) p s c' c }
|
||||
| .false => c
|
||||
|
||||
/-- Simplifies `c` using the basis when `(← isCommutative)` is `false` -/
|
||||
|
|
@ -135,14 +135,14 @@ local macro "gen_cnstr_fns " cnstr:ident : command =>
|
|||
|
||||
private def $(mkId `simplifyLhsWithAC) (c : $cnstr) (c' : EqCnstr) (r : AC.SubsetResult) : $cnstr :=
|
||||
match r with
|
||||
| .exact => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c c' }
|
||||
| .strict s => { c with lhs := c'.rhs.union s, h := .simp_ac (lhs := true) s c c' }
|
||||
| .exact => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c' c }
|
||||
| .strict s => { c with lhs := c'.rhs.union s, h := .simp_ac (lhs := true) s c' c }
|
||||
| .false => c
|
||||
|
||||
private def $(mkId `simplifyRhsWithAC) (c : $cnstr) (c' : EqCnstr) (r : AC.SubsetResult) : $cnstr :=
|
||||
match r with
|
||||
| .exact => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c c' }
|
||||
| .strict s => { c with rhs := c'.rhs.union s, h := .simp_ac (lhs := false) s c c' }
|
||||
| .exact => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c' c }
|
||||
| .strict s => { c with rhs := c'.rhs.union s, h := .simp_ac (lhs := false) s c' c }
|
||||
| .false => c
|
||||
|
||||
/--
|
||||
|
|
@ -196,7 +196,7 @@ def saveDiseq (c : DiseqCnstr) : ACM Unit := do
|
|||
|
||||
def DiseqCnstr.assert (c : DiseqCnstr) : ACM Unit := do
|
||||
let c ← c.eraseDup
|
||||
-- let c ← c.simplify -- TODO: uncomment after implementing proof generation
|
||||
let c ← c.simplify
|
||||
trace[grind.ac.assert] "{← c.denoteExpr}"
|
||||
if c.lhs == c.rhs then
|
||||
c.setUnsat
|
||||
|
|
@ -306,8 +306,11 @@ private def getNext? : ACM (Option EqCnstr) := do
|
|||
return some c
|
||||
|
||||
private def checkDiseqs : ACM Unit := do
|
||||
-- TODO
|
||||
return ()
|
||||
let diseqs := (← getStruct).diseqs
|
||||
modifyStruct fun s => { s with diseqs := {} }
|
||||
for c in diseqs do
|
||||
c.assert
|
||||
if (← isInconsistent) then return
|
||||
|
||||
private def propagateEqs : ACM Unit := do
|
||||
-- TODO
|
||||
|
|
|
|||
|
|
@ -121,6 +121,51 @@ where
|
|||
go : ProofM Expr := do
|
||||
mkContext (← x)
|
||||
|
||||
partial def EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr := do caching c do
|
||||
match c.h with
|
||||
| .core a b lhs rhs =>
|
||||
let h ← match (← isCommutative), (← hasNeutral) with
|
||||
| false, false => mkAPrefix ``AC.eq_norm_a
|
||||
| false, true => mkAIPrefix ``AC.eq_norm_ai
|
||||
| true, false => mkACPrefix ``AC.eq_norm_ac
|
||||
| true, true => mkACIPrefix ``AC.eq_norm_aci
|
||||
return mkApp6 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← mkEqProof a b)
|
||||
| .erase_dup c₁ =>
|
||||
let h ← mkDupPrefix ``AC.eq_erase_dup
|
||||
return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
|
||||
| .erase0 c₁ =>
|
||||
let h ← mkAIPrefix ``AC.eq_erase0
|
||||
return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
|
||||
| .simp_exact isLhs c₁ c₂ =>
|
||||
let h ← mkPrefix <| if isLhs then ``AC.eq_simp_lhs_exact else ``AC.eq_simp_rhs_exact
|
||||
let o := if isLhs then c₂.rhs else c₂.lhs
|
||||
return mkApp5 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl o) (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_prefix isLhs tail c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_prefix else ``AC.eq_simp_rhs_prefix
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_suffix isLhs head c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_suffix else ``AC.eq_simp_rhs_suffix
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_middle isLhs head tail c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_middle else ``AC.eq_simp_rhs_middle
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp10 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_ac isLhs s c₁ c₂ =>
|
||||
let h ← mkACPrefix <| if isLhs then ``AC.eq_simp_lhs_ac else ``AC.eq_simp_rhs_ac
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl s) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .swap c =>
|
||||
let h ← mkPrefix ``AC.eq_orient
|
||||
return mkApp3 h (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) (← c.toExprProof)
|
||||
| .superpose_prefix .. => throwError "NIY"
|
||||
| .superpose_ac .. => throwError "NIY"
|
||||
|
||||
partial def DiseqCnstr.toExprProof (c : DiseqCnstr) : ProofM Expr := do caching c do
|
||||
match c.h with
|
||||
| .core a b lhs rhs =>
|
||||
|
|
@ -133,7 +178,33 @@ partial def DiseqCnstr.toExprProof (c : DiseqCnstr) : ProofM Expr := do caching
|
|||
| .erase_dup c₁ =>
|
||||
let h ← mkDupPrefix ``AC.diseq_erase_dup
|
||||
return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
|
||||
| _ => throwError "NIY"
|
||||
| .erase0 c₁ =>
|
||||
let h ← mkAIPrefix ``AC.diseq_erase0
|
||||
return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
|
||||
| .simp_exact isLhs c₁ c₂ =>
|
||||
let h ← mkPrefix <| if isLhs then ``AC.diseq_simp_lhs_exact else ``AC.diseq_simp_rhs_exact
|
||||
let o := if isLhs then c₂.rhs else c₂.lhs
|
||||
return mkApp5 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl o) (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_prefix isLhs tail c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_prefix else ``AC.diseq_simp_rhs_prefix
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_suffix isLhs head c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_suffix else ``AC.diseq_simp_rhs_suffix
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_middle isLhs head tail c₁ c₂ =>
|
||||
let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_middle else ``AC.diseq_simp_rhs_middle
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp10 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .simp_ac isLhs s c₁ c₂ =>
|
||||
let h ← mkACPrefix <| if isLhs then ``AC.diseq_simp_lhs_ac else ``AC.diseq_simp_rhs_ac
|
||||
let s' := if isLhs then c.lhs else c.rhs
|
||||
return mkApp9 h (← mkSeqDecl s) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
|
||||
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
|
||||
def DiseqCnstr.setUnsat (c : DiseqCnstr) : ACM Unit := do
|
||||
let h ← withProofContext do
|
||||
|
|
|
|||
|
|
@ -61,11 +61,11 @@ inductive DiseqCnstrProof where
|
|||
| core (a b : Expr) (ea eb : AC.Expr)
|
||||
| erase_dup (c : DiseqCnstr)
|
||||
| erase0 (c : DiseqCnstr)
|
||||
| simp_exact (lhs : Bool) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
|
||||
| simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
|
||||
| simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
|
||||
| simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
|
||||
| simp_middle (lhs : Bool) (s₁ s₂ : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
|
||||
| simp_exact (lhs : Bool) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
| simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
| simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
| simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
| simp_middle (lhs : Bool) (s₁ s₂ : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
end
|
||||
|
||||
structure Struct where
|
||||
|
|
|
|||
44
tests/lean/run/grind_ac_2.lean
Normal file
44
tests/lean/run/grind_ac_2.lean
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
|
||||
: op a (op b b) = c → op c c = op (op a b) (op b c) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
|
||||
: op a (op b b) = c → op (op a b) (op b c) = op c c := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
|
||||
: op a (op b b) = c → op (op c a) (op b b) = op c c := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
|
||||
: op a (op b b) = c → op c c = op (op c a) (op b b) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
|
||||
: op a (op b b) = op c d → op c (op d c) = op (op a b) (op b c) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
|
||||
: op a (op b b) = op c d → op (op a b) (op b c) = op (op c d) c := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
|
||||
: op a (op b b) = op c d → op c (op c (op d c)) = op (op c a) (op b (op b c)) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
|
||||
: op a (op b b) = op c d → op (op c a) (op b (op b c)) = op c (op c (op d c)) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d : α)
|
||||
: op a (op b b) = op d c → op c (op d c) = op (op b a) (op b c) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d : α)
|
||||
: op a (op b b) = op d c → op (op b a) (op b c) = op c (op d c) := by
|
||||
grind only
|
||||
|
||||
example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op]
|
||||
(one : α) [Std.LawfulIdentity op one] (a b c d : α)
|
||||
: op a (op (op b one) b) = op d c → op (op b a) (op (op b one) c) = op (op c one) (op d c) := by
|
||||
grind only
|
||||
Loading…
Add table
Reference in a new issue