Trying to understand unification failures

Stream: lean4

[Alex Meiburg]

Sometimes rw fails to match an expression, for reasons I really don't understand.

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  rw [← Classical.skolem (p := fun x y ↦ _ = _)]
  sorry

this rw works, but if I remove this teeny tiny hint that p should match _ = _, then it fails. Even if I provide all the other arguments, if I change it to p := fun x y => _ instead it fails. I guess this is a generic unification failure, because apply has the same issue.

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  apply (Classical.skolem (α := ℤ) (b := fun _ ↦ ℤ) (p := fun x y ↦ _)).mp
  sorry

fails to unify, but

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  apply (Classical.skolem (p := fun x y ↦ _ = _)).mp
  sorry

works fine.

The error message when it fails is

tactic 'apply' failed, failed to unify
  ∃ f, ∀ (x : ℤ), ?m.32623 x (f x)
with
  ∃ f, ∀ (n : ℤ), 1 + f n = n + 5
⊢ ∃ f, ∀ (n : ℤ), 1 + f n = n + 5

Now I don't know the details of unification internally, but as a user, this is extremely weird! If I look at the expression ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5, it seems there is exactly one to unify ?m.32623 x (f x) with 1 + f n = n + 5, since it's the head of the expression that's undetermined! As long as the expression 1 + f n = n + 5 can be written in terms of x and f x, obviously these can be unified! And yet when I tell it to match it to _ = _, then it magically works: it can unify 1 + f n with ?m x (f x), as well as n + 5.

There are even stranger cases.

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), f n + n = n + f n := by
  apply (Classical.skolem (α := ℤ) (b := fun _ ↦ ℤ) (p := fun x y ↦ y + x = x + _)).mp
  sorry

fails to unify:

tactic 'apply' failed, failed to unify
  ∃ f, ∀ (x : ℤ), f x + x = x + ?m.32638 x (f x)
with
  ∃ f, ∀ (n : ℤ), f n + n = n + f n
⊢ ∃ f, ∀ (n : ℤ), f n + n = n + f n

so in other words it can't unify the f n with ?m n (f n), which seems _super_ strange to me.

Is there some setting I can twiddle with to make this rw, well, smarter? It gets really frustrating that I end up having to manually write out the whole gosh-darn expression I want to simplify.

[Kevin Buzzard]

import Mathlib.Tactic

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  refine (Classical.skolem).mp _
  sorry

gives (amongst other things) a universe unification error, which might be some (but probably not all) the problem. But even

import Mathlib.Tactic

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  refine (Classical.skolem.{1, 1}).mp ?_
  sorry

doesn't work.

[Alex Meiburg]

Even

example : ∃ (f : ℤ → ℤ), ∀ (n : ℤ), 1 + f n = n + 5 := by
  refine (Classical.skolem.{1, 1} (p := ?_)).mp ?_
  sorry
  sorry

doesn't work, which is weird because I would think that refine would at least me _try_ to provide p in the following goal.

[Kyle Miller]

This is higher-order unification, and it's hit-or-miss. I believe that the limitation is that unification can handle ?m x y z =?= v where x, y, and z are variables, but not otherwise. For example, not your case ?m x (f x) =?= 1 + f n = n + 5 where it's x and the non-variable f x.

[Kyle Miller]

If arguments to a metavariable are variables, unification can abstract out x, y, and z from v to make a function g := fun x y z => v' satisfying g x y z = v, and then assign ?m := g.

If any of the arguments aren't variables, abstracting is more fraught with difficulties ("motive not type correct" is a difficulty you're probably familiar with), and it looks like it gives up. I don't know the details — I'm just trying to read the code.

[Mario Carneiro]

note that higher order unification is undecidable, which is one of the main motivations for not doing the "right" thing in all cases here and using a heuristic instead

[Alex Meiburg]

Ahhh man... I mean, I know that these things get undecidble fast, but ?m (f x) (g y) = v -- where the only metavariable is the function being applied -- would seem like a tractable case, no?

Or is the issue that it's something like, if f x had a particular fixed value, then the ?m could do something that "looks inside" and does something nontrivial...?

Like if f had an inverse g so that g (f x) was defeq x, then I guess ?m (f x) could unify with x. Is that the kind of issue here?

[Alex Meiburg]

Thanks for the info so far though

[Kyle Miller]

I think that's one of the issues in the direction of undecidability. Another issue that's more immediate is the dependent type issue I mentioned, that v might contain f x but depend on it being defeq to something (meaning you can't abstract it out).