chore: update test

`congrArg` is not needed anymore.

src/Init/Grind/Tactics.lean

@@ -76,6 +76,12 @@ structure Config where
   /-- If `extAll` is `true`, `grind` uses any extensionality theorems available in the environment. -/
   extAll : Bool := false
   /--
+  If `etaStruct` is `true`, then for each term `t : S` such that `S` is a structure,
+  and is tagged with `[grind ext]`, `grind` adds the equation `t = ⟨t.1, ..., t.n⟩`
+  which holds by reflexivity. Moreover, the extensionality theorem for `S` is not used.
+  -/
+  etaStruct : Bool := true
+  /--
   If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
   on equalities between lambda expressions.
   -/

src/Lean/Meta/Tactic/Grind/ExtAttr.lean

@@ -19,8 +19,9 @@ builtin_initialize extTheoremsExt : SimpleScopedEnvExtension Name ExtTheorems
   }
 
 def validateExtAttr (declName : Name) : CoreM Unit := do
-  unless (← Ext.isExtTheorem declName) do
-    throwError "invalid `[grind ext]`, `{declName}` is not tagged with `[ext]`"
+  if !(← Ext.isExtTheorem declName) then
+  if !(isStructure (← getEnv) declName) then
+    throwError "invalid `[grind ext]`, `{declName}` is neither tagged with `[ext]` nor is a structure"
 
 def addExtAttr (declName : Name) (attrKind : AttributeKind) : CoreM Unit := do
   validateExtAttr declName

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -187,27 +187,34 @@ private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Un
           modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm }
 
 /--
-If type of `a` is an inductive datatype with one constructor `ctor` without fields,
-pushes the equality `a = ctor`.
+If type of `a` is a structure and is tagged with `[grind ext]` attribute,
+propagate `a = ⟨a.1, ..., a.n⟩`
 
-Remark: we added this feature because `isDefEq` implements it, and consequently
-the simplifier reduces terms of the form `a = ctor` to `True` using `eq_self`.
+This function subsumes the `propagateUnitLike` function we used in the past.
+Recall that the `propagateUnitLike` was added because `isDefEq` implements it,
+and consequently the simplifier reduces terms of the form `a = ctor` to `True` using `eq_self`.
 This `isDefEq` feature was negatively affecting `grind` until we added an
 equivalent one here. For example, when splitting on a `match`-expression
 using Unit-like types, equalites about these types were being reduced to `True`
 by `simp` (i.e., in the `grind` preprocessor), and `grind` would never see
 these facts.
 -/
-private def propagateUnitLike (a : Expr) (generation : Nat) : GoalM Unit := do
+private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
   let aType ← whnfD (← inferType a)
   matchConstStructureLike aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do
     unless a.isAppOf ctorVal.name do
-      if ctorVal.numFields == 0 then
+      -- TODO: remove ctorVal.numFields after update stage0
+      if (← isExtTheorem inductVal.name) || ctorVal.numFields == 0 then
         let params := aType.getAppArgs[:inductVal.numParams]
-        let unit := mkAppN (mkConst ctorVal.name us) params
-        let unit ← shareCommon unit
-        internalize unit generation
-        pushEq a unit <| (← mkEqRefl unit)
+        let mut ctorApp := mkAppN (mkConst ctorVal.name us) params
+        for j in [: ctorVal.numFields] do
+          let mut proj ← mkProjFn ctorVal us params j a
+          if (← isProof proj) then
+            proj ← markProof proj
+          ctorApp := mkApp ctorApp proj
+        ctorApp ← shareCommon ctorApp
+        internalize ctorApp generation
+        pushEq a ctorApp <| (← mkEqRefl a)
 
 /-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application. -/
 private def extParentsToIgnore (declName : Name) : Bool :=
@@ -284,82 +291,85 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
     Otherwise, it will not be able to propagate that `a + 1 = 1` when `a = 0`
     -/
     Arith.internalize e parent?
-    return ()
-  trace_goal[grind.internalize] "{e}"
-  propagateUnitLike e generation
-  match e with
-  | .bvar .. => unreachable!
-  | .sort .. => return ()
-  | .fvar .. =>
-    mkENode' e generation
-    checkAndAddSplitCandidate e
-  | .letE .. =>
-    mkENode' e generation
-  | .lam .. =>
-    addSplitCandidatesForFunext e generation parent?
-    mkENode' e generation
-  | .forallE _ d b _ =>
-    mkENode' e generation
-    internalizeImpl d generation e
-    registerParent e d
-    unless b.hasLooseBVars do
-      internalizeImpl b generation e
-      registerParent e b
-      addCongrTable e
-    if (← isProp d <&&> isProp e) then
-      propagateUp e
+  else
+    go
+    propagateEtaStruct e generation
+where
+  go : GoalM Unit := do
+    trace_goal[grind.internalize] "{e}"
+    match e with
+    | .bvar .. => unreachable!
+    | .sort .. => return ()
+    | .fvar .. =>
+      mkENode' e generation
       checkAndAddSplitCandidate e
