fix: improve isDefEqProj (#3977)

Currently this will fail in two tests, because of changes in #3965.

* Sometimes we need to add an additional universe annotation, or we get
a `stuck at solving universe constraint max u ?u =?= u`.
* Sometimes we need to specify arguments that could previously be found
by unification.

---------

Co-authored-by: Leonardo de Moura <[email protected]>

src/Lean/Meta/ExprDefEq.lean

@@ -1757,10 +1757,21 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .lt => unfold t (return .unknown) (k · s)
     | .gt => unfold s (return .unknown) (k t ·)
     | .eq =>
-      unfold t
-        (unfold s (return .unknown) (k t ·))
-        (fun t => unfold s (k t s) (k t ·))
+      -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
+      -- if `f` is not a projection. The projection case generates a performance regression.
+      if tInfo.name == sInfo.name && !(← isProjectionFn tInfo.name) then
+        if t.isApp && s.isApp && (← tryHeuristic t s) then
+          return .eq
+        else
+          unfoldBoth t s
+      else
+        unfoldBoth t s
 where
+  unfoldBoth (t s : Expr) : MetaM DeltaStepResult := do
+    unfold t
+      (unfold s (return .unknown) (k t ·))
+      (fun t => unfold s (k t s) (k t ·))
+
   k (t s : Expr) : MetaM DeltaStepResult := do
     let t ← whnfCore t
     let s ← whnfCore s

tests/lean/run/3965.lean

@@ -0,0 +1,206 @@
+section Mathlib.Logic.Function.Iterate
+
+universe u v
+
+variable {α : Type u}
+
+/-- Iterate a function. -/
+def Nat.iterate {α : Sort u} (op : α → α) : Nat → α → α := sorry
+
+notation:max f "^["n"]" => Nat.iterate f n
+
+theorem Function.iterate_succ' (f : α → α) (n : Nat) : f^[n.succ] = f ∘ f^[n] := sorry
+
+end Mathlib.Logic.Function.Iterate
+
+section Mathlib.Data.Quot
+
+variable {α : Sort _}
+
+noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α := sorry
+
+end Mathlib.Data.Quot
+
+section Mathlib.Init.Order.Defs
+
+universe u
+variable {α : Type u}
+
+section Preorder
+
+class Preorder (α : Type u) extends LE α, LT α where
+
+variable [Preorder α]
+
+theorem lt_of_lt_of_le : ∀ {a b c : α}, a < b → b ≤ c → a < c := sorry
+
+end Preorder
+
+variable [LE α]
+
+theorem le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Order.RelClasses
+
+universe u
+
+class IsWellOrder (α : Type u) (r : α → α → Prop) : Prop
+
+end Mathlib.Order.RelClasses
+
+section Mathlib.Order.SetNotation
+
+universe u v
+variable {α : Type u} {ι : Sort v}
+
+class SupSet (α : Type _) where
+
+def iSup [SupSet α] (s : ι → α) : α := sorry
+
+end Mathlib.Order.SetNotation
+
+section Mathlib.SetTheory.Ordinal.Basic
+
+noncomputable section
+
+universe u v w
+
+variable {α : Type u}
+
+structure WellOrder : Type (u + 1) where
+  α : Type u
+
+instance Ordinal.isEquivalent : Setoid WellOrder := sorry
+
+def Ordinal : Type (u + 1) := Quotient Ordinal.isEquivalent
+
+instance (o : Ordinal) : LT o.out.α := sorry
+
+namespace Ordinal
+
+def typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal := sorry
+
+instance partialOrder : Preorder Ordinal := sorry
+
+theorem typein_lt_self {o : Ordinal} (i : o.out.α) :
+    @typein _ (· < ·) sorry i < o := sorry
+
+instance : SupSet Ordinal := sorry
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Basic
+
+section Mathlib.SetTheory.Ordinal.Arithmetic
+
+noncomputable section
+
+universe u v w
+
+namespace Ordinal
+
+def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} :=
+  iSup f
+
+def lsub {ι} (f : ι → Ordinal) : Ordinal :=
+  sup f
+
+def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) :
+    Ordinal :=
+  lsub (fun x : o₁.out.α × o₂.out.α => op (typein_lt_self x.1) (typein_lt_self x.2))
+
+theorem lt_blsub₂ {o₁ o₂ : Ordinal}
+    (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
+    (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := sorry
+
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Arithmetic
+
+section Mathlib.SetTheory.Ordinal.FixedPoint
+
+noncomputable section
+
+universe u v
+
+namespace Ordinal
+
+section
+
+variable {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}}
+
+def nfpFamily (f : ι → Ordinal → Ordinal) (a : Ordinal) : Ordinal :=
+  sup (List.foldr f a)
+
+end
+
+section
+
+variable {f : Ordinal.{u} → Ordinal.{u}}
+
+def nfp (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
+  nfpFamily fun _ : Unit => f
+
+theorem lt_nfp {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := sorry
+
+end
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.FixedPoint
+
+section Mathlib.SetTheory.Ordinal.Principal
+
+universe u v w
+
+namespace Ordinal
+
+def Principal (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Prop :=
+  ∀ ⦃a b⦄, a < o → b < o → op a b < o
+
+theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- after https://github.com/leanprover/lean4/pull/3965 this requires `lt_blsub₂.{u}` or we get
+    -- `stuck at solving universe constraint max u ?u =?= u`
+    -- Note that there are two solutions: 0 and u. Both of them work.
+    exact lt_blsub₂.{u} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+-- Trying again with 0
+theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- universe 0 also works here
+    exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+
+end Ordinal
+
+end Mathlib.SetTheory.Ordinal.Principal

tests/lean/run/3965_2.lean

@@ -0,0 +1,98 @@
+section Mathlib.Init.Order.Defs
+
+universe u
+
+variable {α : Type u}
+
+class PartialOrder (α : Type u) extends LE α, LT α where
+
+theorem le_antisymm [PartialOrder α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Init.Data.Nat.Lemmas
+
+namespace Nat
+
+instance : PartialOrder Nat where
+  le := Nat.le
+  lt := Nat.lt
+
+section Find
+
+variable {p : Nat → Prop}
+
+private def lbp (m n : Nat) : Prop :=
+  m = n + 1 ∧ ∀ k ≤ n, ¬p k
+
+variable [DecidablePred p] (H : ∃ n, p n)
+
+private def wf_lbp {p : Nat → Prop} (H : ∃ n, p n) : WellFounded (@lbp p) := sorry
+
+protected noncomputable def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
+  @WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
+    sorry 0 sorry
+
+protected noncomputable def find {p : Nat → Prop} [DecidablePred p] (H : ∃ n, p n) : Nat :=
+  (Nat.findX H).1
+
+protected theorem find_spec : p (Nat.find H) := sorry
+
+protected theorem find_min' {m : Nat} (h : p m) : Nat.find H ≤ m := sorry
+
+end Find
+
+end Nat
+
+end Mathlib.Init.Data.Nat.Lemmas
+
+section Mathlib.Logic.Basic
+
+theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
+  | ⟨h, _⟩ => h
+
+end Mathlib.Logic.Basic
+
+section Mathlib.Order.Basic
+
+open Function
+
+def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) : PartialOrder α where
+  le x y := f x ≤ f y
+  lt x y := f x < f y
+
+end Mathlib.Order.Basic
+
+section Mathlib.Data.Fin.Basic
+
+instance {n : Nat} : PartialOrder (Fin n) :=
+  PartialOrder.lift Fin.val
+
+end Mathlib.Data.Fin.Basic
+
+section Mathlib.Data.Fin.Tuple.Basic
+
+universe u v
+
+namespace Fin
+
+variable {n : Nat}
+
+def find : ∀ {n : Nat} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)
+  | 0, _p, _ => none
+  | n + 1, p, _ => by
+    exact
+      Option.casesOn (@find n (fun i ↦ p (i.castLT sorry)) _)
+        (if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦
+        some (i.castLT sorry)
+
+theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p]
+    (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
+    (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p := by
+  rcases hf : find p with f | f
+  · sorry
+  · exact Option.some_inj.2 (le_antisymm sorry (Nat.find_min' _ ⟨f.2, sorry⟩))
+
+end Fin
+
+end Mathlib.Data.Fin.Tuple.Basic