chore: remove noise

src/Init/Grind/Tactics.lean

@@ -70,6 +70,11 @@ structure Config where
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems available in the environment. -/
   ext : Bool := true
+  /--
+  If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
+  on equalities between lambda expressions.
+  -/
+  funext : Bool := true
   /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
   verbose : Bool := true
   /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/

src/Lean/Meta/Tactic/Grind.lean

@@ -52,6 +52,8 @@ builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
 builtin_initialize registerTraceClass `grind.beta
 builtin_initialize registerTraceClass `grind.mbtc
+builtin_initialize registerTraceClass `grind.ext
+builtin_initialize registerTraceClass `grind.ext.candidate
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -76,5 +78,6 @@ builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
 builtin_initialize registerTraceClass `grind.debug.ematch.activate
 builtin_initialize registerTraceClass `grind.debug.appMap
+builtin_initialize registerTraceClass `grind.debug.ext
 
 end Lean

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

@@ -35,6 +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'}"
   addNewRawFact proof' prop' ((← getGeneration e) + 1)
 
 end Lean.Meta.Grind

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

@@ -207,6 +207,65 @@ private def propagateUnitLike (a : Expr) (generation : Nat) : GoalM Unit := do
         internalize unit generation
         pushEq a unit <| (← mkEqRefl unit)
 
+/-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application. -/
+private def extParentsToIgnore (declName : Name) : Bool :=
+  declName == ``Eq || declName == ``HEq || declName == ``dite || declName == ``ite
+  || declName == ``Exists || declName == ``Subtype
+
+/--
+Given a term `e` that occurs as the argument at position `i` of an `f`-application `parent?`,
+we consider `e` as a candidate for case-splitting. For every other argument `e'` that also appears
+at position `i` in an `f`-application and has the same type as `e`, we add the case-split candidate `e = e'`.
+
+When performing the case split, we consider the following two cases:
+- `e = e'`, which may introduce a new congruence between the corresponding `f`-applications.
+- `¬(e = e')`, which may trigger extensionality theorems for the type of `e`.
+
+This feature enables `grind` to solve examples such as:
+```lean
+example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
+  grind
+```
+-/
+private def addSplitCandidatesForExt (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
+  let some parent := parent? | return ()
+  unless parent.isApp do return ()
+  let f := parent.getAppFn
+  if let .const declName _ := f then
+    if extParentsToIgnore declName then return ()
+  let type ← inferType e
+  -- Remark: we currently do not perform function extensionality on functions that produce a type that is not a proposition.
+  -- We may add an option to enable that in the future.
+  let u? ← typeFormerTypeLevel type
+  if u? != .none && u? != some .zero then return ()
+  let mut i  := parent.getAppNumArgs
+  let mut it := parent
+  repeat
+    if !it.isApp then return ()
+    i := i - 1
+    let arg := it.appArg!
+    if isSameExpr arg e then
+      found f i type
+    it := it.appFn!
+where
+  found (f : Expr) (i : Nat) (type : Expr) : GoalM Unit := do
+    trace[grind.debug.ext] "{f}, {i}, {e}"
+    let others := (← get).termsAt.find? (f, i) |>.getD []
+    for (e', type') in others do
+      if (← withDefault <| isDefEq type type') then
+        let eq := mkApp3 (mkConst ``Eq [← getLevel type]) type e e'
+        let eq ← shareCommon eq
+        internalize eq generation
+        trace_goal[grind.ext.candidate] "{eq}"
+        addSplitCandidate eq
+    modify fun s => { s with termsAt := s.termsAt.insert (f, i) ((e, type) :: others) }
+    return ()
+
+/-- Applies `addSplitCandidatesForExt` if `funext` is enabled. -/
+private def addSplitCandidatesForFunext (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
+  unless (← getConfig).funext do return ()
+  addSplitCandidatesForExt e generation parent?
+
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then
@@ -229,7 +288,10 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
   | .fvar .. =>
     mkENode' e generation
     checkAndAddSplitCandidate e
-  | .letE .. | .lam .. =>
+  | .letE .. =>
+    mkENode' e generation
+  | .lam .. =>
+    addSplitCandidatesForFunext e generation parent?
     mkENode' e generation
   | .forallE _ d b _ =>
     mkENode' e generation

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

@@ -529,6 +529,13 @@ structure Goal where
   arith      : Arith.State := {}
   /-- State of the clean name generator. -/
   clean      : Clean.State := {}
+  /--
+  Mapping from pairs `(f, i)` to a list of `(e, type)`.
+  The meaning is: `e : type` is lambda expression that occurs at argument `i` of an `f`-application.
+  We use this information to add case-splits for triggering extensionality theorems.
+  See `addSplitCandidatesForExt`.
+  -/
+  termsAt    : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

tests/lean/grind/clear_aux_decls.lean

@@ -250,19 +250,16 @@ def normalize (l : AList (fun _ : Nat => Bool)) :
   | .ite (var v)      t e =>
     match h : l.lookup v with
     | none =>
-      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
-      have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
+      have ⟨t', _⟩ := normalize (l.insert v true) t
+      have ⟨e', _⟩ := normalize (l.insert v false) e
       ⟨if t' = e' then t' else .ite (var v) t' e', by
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · -- eval = eval
           simp only [apply_ite, eval_ite_var]
           cases hfv : f v
           · simp_all
-            congr
-            ◾
-          · simp [h, ht₁]
-            congr
             ◾
+          · ◾
         · -- normalized
           split
           · ◾

tests/lean/run/grind_bintree.lean

@@ -0,0 +1,128 @@
+set_option grind.warning false
+reset_grind_attrs%
+
+attribute [grind] List.append_assoc List.cons_append List.nil_append
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+  deriving Repr
+
+def Tree.contains (t : Tree β) (k : Nat) : Bool :=
+  match t with
+  | leaf => false
+  | node left key _ right =>
+    if k < key then
+      left.contains k
+    else if key < k then
+      right.contains k
+    else
+      true
+
+def Tree.find? (t : Tree β) (k : Nat) : Option β :=
+  match t with
+  | leaf => none
+  | node left key value right =>
+    if k < key then
+      left.find? k
+    else if key < k then
+      right.find? k
+    else
+      some value
+
+def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
+  match t with
+  | leaf => node leaf k v leaf
+  | node left key value right =>
+    if k < key then
+      node (left.insert k v) key value right
+    else if key < k then
+      node left key value (right.insert k v)
+    else
+      node left k v right
+
+def Tree.toList (t : Tree β) : List (Nat × β) :=
+  match t with
+  | leaf => []
+  | node l k v r => l.toList ++ [(k, v)] ++ r.toList
+
+def Tree.toListTR (t : Tree β) : List (Nat × β) :=
+  go t []
+where
+  go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
+    match t with
+    | leaf => acc
+    | node l k v r => go l ((k, v) :: go r acc)
+
+theorem Tree.toList_eq_toListTR (t : Tree β)
+        : t.toList = t.toListTR := by
+  simp [toListTR, go t []]
+where
+  go (t : Tree β) (acc : List (Nat × β))
+     : toListTR.go t acc = t.toList ++ acc := by
+    induction t generalizing acc <;> grind [toListTR.go, toList]
+
+@[csimp] theorem Tree.toList_eq_toListTR_csimp
+                 : @Tree.toList = @Tree.toListTR := by
+  grind [toList_eq_toListTR]
+
+inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
+  | leaf : ForallTree p .leaf
+  | node :
+     ForallTree p left →
+     p key value →
+     ForallTree p right →
+     ForallTree p (.node left key value right)
+
+inductive BST : Tree β → Prop
+  | leaf : BST .leaf
+  | node :
+     ForallTree (fun k _ => k < key) left →
+     ForallTree (fun k _ => key < k) right →
+     BST left → BST right →
+     BST (.node left key value right)
+
+attribute [local simp, grind] Tree.insert
+
+theorem Tree.forall_insert_of_forall
+        (h₁ : ForallTree p t) (h₂ : p key value)
+        : ForallTree p (t.insert key value) := by
+  induction h₁ <;> grind [ForallTree.node, ForallTree.leaf]
+
+theorem Tree.bst_insert_of_bst
+        {t : Tree β} (h : BST t) (key : Nat) (value : β)
+        : BST (t.insert key value) := by
+  -- TODO: improve `grind` `funext` support, and minimize the number of splits
+  induction h <;> grind (splits := 12) [BST.node, BST.leaf, ForallTree.leaf, forall_insert_of_forall]
+
+def BinTree (β : Type u) := { t : Tree β // BST t }
+
+def BinTree.mk : BinTree β :=
+  ⟨.leaf, .leaf⟩
+
+def BinTree.contains (b : BinTree β) (k : Nat) : Bool :=
+  b.val.contains k
+
+def BinTree.find? (b : BinTree β) (k : Nat) : Option β :=
+  b.val.find? k
+
+def BinTree.insert (b : BinTree β) (k : Nat) (v : β) : BinTree β :=
+  ⟨b.val.insert k v, b.val.bst_insert_of_bst b.property k v⟩
+
+attribute [local simp, local grind]
+  BinTree.mk BinTree.contains BinTree.find?
+  BinTree.insert Tree.find? Tree.contains Tree.insert
+
+theorem BinTree.find_mk (k : Nat)
+        : BinTree.mk.find? k = (none : Option β) := by
+  grind [Tree.find?]
+
+theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
+        : (b.insert k v).find? k = some v := by
+  let ⟨t, h⟩ := b; simp
+  induction t <;> simp <;> grind [BST]
+
+theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
+        : (b.insert k v).find? k' = b.find? k' := by
+  let ⟨t, h⟩ := b; simp
+  induction t <;> simp <;> grind [BST]

tests/lean/run/grind_funext.lean

@@ -0,0 +1,6 @@
+example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
+  grind
+
+example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
+  fail_if_success grind -funext
+  sorry