Zulip Chat Archive
Stream: new members
Topic: apply tactic weird behaviour with lambda expressions
EdwardW (Sep 06 2024 at 12:57):
Hello,
Forgive me if this behaviour is well-known, I have not had (many) issues with apply before and so I am very confused by this behaviour.
import Mathlib.Data.Real.Basic
theorem test {f1 g1 : ℕ → ℕ} (n1 : ℕ) (hfg : ∀a, f1 (g1 a) = a) :
f1 (g1 n1) = n1 := hfg n1
theorem test2 {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
apply test
intro a
-- goal is ((g2 n2).mul 1).add (g2 a) = a. Why??
theorem test3 (n3 : ℕ) : (· / 2) ((· * 2) n3) = n3 := by
apply test n3 -- Doesn't work without specifying n3. Why?
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, mul_div_cancel_right₀]
intro a
-- goal is n3 = a. Impossible
I suspect apply is trying to bind to the definitional function of multiplication, as test2
doesn't even work when using x / 2
instead of x * 2
. However, I cannot see why, as the syntax trees are easy enough to match, and pp.explicit true doesn't show any type mismatches either. I don't see why the parameter n3
or n2
participates in the expression in any case.
What is going on?
Thanks
Ruben Van de Velde (Sep 06 2024 at 14:39):
Odd. It's not just apply
, refine
also gets confused.
import Mathlib.Data.Real.Basic
theorem test {f1 g1 : ℕ → ℕ} (n1 : ℕ) (hfg : ∀a, f1 (g1 a) = a) :
f1 (g1 n1) = n1 := hfg n1
theorem test2 {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
refine test n2 ?_
intro a
-- goal is ((g2 n2).mul 1).add (g2 a) = a. Why??
theorem test2b {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
refine test (g1 := g2) n2 ?_
intro a
-- goal is ((g2 n2).mul 1).add (g2 a) = a. Why??
theorem test2c {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
refine test (f1 := λx => x * 2) n2 ?_
intro a
-- Better:
-- ⊢ (fun x => x * 2) (g2 a) = a
Kevin Buzzard (Sep 06 2024 at 15:13):
Isn't this just "higher order unification is undecidable and the system is thus forced to use heuristics; it finds a perfectly good solution to (λx => x * 2) (g2 x) == ?f (?g x)
which happens to be different to the one you were thinking of"? Because there's more than one solution, it's perhaps not surprising that you have to give some hints.
EdwardW (Sep 06 2024 at 15:22):
Sure, in the event that it works, but then it's some weird heuristics if it can't match a syntax tree that simple, right?
And that doesn't explain why it can't match in test3
, and when you provide a hint then it results in an impossible goal to prove. I don't understand why the parameter variable n
should ever get introduced after the application of apply
anyway...
Jireh Loreaux (Sep 06 2024 at 17:33):
@Kevin Buzzard at first I was going to agree with you, and I was even going to argue that maybe Lean's guess made more sense. So I turned on pp.raw
. After poking around, I realized that the argument I was going to make was bogus (since 2
is represented via OfNat.ofNat
as opposed to a direct Nat.succ 1
). So, I then did the following, and boy was I surprised:
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
f (g n) = n := hfg n
example {g : Nat → Nat} (n : Nat) (hg : ∀a, (g a) * 2 = a) : (λx => x * 2) (g n) = n :=
test (f := λ x => x * 2) n hg -- works
example {g : Nat → Nat} (n : Nat) (hg : ∀a, (g a) * 2 = a) : (λx => x * 2) (g n) = n := by
with_reducible exact test (f := λ x => x * 2) n hg -- works
example {g : Nat → Nat} (n : Nat) (hg : ∀a, (g a) * 2 = a) : (λx => x * 2) (g n) = n :=
/-
application type mismatch
test n hg
argument
hg
has type
∀ (a : Nat), g a * 2 = a : Prop
but is expected to have type
∀ (a : Nat), ((g n).mul 1).add (g a) = a : Prop
-/
test n hg -- fails!
Jireh Loreaux (Sep 06 2024 at 17:34):
To me, this actually looks like something to do with core's handling / simplification of numerals (but I don't know much about such things).
Kyle Miller (Sep 06 2024 at 17:37):
Here's what isDefEq seems to be seeing when solving apply test
in test2
:
theorem test2 {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
dsimp only [HMul.hMul, Mul.mul]
-- (g2 n2).mul 2 = n2
unfold Nat.mul
-- ((g2 n2).mul 1).add (g2 n2) = n2
-- ~~~~~~~~~~~~~~~~~~~ ~~ ~~ ~~
-- f1 g1 \ n1 /
apply test (f1 := ((g2 n2).mul 1).add) (g1 := g2) (n1 := n2)
-- ∀ (a : ℕ), ((g2 n2).mul 1).add (g2 a) = a
sorry
Jireh Loreaux (Sep 06 2024 at 17:39):
But Kyle, in my example shouldn't the metavariable for f
get delayed until hg
is incorporated? It really seems like it should be enough in my case.
Kyle Miller (Sep 06 2024 at 17:39):
I haven't read your example yet; I was independently investigating
Kyle Miller (Sep 06 2024 at 17:42):
But one thing I'll mention is that we can't expect Lean to preserve beta-reducible terms, which is why I started with dsimp
.
Also, the heuristics to solve HO unification only kick in once other avenues are exhausted, is my understanding. The isDefEq algorithm is looking for the solution, not a solution. The apply
tactic has to opt into getting approximate solutions. (Though approximations still seem to happen in various places it seems — I don't know the full story.)
Kyle Miller (Sep 06 2024 at 17:46):
@Jireh Loreaux It seems that for your example, test n hg
is unifying with the the expected type to get f
. I can try to check the elaborator to see when this occurs.
If you do (test n hg :)
instead, to temporarily disable using the expected type, you get a different error:
application type mismatch
test n hg
argument
hg
has type
∀ (a : ℕ), g a * 2 = a : Prop
but is expected to have type
∀ (a : ℕ), ?m.1254 (?m.1255 a) = a : Prop
Maybe this error is why it tries to use the expected type?
Kyle Miller (Sep 06 2024 at 18:04):
@Jireh Loreaux My understanding now of how expected type propagation works is that it tries to unify the return value of a function with the expected type right before elaborating an explicit argument. This unification is allowed to fail, and it will try again on each successive explicit argument. (There is one exception: if the expected type is Prop
itself, then it's not propagated.)
You can see a bit of what it's doing with set_option trace.Elab.app true
. It tries doing (fun x ↦ x * 2) (g n) = n =?= ?m.1254 (?m.1255 n) = n
before elaborating the hg
argument, which (I'm guessing) succeeds, but then it goes on to elaborate hg
but its expected type doesn't match. There aren't enough trace messages to be totally sure.
It's doing a plain isDefEq without any approximations turned on. I suppose this might not count as higher-order unification because after unfolding just a little bit it's able to find a solution without any lambdas. I'm wondering if it's a mistake in isDefEq that it accepts this solution, since it's not 'the' solution.
Kyle Miller (Sep 06 2024 at 18:13):
Given that (test n hg :)
doesn't work, I think it's out of scope for the app elaborator to be able to elaborate this at all, and I think the question here is whether it's failing in the correct way.
Jireh Loreaux (Sep 06 2024 at 18:19):
@Kyle Miller That unfolding of Nat.mul
was very suspicious to me. I tried to avoid it by doing by with_reducible refine test n ?_
but it still errors.
Kyle Miller (Sep 06 2024 at 18:28):
I think the logic is that it sees (g2 n2).mul 2 = n2
and knows it has to be of the form ?f (?g ?n) = ?n
, it solves ?n := n2
, and goes on to (g2 n2).mul 2 =?= ?f (?g n2)
, but it's not the right form, so it does the obvious next step, unfold the head function (Nat.mul
). After that, it's ((g2 n2).mul 1).add (g2 n2)
, and that matches.
Kyle Miller (Sep 06 2024 at 18:30):
I'm not sure why with_reducible
doesn't prevent Nat.mul
from unfolding, or for that matter the instances.
Kyle Miller (Sep 06 2024 at 18:32):
Oh, apparently isDefEq has a lot of places with withAtLeastTransparency TransparencyMode.default
Last updated: May 02 2025 at 03:31 UTC