chore: move test to run

src/Init/Grind/Ext.lean

@@ -9,4 +9,4 @@ prelude
 import Init.Ext
 import Init.Grind.Tactics
 
-attribute [grind ext] funext
+attribute [grind ext] funext Prod Subtype Sigma PSigma

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

@@ -35,7 +35,7 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   if proof'.hasMVar || prop'.hasMVar then
     reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
     return ()
-  trace[grind.ext] "{prop'}"
+  trace[grind.ext] "{thm.declName}: {prop'}"
   addNewRawFact proof' prop' ((← getGeneration e) + 1)
 
 end Lean.Meta.Grind

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

@@ -18,6 +18,13 @@ import Lean.Meta.Tactic.Grind.Arith.Internalize
 
 namespace Lean.Meta.Grind
 
+/--
+A lighter version of `preprocess` which produces a definitionally equal term,
+but ensures assumptions made by `grind` are satisfied.
+-/
+private def preprocessLight (e : Expr) : GoalM Expr := do
+  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedProofs (← unfoldReducible e))))))
+
 /-- Adds `e` to congruence table. -/
 def addCongrTable (e : Expr) : GoalM Unit := do
   if let some { e := e' } := (← get).congrTable.find? { e } then
@@ -114,9 +121,6 @@ private def pushCastHEqs (e : Expr) : GoalM Unit := do
   | f@Eq.recOn α a motive b h v => pushHEq e v (mkApp6 (mkConst ``Grind.eqRecOn_heq f.constLevels!) α a motive b h v)
   | _ => return ()
 
-private def preprocessGroundPattern (e : Expr) : GoalM Expr := do
-  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← unfoldReducible e)))))
-
 private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
   mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
 
@@ -130,7 +134,7 @@ where
     if pattern.isBVar || isPatternDontCare pattern then
       return pattern
     else if let some e := groundPattern? pattern then
-      let e ← preprocessGroundPattern e
+      let e ← preprocessLight e
       internalize e generation none
       return mkGroundPattern e
     else pattern.withApp fun f args => do
@@ -200,6 +204,7 @@ by `simp` (i.e., in the `grind` preprocessor), and `grind` would never see
 these facts.
 -/
 private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
+  unless (← getConfig).etaStruct do return ()
   let aType ← whnfD (← inferType a)
   matchConstStructureLike aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do
     unless a.isAppOf ctorVal.name do
@@ -212,7 +217,7 @@ private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do
           if (← isProof proj) then
             proj ← markProof proj
           ctorApp := mkApp ctorApp proj
-        ctorApp ← shareCommon ctorApp
+        ctorApp ← preprocessLight ctorApp
         internalize ctorApp generation
         pushEq a ctorApp <| (← mkEqRefl a)
 

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

@@ -22,13 +22,15 @@ private unsafe def markNestedProofImpl (e : Expr) (visit : Expr → StateRefT (P
   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
+  let prop ← unfoldReducible prop
   /- We must mask proofs occurring in `prop` too. -/
   let prop ← visit prop
+  let prop ← eraseIrrelevantMData prop
+  /- We must fold kernel projections like it is done in the preprocessor. -/
+  let prop ← foldProjs prop
+  let prop ← normalizeLevels prop
   return mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
 
 unsafe def markNestedProofsImpl (e : Expr) : MetaM Expr := do

tests/lean/run/grind_cat.lean

@@ -69,7 +69,10 @@ structure NatTrans [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F G : Fu
   /-- The naturality square for a given morphism. -/
   naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f := by grind
 
-attribute [grind ext] NatTrans.ext -- TODO: remove after builtin extensionality for structures
+-- In the following examples `[grind ext] NatTrans.ext` is more effective than
+-- `[grind ext] NatTrans` which only applies eta-extension because it will allows
+-- chaining with function extensionality
+attribute [grind ext] NatTrans.ext
 
 attribute [simp, grind =] NatTrans.naturality
 

tests/lean/run/grind_congrArg.lean

@@ -6,8 +6,6 @@ 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)
@@ -15,9 +13,6 @@ attribute [grind ext] Subtype Prod -- TODO: remove after update stage0
   fun_induction qsort.sort
   case case1 a b =>
     unfold qsort.sort
-    -- `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

@@ -2,8 +2,6 @@ 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
 

tests/lean/run/grind_t1.lean

@@ -337,17 +337,24 @@ example : (replicate n a).map f = replicate n (f a) := by
   fail_if_success grind -ext only [Option.map_some, Option.map_none, getElem?_map, getElem?_replicate]
   sorry
 
-@[ext] structure S where
+@[ext, grind ext] structure S where
   a : Nat
   b : Bool
 
-attribute [grind ext] S.ext
-
 example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
   grind
 
 example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
-  fail_if_success grind -ext
+  fail_if_success grind -etaStruct
+  sorry
+
+attribute [grind ext] S.ext -- enable extensionality using S.ext
+
+example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
+  grind -etaStruct -- It is applying the extensionality theorem instead of eta for structures
+
+example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
+  fail_if_success grind -etaStruct -ext
   sorry
 
 example (x : S) : x.a = 10 → false ≠ x.b → x = { a := 10, b := true } := by