-  | .lit .. =>
-    mkENode e generation
-  | .const declName _ =>
-    mkENode e generation
-    activateTheoremPatterns declName generation
-  | .mvar .. =>
-    if (← reportMVarInternalization) then
-      reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
-    mkENode' e generation
-  | .mdata .. =>
-    reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
-    mkENode' e generation
-  | .proj .. =>
-    reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
-    mkENode' e generation
-  | .app .. =>
-    if (← isLitValue e) then
-      -- We do not want to internalize the components of a literal value.
+    | .letE .. =>
+      mkENode' e generation
+    | .lam .. =>
+      addSplitCandidatesForFunext e generation parent?
+      mkENode' e generation
+    | .forallE _ d b _ =>
+      mkENode' e generation
+      internalizeImpl d generation e
+      registerParent e d
+      unless b.hasLooseBVars do
+        internalizeImpl b generation e
+        registerParent e b
+        addCongrTable e
+      if (← isProp d <&&> isProp e) then
+        propagateUp e
+        checkAndAddSplitCandidate e
+    | .lit .. =>
       mkENode e generation
-      Arith.internalize e parent?
-    else if e.isAppOfArity ``Grind.MatchCond 1 then
-      internalizeMatchCond e generation
-    else e.withApp fun f args => do
+    | .const declName _ =>
       mkENode e generation
-      updateAppMap e
-      checkAndAddSplitCandidate e
-      pushCastHEqs e
-      addMatchEqns f generation
-      if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
-        -- We only internalize the proposition. We can skip the proof because of
-        -- proof irrelevance
-        let c := args[0]!
-        internalizeImpl c generation e
-        registerParent e c
-      else if f.isConstOf ``ite && args.size == 5 then
-        let c := args[1]!
-        internalizeImpl c generation e
-        registerParent e c
-      else
-        if let .const fName _ := f then
-          activateTheoremPatterns fName generation
+      activateTheoremPatterns declName generation
+    | .mvar .. =>
+      if (← reportMVarInternalization) then
+        reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
+      mkENode' e generation
+    | .mdata .. =>
+      reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
+      mkENode' e generation
+    | .proj .. =>
+      reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
+      mkENode' e generation
+    | .app .. =>
+      if (← isLitValue e) then
+        -- We do not want to internalize the components of a literal value.
+        mkENode e generation
+        Arith.internalize e parent?
+      else if e.isAppOfArity ``Grind.MatchCond 1 then
+        internalizeMatchCond e generation
+      else e.withApp fun f args => do
+        mkENode e generation
+        updateAppMap e
+        checkAndAddSplitCandidate e
+        pushCastHEqs e
+        addMatchEqns f generation
+        if f.isConstOf ``Lean.Grind.nestedProof && args.size == 2 then
+          -- We only internalize the proposition. We can skip the proof because of
+          -- proof irrelevance
+          let c := args[0]!
+          internalizeImpl c generation e
+          registerParent e c
+        else if f.isConstOf ``ite && args.size == 5 then
+          let c := args[1]!
+          internalizeImpl c generation e
+          registerParent e c
         else
-          internalizeImpl f generation e
-        registerParent e f
-        for h : i in [: args.size] do
-          let arg := args[i]
-          internalize arg generation e
-          registerParent e arg
-      addCongrTable e
-      Arith.internalize e parent?
-      propagateUp e
-      propagateBetaForNewApp e
+          if let .const fName _ := f then
+            activateTheoremPatterns fName generation
+          else
+            internalizeImpl f generation e
+          registerParent e f
+          for h : i in [: args.size] do
+            let arg := args[i]
+            internalize arg generation e
+            registerParent e arg
+        addCongrTable e
+        Arith.internalize e parent?
+        propagateUp e
+        propagateBetaForNewApp e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean

@@ -13,6 +13,24 @@ import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind
 
