apply tactic weird behaviour with lambda expressions

Stream: new members

[EdwardW]

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]

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]

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]

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]

@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]

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]

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]

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]

I haven't read your example yet; I was independently investigating

[Kyle Miller]

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]

@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]

@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]

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]

@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]

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]

I'm not sure why with_reducible doesn't prevent Nat.mul from unfolding, or for that matter the instances.

[Kyle Miller]

Oh, apparently isDefEq has a lot of places with withAtLeastTransparency TransparencyMode.default