From 2b09600e26a312ac7f7a2941b1739217c968b9fd Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Tue, 16 Apr 2024 18:11:06 +0200 Subject: [PATCH] Undo sparse explanations introduced in 7ba9316ecfe007dbe12affaba4dec8d7ebb03f1d --- Lean/Egg/Core/Explanation/Basic.lean | 2 +- Lean/Egg/Core/Explanation/Proof.lean | 63 +++++++++------------------- Lean/Egg/Tests/Int.lean | 2 +- 3 files changed, 21 insertions(+), 46 deletions(-) diff --git a/Lean/Egg/Core/Explanation/Basic.lean b/Lean/Egg/Core/Explanation/Basic.lean index 9c81924..fa8ca74 100644 --- a/Lean/Egg/Core/Explanation/Basic.lean +++ b/Lean/Egg/Core/Explanation/Basic.lean @@ -34,7 +34,7 @@ inductive Expression where deriving Inhabited structure Step extends Rewrite.Info where - dst : Option Expression + dst : Expression deriving Inhabited end Explanation diff --git a/Lean/Egg/Core/Explanation/Proof.lean b/Lean/Egg/Core/Explanation/Proof.lean index 90d41fa..a6addf8 100644 --- a/Lean/Egg/Core/Explanation/Proof.lean +++ b/Lean/Egg/Core/Explanation/Proof.lean @@ -3,8 +3,6 @@ import Egg.Core.Explanation.Congr import Egg.Core.Rewrites open Lean Meta --- TODO: Simplify tracing by adding `MessageData` instances for relevant types. - namespace Egg.Explanation private partial def replaceSubexprs @@ -100,17 +98,17 @@ def proof (expl : Explanation) (cgr : Congr) (rws : Rewrites) (amb : AmbientMVar for step in steps, idx in [:steps.size] do withTraceNode `egg.reconstruction (fun _ => return s!"Step {idx}") do trace[egg.reconstruction] step.src.description - trace[egg.reconstruction] ← step.dst.mapM (·.toExpr) + trace[egg.reconstruction] ← step.dst.toExpr unless ← isDefEq cgr.lhs current do throwError s!"{errorPrefix} initial expression is not defeq to lhs of proof goal" let mut proof ← mkEqRefl current for step in steps, idx in [:steps.size] do - let next? ← step.dst.mapM (·.toExpr) - let (stepEq, next) ← do + let next ← step.dst.toExpr + let stepEq ← do withTraceNode `egg.reconstruction (fun _ => return m!"Step {idx}") do trace[egg.reconstruction] m!"Current: {current}" - trace[egg.reconstruction] m!"Next: {next?}" - proofStep current next? step.toInfo + trace[egg.reconstruction] m!"Next: {next}" + proofStep current next step.toInfo proof ← mkEqTrans proof stepEq current := next checkFinalProof proof current steps @@ -120,53 +118,30 @@ def proof (expl : Explanation) (cgr : Congr) (rws : Rewrites) (amb : AmbientMVar where errorPrefix := "egg failed to reconstruct proof:" - proofStep (current : Expr) (next? : Option Expr) (rwInfo : Rewrite.Info) : - MetaM (Expr × Expr) := do - if rwInfo.src.isDefEq then - if let some next := next? - then return (← mkReflStep current next rwInfo.src, next) - else throwError s!"{errorPrefix} defeq steps in sparse explanations aren't supported yet" + proofStep (current next : Expr) (rwInfo : Rewrite.Info) : MetaM Expr := do + if rwInfo.src.isDefEq then return ← mkReflStep current next rwInfo.src let some rw := rws.find? rwInfo.src | throwError s!"{errorPrefix} unknown rewrite" - if ← isRflProof rw.proof then - if let some next := next? then - return (← mkReflStep current next rwInfo.src, next) - mkCongrStep current next? rwInfo.pos (← rw.forDir rwInfo.dir) + if ← isRflProof rw.proof then return ← mkReflStep current next rwInfo.src + mkCongrStep current next rwInfo.pos (← rw.forDir rwInfo.dir) mkReflStep (current next : Expr) (src : Source) : MetaM Expr := do unless ← isDefEq current next do throwError s!"{errorPrefix} unification failure for proof by reflexivity with rw {src.description}" mkEqRefl next - mkCongrStep (current : Expr) (next? : Option Expr) (pos : SubExpr.Pos) (rw : Rewrite) : - MetaM (Expr × Expr) := do + mkCongrStep (current next : Expr) (pos : SubExpr.Pos) (rw : Rewrite) : MetaM Expr := do let mvc := (← getMCtx).mvarCounter - let (lhs, rhs) ← placeCHoles current next? pos rw - try - let proof ← (← mkCongrOf 0 mvc lhs rhs).eq - let next := next?.getD (← unwrapHole rhs pos) - return (proof, next) - catch err => - throwError m!"{errorPrefix} 'mkCongrOf' failed with\n {err.toMessageData}" - - unwrapHole (expr : Expr) (pos : SubExpr.Pos) : MetaM Expr := - replaceSubexpr (root := expr) (p := pos) fun h => - if let some (_, val, _) := cHole? h - then return val - else throwError "{errorPrefix} expected to find congr-hole but didn't" + let (lhs, rhs) ← placeCHoles current next pos rw + try (← mkCongrOf 0 mvc lhs rhs).eq + catch err => throwError m!"{errorPrefix} 'mkCongrOf' failed with\n {err.toMessageData}" - placeCHoles (current : Expr) (next? : Option Expr) (pos : SubExpr.Pos) (rw : Rewrite) : - MetaM (Expr × Expr) := do - replaceSubexprs (root₁ := current) (root₂ := next?.getD current) (p := pos) fun lhs rhs => do + placeCHoles (current next : Expr) (pos : SubExpr.Pos) (rw : Rewrite) : MetaM (Expr × Expr) := do + replaceSubexprs (root₁ := current) (root₂ := next) (p := pos) fun lhs rhs => do -- It's necessary that we create the fresh rewrite (that is, create the fresh mvars) in *this* -- local context as otherwise the mvars can't unify with variables under binders. let rw ← rw.fresh unless ← isDefEq lhs rw.lhs do throwError "{errorPrefix} unification failure for LHS of rewrite" - let rhs ← - if next?.isSome then - unless ← isDefEq rhs rw.rhs do throwError "{errorPrefix} unification failure for RHS of rewrite" - pure rhs - else - pure rw.rhs + unless ← isDefEq rhs rw.rhs do throwError "{errorPrefix} unification failure for RHS of rewrite" let proof ← rw.eqProof return ( ← mkCHole (forLhs := true) lhs proof, @@ -174,9 +149,9 @@ where ) checkFinalProof (proof : Expr) (current : Expr) (steps : Array Step) : MetaM Unit := do - if let some last := steps.back?.map (·.dst) |>.getD (some expl.start) then - unless ← isDefEq current (← last.toExpr) do - throwError s!"{errorPrefix} final expression is not defeq to rhs of proof goal" + let last := steps.back?.map (·.dst) |>.getD expl.start + unless ← isDefEq current (← last.toExpr) do + throwError s!"{errorPrefix} final expression is not defeq to rhs of proof goal" let proof ← instantiateMVars proof for mvar in (proof.collectMVars {}).result do unless amb.contains mvar do throwError s!"{errorPrefix} final proof contains mvar {mvar.name}" diff --git a/Lean/Egg/Tests/Int.lean b/Lean/Egg/Tests/Int.lean index 9ab560f..814c696 100644 --- a/Lean/Egg/Tests/Int.lean +++ b/Lean/Egg/Tests/Int.lean @@ -1,5 +1,5 @@ import Egg -import Std +import Std.Data.Int.Lemmas example (a b c d : Int) : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by egg [Int.sub_mul, Int.sub_sub, Int.add_comm, Int.mul_comm, Int.one_mul]