diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 53f5373b46..f85093b5df 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -73,5 +73,6 @@ builtin_initialize registerTraceClass `grind.debug.offset.proof builtin_initialize registerTraceClass `grind.debug.ematch.pattern builtin_initialize registerTraceClass `grind.debug.beta builtin_initialize registerTraceClass `grind.debug.matchCond +builtin_initialize registerTraceClass `grind.debug.matchCond.lambda end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index 1ab00bbdef..9d1d852826 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Ctor import Lean.Meta.Tactic.Grind.Util import Lean.Meta.Tactic.Grind.Beta import Lean.Meta.Tactic.Grind.Internalize +import Lean.Meta.Tactic.Grind.Simp namespace Lean.Meta.Grind @@ -233,18 +234,19 @@ private def popNextEq? : GoalM (Option NewEq) := do modify fun s => { s with newEqs := s.newEqs.pop } return r -private partial def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do - addEqStep lhs rhs proof isHEq - processTodo -where - processTodo : GoalM Unit := do +private def processNewEqs : GoalM Unit := do + repeat if (← isInconsistent) then resetNewEqs return () checkSystem "grind" - let some { lhs, rhs, proof, isHEq } := (← popNextEq?) | return () + let some { lhs, rhs, proof, isHEq } := (← popNextEq?) + | return () addEqStep lhs rhs proof isHEq - processTodo + +private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do + addEqStep lhs rhs proof isHEq + processNewEqs /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/ private def addEq (lhs rhs proof : Expr) : GoalM Unit := do @@ -309,4 +311,56 @@ where def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do add (← fvarId.getType) (mkFVar fvarId) generation +/-- +Helper function for executing `x` with a fresh `newEqs` and without modifying +the goal state. + -/ +private def withoutModifyingState (x : GoalM α) : GoalM α := do + let saved ← get + modify fun goal => { goal with newEqs := {} } + try + x + finally + set saved + +/-- +If `e` has not been internalized yet, simplify it, and internalize the result. +-/ +private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do + if (← alreadyInternalized e) then + return { expr := e } + else + let r ← simp e + internalize r.expr gen + return r + +/-- +Try to construct a proof that `lhs = rhs` using the information in the +goal state. If `lhs` and `rhs` have not been internalized, this function +will internalize then, process propagated equalities, and then check +whether they are in the same equivalence class or not. +The goal state is not modified by this function. +This function mainly relies on congruence closure, and constraint +propagation. It will not perform case analysis. +-/ +def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do + if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then + if (← isEqv lhs rhs) then + return some (← mkEqProof lhs rhs) + else + return none + else withoutModifyingState do + let lhs ← simpAndInternalize lhs + let rhs ← simpAndInternalize rhs + processNewEqs + unless (← isEqv lhs.expr rhs.expr) do return none + unless (← hasSameType lhs.expr rhs.expr) do return none + let h ← mkEqProof lhs.expr rhs.expr + let h ← match lhs.proof?, rhs.proof? with + | none, none => pure h + | none, some h₂ => mkEqTrans h (← mkEqSymm h₂) + | some h₁, none => mkEqTrans h₁ h + | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂) + return some h + end Lean.Meta.Grind diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index 0a0a966de2..0d457d82dc 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Grind.Types import Lean.Meta.Tactic.Grind.Intro import Lean.Meta.Tactic.Grind.DoNotSimp import Lean.Meta.Tactic.Grind.MatchCond +import Lean.Meta.Tactic.Grind.Core namespace Lean.Meta.Grind namespace EMatch @@ -270,13 +271,20 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w return () -- Apply assignment for h : i in [:mvars.size] do - let v := c.assignment[numParams - i - 1]! + let mut v := c.assignment[numParams - i - 1]! unless isSameExpr v unassigned do let mvarId := mvars[i].mvarId! let mvarIdType ← mvarId.getType let vType ← inferType v - unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do + let report : M Unit := do reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}" + unless (← isDefEq mvarIdType vType) do + let some heq ← proveEq? vType mvarIdType + | report + return () + v ← mkAppM ``cast #[heq, v] + unless (← mvarId.checkedAssign v) do + report return () -- Synthesize instances for mvar in mvars, bi in bis do diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 356a491406..89f6a446f3 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -133,6 +133,7 @@ private partial def internalizeMatchCond (matchCond : Expr) (generation : Nat) : lhss.forM fun lhs => do internalize lhs generation; registerParent matchCond lhs propagateUp matchCond internalize e' generation + trace[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}" pushEq matchCond e' (← mkEqRefl matchCond) partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do