+private unsafe def markNestedProofImpl (e : Expr) (visit : Expr → StateRefT (PtrMap Expr Expr) MetaM Expr)
+    : StateRefT (PtrMap Expr Expr) MetaM Expr := do
+  let prop ← inferType e
+  /-
+  We must unfold reducible constants occurring in `prop` because the congruence closure
+  module in `grind` assumes they have been expanded.
+  See `grind_mark_nested_proofs_bug.lean` for an example.
+  TODO: We may have to normalize `prop` too.
+  -/
+  let prop ← unfoldReducible prop
+  /- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
+  let prop ← Core.betaReduce prop
+  /- We must fold kernel projections like it is done in the preprocessor. -/
+  let prop ← foldProjs prop
+  /- We must mask proofs occurring in `prop` too. -/
+  let prop ← visit prop
+  return mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
+
 unsafe def markNestedProofsImpl (e : Expr) : MetaM Expr := do
   visit e |>.run' mkPtrMap
 where
@@ -22,21 +40,7 @@ where
         return e -- `e` is already marked
       if let some r := (← get).find? e then
         return r
-      let prop ← inferType e
-      /-
-      We must unfold reducible constants occurring in `prop` because the congruence closure
-      module in `grind` assumes they have been expanded.
-      See `grind_mark_nested_proofs_bug.lean` for an example.
-      TODO: We may have to normalize `prop` too.
-      -/
-      let prop ← unfoldReducible prop
-      /- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
-      let prop ← Core.betaReduce prop
-      /- We must fold kernel projections like it is done in the preprocessor. -/
-      let prop ← foldProjs prop
-      /- We must mask proofs occurring in `prop` too. -/
-      let prop ← visit prop
-      let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
+      let e' ← markNestedProofImpl e visit
       modify fun s => s.insert e e'
       return e'
     -- Remark: we have to process `Expr.proj` since we only
@@ -78,4 +82,13 @@ Recall that the congruence closure module has special support for `Lean.Grind.ne
 def markNestedProofs (e : Expr) : MetaM Expr :=
   unsafe markNestedProofsImpl e
 
+/--
+Given a proof `e`, mark it with `Lean.Grind.nestedProof`
+-/
+def markProof (e : Expr) : MetaM Expr := do
+  if e.isAppOf ``Lean.Grind.nestedProof then
+    return e -- `e` is already marked
+  else
+    unsafe markNestedProofImpl e markNestedProofsImpl.visit |>.run' mkPtrMap
+
 end Lean.Meta.Grind

tests/lean/grind/grind_congrArg.lean

@@ -6,6 +6,8 @@ private theorem getElem_qpartition_snd_of_hi_lt {n} (lt : α → α → Bool) (a
     (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
     (k : Nat) (h : hi < k) (h' : k < n) : (qpartition as lt lo hi hlo hhi).2[k] = as[k] := sorry
 
+attribute [grind ext] Subtype Prod -- TODO: remove after update stage0
+
 @[local grind] private theorem getElem_qsort_sort_of_hi_lt
     {n} (lt : α → α → Bool) (as : Vector α n) (lo hi : Nat)
     (hlo : lo < n) (hhi : hi < n) (w : lo ≤ hi)
@@ -13,9 +15,9 @@ private theorem getElem_qpartition_snd_of_hi_lt {n} (lt : α → α → Bool) (a
   fun_induction qsort.sort
   case case1 a b =>
     unfold qsort.sort
-    -- `grind` fails unless we uncomment the following two lines. I would hope it manages both!
-    -- have := congrArg (·.2) a
+    -- `grind` fails unless we uncomment the following line. I would hope it manages both!
     -- simp only [dif_pos, *]
+    simp only [a] -- It needs `a` to be manually unfolded
     grind [getElem_qpartition_snd_of_hi_lt]
   case case2 a b ih1 ih2 ih3 => sorry
   case case3 => sorry

tests/lean/run/grind_etaStruct.lean

@@ -0,0 +1,24 @@
+set_option grind.warning false
+
+opaque f (a : Nat) : Nat × Bool
+
+attribute [grind ext] Prod Subtype
+
+example (a b : Nat) : (f a).1 = (f b).1 → (f a).2 = (f b).2 → f a = f b := by
+  grind
+
+def g (a : Nat) : { x : Nat // x > 1 } :=
+  ⟨a+2, by grind⟩
+
+example (a b : Nat) : (g a).1 = (g b).1 → g a = g b := by
+  grind
+
+@[grind ext] structure S where
+  x : Nat
+  y : Int
+
+example (x y : S) : x.1 = y.1 → x.2 = y.2 → x = y := by
+  grind
+
+example {a b} (x : S) : x = ⟨a, b⟩ → x.1 = a := by
+  grind