From a5b1ed906c867d56b6e595fd74e2aff6852c0463 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Jan 2025 22:40:32 +0100 Subject: [PATCH] fix: nondeterministic failure in `grind` (#6530) This PR fixes nondeterministic failures in the (WIP) `grind` tactic. --- src/Lean/Meta/Tactic/Grind.lean | 1 + src/Lean/Meta/Tactic/Grind/Canon.lean | 40 ++++++-------- src/Lean/Meta/Tactic/Grind/Core.lean | 5 +- src/Lean/Meta/Tactic/Grind/ForallProp.lean | 3 + .../Meta/Tactic/Grind/MarkNestedProofs.lean | 55 +++++++++++-------- src/Lean/Meta/Tactic/Grind/Util.lean | 11 +++- 6 files changed, 64 insertions(+), 51 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 11b15243e263..01ee792bbec6 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -47,5 +47,6 @@ builtin_initialize registerTraceClass `grind.debug.proof builtin_initialize registerTraceClass `grind.debug.proj builtin_initialize registerTraceClass `grind.debug.parent builtin_initialize registerTraceClass `grind.debug.final +builtin_initialize registerTraceClass `grind.debug.forallPropagator end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index c895dd639a73..05057121709c 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -111,22 +111,13 @@ unsafe def canonImpl (e : Expr) : StateT State MetaM Expr := do visit e |>.run' mkPtrMap where visit (e : Expr) : StateRefT (PtrMap Expr Expr) (StateT State MetaM) Expr := do - match e with - | .bvar .. => unreachable! - -- Recall that `grind` treats `let`, `forall`, and `lambda` as atomic terms. - | .letE .. | .forallE .. | .lam .. - | .const .. | .lit .. | .mvar .. | .sort .. | .fvar .. - -- Recall that the `grind` preprocessor uses the `foldProjs` preprocessing step. - | .proj .. - -- Recall that the `grind` preprocessor uses the `eraseIrrelevantMData` preprocessing step. - | .mdata .. => return e - -- We only visit applications - | .app .. => - -- Check whether it is cached - if let some r := (← get).find? e then - return r - e.withApp fun f args => do - let e' ← if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then + unless e.isApp || e.isForall do return e + -- Check whether it is cached + if let some r := (← get).find? e then + return r + let e' ← match e with + | .app .. => e.withApp fun f args => do + if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then let prop := args[0]! let prop' ← visit prop if let some r := (← getThe State).proofCanon.find? prop' then @@ -149,12 +140,17 @@ where args := args.set! i arg' modified := true pure <| if modified then mkAppN f args else e - modify fun s => s.insert e e' - return e' - -/-- -Canonicalizes nested types, type formers, and instances in `e`. --/ + | .forallE _ d b _ => + -- Recall that we have `ForallProp.lean`. + let d' ← visit d + -- Remark: users may not want to convert `p → q` into `¬p ∨ q` + let b' ← if b.hasLooseBVars then pure b else visit b + pure <| e.updateForallE! d' b' + | _ => unreachable! + modify fun s => s.insert e e' + return e' + +/-- Canonicalizes nested types, type formers, and instances in `e`. -/ def canon (e : Expr) : StateT State MetaM Expr := unsafe canonImpl e diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index ce63088c7fbb..635e7aef85e9 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -41,7 +41,8 @@ This is an auxiliary function performed while merging equivalence classes. private def removeParents (root : Expr) : GoalM ParentSet := do let parents ← getParentsAndReset root for parent in parents do - if (← isCongrRoot parent) then + -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean` + if (← pure parent.isApp <&&> isCongrRoot parent) then trace[grind.debug.parent] "remove: {parent}" modify fun s => { s with congrTable := s.congrTable.erase { e := parent } } return parents @@ -52,7 +53,7 @@ This is an auxiliary function performed while merging equivalence classes. -/ private def reinsertParents (parents : ParentSet) : GoalM Unit := do for parent in parents do - if (← isCongrRoot parent) then + if (← pure parent.isApp <&&> isCongrRoot parent) then trace[grind.debug.parent] "reinsert: {parent}" addCongrTable parent diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean index 9228fe671309..9993f0e50e2d 100644 --- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean +++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean @@ -17,13 +17,16 @@ If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `pr -/ def propagateForallProp (parent : Expr) : GoalM Unit := do let .forallE n p q bi := parent | return () + trace[grind.debug.forallPropagator] "{parent}" unless (← isEqTrue p) do return () + trace[grind.debug.forallPropagator] "isEqTrue, {parent}" let h₁ ← mkEqTrueProof p let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁) let r ← simp qh₁ let q := mkLambda n bi p q let q' := r.expr internalize q' (← getGeneration parent) + trace[grind.debug.forallPropagator] "q': {q'} for{indentExpr parent}" let h₂ ← r.getProof let h := mkApp5 (mkConst ``Lean.Grind.forall_propagator) p q q' h₁ h₂ pushEq parent q' h diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean index 485bd0a35c7d..85d2d8fa8cb4 100644 --- a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean +++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean @@ -24,30 +24,37 @@ where let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e modify fun s => s.insert e e' return e' - else match e with - | .bvar .. => unreachable! - -- See comments on `Canon.lean` for why we do not visit these cases. - | .letE .. | .forallE .. | .lam .. - | .const .. | .lit .. | .mvar .. | .sort .. | .fvar .. => return e - | .proj _ _ b => return e.updateProj! (← visit b) - | .mdata _ b => return e.updateMData! (← visit b) - -- We only visit applications - | .app .. => - -- Check whether it is cached - if let some r := (← get).find? e then - return r - e.withApp fun f args => do - let mut modified := false - let mut args := args - for i in [:args.size] do - let arg := args[i]! - let arg' ← visit arg - unless ptrEq arg arg' do - args := args.set! i arg' - modified := true - let e' := if modified then mkAppN f args else e - modify fun s => s.insert e e' - return e' + -- Remark: we have to process `Expr.proj` since we only + -- fold projections later during term internalization + unless e.isApp || e.isForall || e.isProj do + return e + -- Check whether it is cached + if let some r := (← get).find? e then + return r + let e' ← match e with + | .app .. => e.withApp fun f args => do + let mut modified := false + let mut args := args + for i in [:args.size] do + let arg := args[i]! + let arg' ← visit arg + unless ptrEq arg arg' do + args := args.set! i arg' + modified := true + if modified then + pure <| mkAppN f args + else + pure e + | .proj _ _ b => + pure <| e.updateProj! (← visit b) + | .forallE _ d b _ => + -- Recall that we have `ForallProp.lean`. + let d' ← visit d + let b' ← if b.hasLooseBVars then pure b else visit b + pure <| e.updateForallE! d' b' + | _ => unreachable! + modify fun s => s.insert e e' + return e' /-- Wrap nested proofs `e` with `Lean.Grind.nestedProof`-applications. diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean index bf7bdabc5817..0805b4dd7fb8 100644 --- a/src/Lean/Meta/Tactic/Grind/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Util.lean @@ -100,12 +100,14 @@ def _root_.Lean.MVarId.clearAuxDecls (mvarId : MVarId) : MetaM MVarId := mvarId. /-- In the `grind` tactic, during `Expr` internalization, we don't expect to find `Expr.mdata`. This function ensures `Expr.mdata` is not found during internalization. -Recall that we do not internalize `Expr.forallE` and `Expr.lam` components. +Recall that we do not internalize `Expr.lam` children. +Recall that we still have to process `Expr.forallE` because of `ForallProp.lean`. +Moreover, we may not want to reduce `p → q` to `¬p ∨ q` when `(p q : Prop)`. -/ def eraseIrrelevantMData (e : Expr) : CoreM Expr := do let pre (e : Expr) := do match e with - | .letE .. | .lam .. | .forallE .. => return .done e + | .letE .. | .lam .. => return .done e | .mdata _ e => return .continue e | _ => return .continue e Core.transform e (pre := pre) @@ -116,11 +118,14 @@ Converts nested `Expr.proj`s into projection applications if possible. def foldProjs (e : Expr) : MetaM Expr := do let post (e : Expr) := do let .proj structName idx s := e | return .done e - let some info := getStructureInfo? (← getEnv) structName | return .done e + let some info := getStructureInfo? (← getEnv) structName | + trace[grind.issues] "found `Expr.proj` but `{structName}` is not marked as structure{indentExpr e}" + return .done e if h : idx < info.fieldNames.size then let fieldName := info.fieldNames[idx] return .done (← mkProjection s fieldName) else + trace[grind.issues] "found `Expr.proj` with invalid field index `{idx}`{indentExpr e}" return .done e Meta.transform e (post := post)