Zulip Chat Archive
Stream: mathlib4
Topic: apply? failure
Nir Paz (Nov 12 2023 at 20:50):
Should apply? get this?
import Mathlib
def re (n m : ℕ) : Prop := n = m
instance reSetoid : Setoid ℕ where
r := re
iseqv := ⟨Eq.refl, Eq.symm, Eq.trans⟩
example (a b : ℕ) (h : Quotient.mk' a = Quotient.mk' b) : re a b := by apply?
Quotient.exact h works.
Eric Wieser (Nov 12 2023 at 23:43):
No, because apply? isn't allowed to look at how you defined re
Eric Wieser (Nov 12 2023 at 23:43):
If you replace it with abbrev re instead of def re, which apply? is allowed to look through, then it works
Nir Paz (Nov 16 2023 at 18:50):
What about this?
import Mathlib
example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by exact?
Patrick Massot (Nov 16 2023 at 18:59):
I think this is simply not stated in Mathlib.
Eric Rodriguez (Nov 16 2023 at 18:59):
docs#mt I thought
Eric Rodriguez (Nov 16 2023 at 18:59):
But I thought this may be the performance optimisation stuff
Patrick Massot (Nov 16 2023 at 19:00):
Eric is right and I was wrong.
Scott Morrison (Nov 17 2023 at 01:58):
Eric, Patrick, and I were all wrong. In fact it was a bug (one of the horsemen!) fixed now in std4#368 and #8458.
Nir Paz (Nov 17 2023 at 04:07):
Cool! Is there a rule of thumb for when it's ok for apply to not find a single-theorem-solution, like due to "optimization stuff"?
Nir Paz (Nov 17 2023 at 04:08):
Because I always think of that as a problem and I guess sometimes it's not
Nir Paz (Nov 17 2023 at 04:09):
(Excluding things like my first example with defs)
Scott Morrison (Nov 17 2023 at 04:13):
As far as I know, after #8458 and #8459 land, I think the claim is:
if you can prove a goal via
apply X; solve_by_elim*for someX, thenexact?should work
and
if you can prove a collection of goals via
apply X; apply Y; ...; apply Z, where all theX Y Zare hypotheses, thensolve_by_elim*should work
These are probably wrong, but I'd be happy to see more examples where they are wrong!
Joachim Breitner (Nov 17 2023 at 06:54):
Great way to phrase the specification for these tactics. Maybe could be part of the docstring?
Nir Paz (Feb 05 2024 at 21:15):
import Mathlib.Tactic.LibrarySearch
import Mathlib.Order.RelIso.Basic
example {α} (r s t : α → α → Prop) (h : s ≃r r) (h' : r ≃r t) : α ↪ α := by
have := h.injective
have := h'.injective
use fun a ↦ h' (h a)
exact? --fails
fails, but works with use fun a ↦ (h' ∘ h) a. (apply Function.Injective.comp; solve_by_elim* works in both cases)
So does exact? not try all theorems with results defeq to the goal? If that's how it works then there must be lots of cases where it can't close goals where a single apply would work.
Patrick Massot (Feb 05 2024 at 21:51):
So this is not what it does. It used to do it in Lean 3 and it became unusable because Mathlib is now too large. So it uses some indexing now and this will not see through definitional equality.
Jireh Loreaux (Feb 06 2024 at 02:42):
Another way to say this: exact? in Lean 4 now requires that matches satisfy a stricter equality constraint.
Nir Paz (Feb 07 2024 at 22:18):
Is there a tactic that does what the old exact did? I often spend >2 minutes loogling and find a single theorem proof, and when it's obvious that what I want is somewhere in the library I'd rather just let that run for a minute.
Kevin Buzzard (Feb 07 2024 at 22:28):
You presumably mean exact? in your message. Yes it would be nice sometimes to have an exact?! or eexact? which tried harder.
Michael Stoll (May 07 2025 at 18:18):
Let me resurrect this thread, even though it is not clear to me whether the following is actually a failure of apply? proper. The following code
import Mathlib.Analysis.CStarAlgebra.Classes
lemma aux {x : ℝ} (hx : 0 < x) (hx₁ : x < 1) {z : ℂ} (hz : ‖z‖ < 1 / 2) :
‖1 - x * (1 + z)‖ < 1 := by
rw [mul_add, ← sub_sub, mul_one]
calc ‖1 - x - x * z‖
_ ≤ ‖(1 - x : ℂ)‖ + ‖x * z‖ := by apply?
_ < 1 := by sorry
(the strange import is suggested by #min_imports when I use import Mathlib) results in a timeout
(deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
Additional diagnostic information may be available using the `set_option diagnostics true` command.
and gives red squiggles not at apply?, but at import(!) and at sorry. Replacing apply? by sorry makes it go away, so the problem should be with apply?.
With set_option diagnostics true, I see
[diag] Diagnostics ▼
[reduction] unfolded declarations (max: 170990, num: 11): ▼
[] HSub.hSub ↦ 170990
[] Sub.sub ↦ 56809
[] Add.add ↦ 27823
[] HAdd.hAdd ↦ 27822
[] HMul.hMul ↦ 723
[] Mul.mul ↦ 723
[] DFunLike.coe ↦ 282
[] Real.toNNReal ↦ 80
[] max ↦ 78
[] LE.le ↦ 36
[] LT.lt ↦ 27
which looks decidedly fishy (this is on live.lean-lang.org with stable Mathlib, but it is similar with latest Mathlib).
So:
- Question 1. Why does
apply?time out in such a simple situation instead of suggesting docs#norm_sub_le ? - Question 2. Why does the error not appear at
apply?, but at two seemingly unrelated locations?
I should mention that I have observed apply? time out fairly regularly recently in similar straight-forward situations, which makes it all but unusable. So it would be really good to fix this...
Michael Stoll (May 07 2025 at 18:33):
More minimal:
import Mathlib.Data.Complex.Norm
set_option diagnostics true
lemma bar (x : ℝ) (z : ℂ) : ‖x - z‖ ≤ ‖(x : ℂ)‖ + ‖z‖ := by
apply?
So it is not related to apply? occurring within a calc block.
Michael Stoll (May 07 2025 at 18:38):
Replacing (x : ℝ) by (x : ℂ) makes the problem go away.
Michael Stoll (May 07 2025 at 18:39):
The diagnostics output is
[diag] Diagnostics ▼
[reduction] unfolded declarations (max: 154626, num: 14): ▼
[] Complex.ofReal ↦ 154626
[] HSub.hSub ↦ 112444
[] Sub.sub ↦ 112444
[] HAdd.hAdd ↦ 33740
[] Add.add ↦ 33736
[] HMul.hMul ↦ 8432
[] Mul.mul ↦ 8432
[] DFunLike.coe ↦ 3734
[] Real.toNNReal ↦ 938
[] max ↦ 936
[] Function.comp ↦ 66
[] Classical.propDecidable ↦ 46
[] dite ↦ 36
[] Function.invFun ↦ 36
[reduction] unfolded instances (max: 33742, num: 3): ▼
[] instHAdd ↦ 33742
[] Real.instAdd ↦ 16872
[] instAddNat ↦ 16870
[reduction] unfolded reducible declarations (max: 179922, num: 9): ▼
[] Complex.re ↦ 179922
[] ZeroHom.toFun ↦ 2812
[] Equiv.toFun ↦ 542
[] Equiv.invFun ↦ 452
[] Subtype.val ↦ 96
[] Function.Embedding.toFun ↦ 87
[] outParam ↦ 43
[] Decidable.casesOn ↦ 36
[] semiOutParam ↦ 24
[def_eq] heuristic for solving `f a =?= f b` (max: 89962, num: 15): ▼
[] Complex.re ↦ 89962
[] HSub.hSub ↦ 30927
[] Sub.sub ↦ 30926
[] instHAdd ↦ 16870
[] HAdd.hAdd ↦ 16869
[] Add.add ↦ 16868
[] HMul.hMul ↦ 4217
[] Mul.mul ↦ 4216
[] DFunLike.coe ↦ 1559
[] ZeroHom.toFun ↦ 1406
[] max ↦ 469
[] Real.toNNReal ↦ 469
[] Equiv.toFun ↦ 149
[] Equiv.invFun ↦ 148
[] Subtype.val ↦ 43
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
Michael Stoll (May 07 2025 at 18:41):
With (x : ℂ), the output is
[diag] Diagnostics ▼
[reduction] unfolded declarations (max: 644, num: 7): ▼
[] DFunLike.coe ↦ 644
[] Function.comp ↦ 62
[] dite ↦ 54
[] Classical.propDecidable ↦ 54
[] Function.invFun ↦ 54
[] norm ↦ 25
[] LE.le ↦ 22
[reduction] unfolded reducible declarations (max: 143, num: 6): ▼
[] Function.Embedding.toFun ↦ 143
[] Equiv.toFun ↦ 140
[] Equiv.invFun ↦ 132
[] Decidable.casesOn ↦ 54
[] outParam ↦ 26
[] Subtype.val ↦ 26
Michael Stoll (May 07 2025 at 18:45):
import Mathlib.Data.Complex.Norm
lemma bar (x : ℝ) (z : ℂ) : ‖x - z‖ ≤ ‖(x : ℂ)‖ + ‖z‖ := by
set w := Complex.ofReal x
apply?
also avoids the error.
Michael Stoll (May 09 2025 at 18:42):
I tried to investigate this further. In
import Mathlib.Data.Complex.Norm
set_option trace.profiler true
set_option trace.profiler.threshold 10
def f (x : ℝ) : ℂ := x
lemma foof (x : ℝ) (z : ℂ) : Norm.norm (f x + z) ≤ Norm.norm (f x) + Norm.norm z := by
exact? -- works
the trace looks like this:
[Elab.async] [0.038708] elaborating proof of Test.foof ▼
[definition.value] [0.038288] Test.foof ▼
[step] [0.037860] exact? ▼
[] [0.037828] exact? ▼
[] [0.037404] exact? ▼
[Tactic.librarySearch] [0.019233] ✅️ ‖f x + z‖ ≤ ‖f x‖ + ‖z‖ ▼
[] [0.018645] ✅️ trying norm_add_le ▼
[Meta.isDefEq] [0.017767] ✅️ ‖?a + ?b‖ ≤ ‖?a‖ + ‖?b‖ =?= ‖f x + z‖ ≤ ‖f x‖ + ‖z‖ ▼
[delta] [0.017692] ✅️ ‖?a + ?b‖ ≤ ‖?a‖ + ‖?b‖ =?= ‖f x + z‖ ≤ ‖f x‖ + ‖z‖ ▼
[] [0.014135] ✅️ ‖?a + ?b‖ =?= ‖f x + z‖ ▼
[delta] [0.014054] ✅️ ‖?a + ?b‖ =?= ‖f x + z‖
[] [0.013741] exact norm_add_le (f x) z
In contrast, in
import Mathlib.Data.Complex.Norm
lemma foocoe (x : ℝ) (z : ℂ) : Norm.norm (Complex.ofReal x + z) ≤ Norm.norm (Complex.ofReal x) + Norm.norm z := by
exact? -- times out
I see (after some unfolding)
[Elab.async] [6.995060] elaborating proof of Test.foocoe ▼
[definition.value] [6.991602] Test.foocoe ▼
[step] [6.991325]
exact?
sorry ▼
[] [6.991303] exact?
sorry ▼
[] [6.991261] exact? ▼
[Tactic.librarySearch] [0.011504] ✅️ ‖↑x + z‖ ≤ ‖↑x‖ + ‖z‖ ▶
[] [6.977442] exact norm_add_le (↑x) z ▼
[] [6.977402] expected type: ‖↑x + z‖ ≤ ‖↑x‖ + ‖z‖, term
norm_add_le (↑x) z ▼
[Meta.isDefEq] [6.977083] 💥️ ‖↑x + z‖ ≤ ‖↑x‖ + ‖z‖ =?= ‖?m.269 + z‖ ≤ ‖?m.269‖ + ‖z‖ ▼
[delta] [6.639590] ❌️ ‖↑x + z‖ ≤ ‖↑x‖ + ‖z‖ =?= ‖?m.269 + z‖ ≤ ‖?m.269‖ + ‖z‖ ▼
[] [6.639567] ❌️ ‖↑x + z‖ =?= ‖?m.269 + z‖ ▼
[] [6.638362] ❌️ Complex.instNorm.1 (↑x + z) =?= SeminormedAddGroup.toNorm.1 (?m.269 + z) ▼
[] [6.638310] ❌️ √(Complex.normSq
(↑x +
z)) =?= { toFun := norm, map_zero' := Complex.norm_map_zero'✝,
add_le' := Complex.norm_add_le'✝, neg' := Complex.norm_neg'✝,
eq_zero_of_map_eq_zero' := Complex.instNormedAddCommGroup._proof_1 }.toAddGroupSeminorm
(?m.269 + z) ▶
[] [0.337464] 💥️ Real.instLE.1 ‖↑x + z‖ (‖↑x‖ + ‖z‖) =?= Real.instLE.1 ‖?m.269 + z‖ (‖?m.269‖ + ‖z‖) ▶
This looks like it tries to unify two norms on ℂ: the one from docs#Complex.instNorm and the one coming via docs#AddGroupNorm.toNormedAddCommGroup, where the toFun component of the argument, which is an docs#AddGroupNorm, is defined as docs#Norm.norm (so should be the same). After several more steps unfolding, it gets to (see next message)
Michael Stoll (May 09 2025 at 18:44):
[] [6.637245] ❌️ (NNReal.sqrt
(Complex.normSq
(↑x +
z)).toNNReal).1 =?= (NNReal.sqrt
(Complex.normSq (?m.269 + z)).toNNReal).1 ▼
[delta] [0.023862] ❌️ NNReal.sqrt (Complex.normSq (↑x + z)).toNNReal =?= NNReal.sqrt (Complex.normSq (?m.269 + z)).toNNReal ▶
[delta] [0.018011] ❌️ (...)
[delta] [0.016281] ❌️ (...)
[delta] [0.015544] ❌️ (...)
[delta] [0.015467] ❌️ (...)
[delta] [0.015251] ❌️ (...)
[delta] [0.016040] ❌️ (...)
[delta] [0.732600] ❌️ (StrictMono.orderIso (fun x ↦ x ^ 2) ⋯).symm
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq
(↑x +
z)).toNNReal) =?= (StrictMono.orderIso (fun x ↦ x ^ 2)
⋯).symm
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal) ▶
[delta] [0.697105] ❌️ (StrictMono.orderIso (fun x ↦ x ^ 2) ⋯).symm.toFun
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq
(↑x +
z)).toNNReal) =?= (StrictMono.orderIso (fun x ↦ x ^ 2)
⋯).symm.toFun
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal) ▶
[delta] [0.713974] ❌️ (StrictMono.orderIso (fun x ↦ x ^ 2) ⋯).invFun
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq
(↑x +
z)).toNNReal) =?= (StrictMono.orderIso (fun x ↦ x ^ 2)
⋯).invFun
(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal) ▶
[delta] [1.433555] ❌️ Function.invFun (fun x ↦ x ^ 2)
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq
(↑x +
z)).toNNReal) =?= Function.invFun (fun x ↦ x ^ 2)
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ ⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal) ▶
[delta] [1.478169] ❌️ if h :
∃ x_1,
(fun x ↦ x ^ 2) x_1 =
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ
⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (↑x + z)).toNNReal) then
h.choose
else
Classical.arbitrary
NNReal =?= if h :
∃ x,
(fun x ↦ x ^ 2) x =
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ
⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal) then
h.choose
else Classical.arbitrary NNReal ▶
[] [1.460850] ❌️ Decidable.rec (fun h ↦ (fun h ↦ Classical.arbitrary NNReal) h) (fun h ↦ (fun h ↦ h.choose) h)
(Classical.propDecidable
(∃ x_1,
(fun x ↦ x ^ 2) x_1 =
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ
⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq
(↑x +
z)).toNNReal))) =?= Decidable.rec
(fun h ↦ (fun h ↦ Classical.arbitrary NNReal) h)
(fun h ↦ (fun h ↦ h.choose) h)
(Classical.propDecidable
(∃ x,
(fun x ↦ x ^ 2) x =
↑(((OrderIso.setCongr (Set.range fun x ↦ x ^ 2) Set.univ
⋯).trans
OrderIso.Set.univ).symm
(Complex.normSq (?m.269 + z)).toNNReal))) ▶
which looks pretty horrible to me.
Is this some kind of diamond?
Michael Stoll (May 09 2025 at 18:48):
Note that when I hover over the norm symbols in the infoview with the cursor after by, all of them look like @norm ℂ Complex.instNorm _ : ℝ. So I wonder why the other norm instance pops up.
Michael Stoll (May 09 2025 at 18:51):
OK; I guess it's because docs#norm_add_le has type
norm_add_le.{u_5} {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a + b‖ ≤ ‖a‖ + ‖b‖
Still, this does not explain why the problem does not occur when I replace docs#Complex.ofReal by f (even with abbrev f : ℝ → ℂ := Complex.ofReal).
Michael Stoll (May 09 2025 at 19:05):
Note also that
import Mathlib.Data.Complex.Norm
example : (@SeminormedAddCommGroup.toSeminormedAddGroup ℂ <|
@NormedAddCommGroup.toSeminormedAddCommGroup ℂ Complex.instNormedAddCommGroup).toNorm =
Complex.instNorm := rfl
is quick.
Michael Stoll (May 09 2025 at 19:13):
Here is a more minimal WE:
import Mathlib.Data.Complex.Norm
lemma foo (x : ℝ) (z : ℂ) : ‖x + z‖ ≤ ‖Complex.ofReal x‖ + ‖z‖ := norm_add_le (↑x) z
It does work with (x : ℂ) or Complex.ofReal x in place of ↑x.
(One difference is that with exact? or apply?, the red squiggle appears at the import statement, whereas here it appears at lemma foo ....)
Michael Stoll (May 09 2025 at 19:22):
Or maybe even
import Mathlib.Data.Complex.Norm
set_option trace.profiler true
set_option trace.profiler.threshold 10
variable (x : ℝ) (z : ℂ)
#check (norm_add_le (↑x) z : ‖x + z‖ ≤ ‖Complex.ofReal x‖ + ‖z‖)
Michael Stoll (May 09 2025 at 19:40):
I moved this discussion to #mathlib4 > Coercion triggers timeout @ 💬 ; the title of this thread does not really fit as the problem does not appear to be specific to apply?.
Michael Stoll (May 15 2025 at 19:06):
If you have observed apply? or exact? timing out (or taking a very long time) unexpectedly, this may be related to what is described in the thread linked above, and so you may want to up-vote the issue I created for this: lean4#8364
Last updated: Dec 20 2025 at 21:32 UTC