fix: nondeterministic failure in grind (#6530)

This PR fixes nondeterministic failures in the (WIP) `grind` tactic.

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

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
 

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
 

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

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.

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)