debugging 'apply' failed to unify

Stream: lean4

[Chris Lovett]

I'm trying to debug why the Eq.subst ha doesn't work in this proof, but the trace output is not very helpful - or at least I don't know how to make it helpful...

theorem cong_fst_arg {α : Type} (a a' b : α)
(f : α → α → α) (ha : a = a') : f a b = f a' b := by
  set_option trace.Meta.isDefEq true in
  apply Eq.subst ha
  apply Eq.refl

The Eq.subst fails saying:

tactic 'apply' failed, failed to unify
  ?m.33 a'
with
  f a b = f a' b

Is it not able to reach inside the function call and substitute a for a' ? Because it could do that in lean3, here:

lemma cong_fst_arg {α : Type} (a a' b : α)
    (f : α → α → α) (ha : a = a') :
  f a b = f a' b :=
begin
  apply eq.subst ha,
  apply eq.refl
end

[Tomas Skrivan]

My guess is that this is a problem with high order unification e.g. filling hole ?m.33 a' where ?m.33 is a function. This is a hard problem which often does not have a unique solution.

It works, if you specify the motive explicitly:

theorem cong_fst_arg {α : Type} (a a' b : α)
(f : α → α → α) (ha : a = a') : f a b = f a' b := by
  apply Eq.subst ha (motive := λ x => f a b = f x b)
  apply Eq.refl

Let's try to prove the theorem using this lemma

theorem subst {α : Type} {a a' : α} {f : α → α} (ha : a = a') : f a = f a' := by rw[ha]

The naive attempt fails with a very similar unification problem

example {α : Type} (a a' b : α) (f : α → α → α) (ha : a = a')
  : f a b = f a' b := by
  -- tactic 'apply' failed, failed to unify ?m.133 a = ?m.133 a' with f a b = f a' b
  apply subst ha

It works when you specify f explicitly: apply subst ha (f := λ x => f x b).

I deal with this problem all the time. My usual work around is to state variants of subst

theorem subst_parm1 {α β : Type} {a a' : α} {b : β} {f : α → β → α} (ha : a = a') : f a b = f a' b := by rw[ha]

then the original theorem is solvable by apply subst_parm1 ha.

---

I do not really understands the inner workings of high order unification, but a good rule of thumb is that the pattern ?m.33 a' has to "match syntactically" i.e. all the parts of the function ?m.33 have to be left of a. Therefore f a b does not match ?m.33 a' because the only solution λ x => f x b is left and right of a.

It would be great if someone who really understands how this works in Lean would comment on this.

Also any improvement to high order unification would be highly appreciated from my side. For example, this exact problem is making automatic differentiation involving high rank tensors quite difficult.

[Chris Lovett]

I have found the set_option trace.Meta.isDefEq true to be useful, It helped me figure out the required second motive in this case which was tricky (no a' on the right hand side of the proposition).

lemma cong_two_args {α : Type} (a a' b b' : α)
  (f : α → α → α) (ha : a = a') (hb : b = b') :
f a b = f a' b' := by
  apply Eq.subst ha (motive := λ x => f a b = f x b')
  apply Eq.subst hb (motive := λ x => f a b = f a x)
  apply Eq.refl

[Chris Lovett]

I wonder if it has something to do with β-conversion (λx => f x) a = f a? The explanation of the cong_fst_arg proof in hglv is as follows:

The Eq.subst instance we use has ?a := a, ?b := a', and ?p := (λ x => f a b = f x b):
lean a = a' → (λx => f a b = f x b) a → (λx => f a b = f x b) a'
In β-reduced form:
lean a = a' → f a b = f a b → f a b = f a' b
The lemma's first assumption matches the hypothesis ha : a = a', which is passed as an argument in the
first apply invocation. The lemma's second assumption is a trivial equality that can be proved by
apply Eq.refl or rfl. The lemma's conclusion matches the goal’s target. Notice how a higher-order
variable (e.g., ?p) can represent an arbitrary context (e.g., f . . . b) around a term (e.g.,
a or a'). This works because apply unifies up to computation, including β-conversion.

This phrase can represent an arbitrary context (e.g., f . . . b) around a term might be important, does this mean lean3 β-conversion can convert (λx => f x n₁ ... nₖ) a = f a n₁ ... nₖ and perhaps lean4 cannot? And this is why it could not handle my f a b function? I could understand in general this is hard, the second motive I have above in cong_two_args is interesting (motive := λ x => f a b = f a x)` because it is not converting the first parameter, it is converting the second!, So for lean to find this out it has to kind of try every combination of parameters which could be slow. Perhaps lean4 doesn't want to be slow doing these kinds of expensive searches? Just a wild guess on my part though...

[Mario Carneiro]

I believe it is a bug in elabAsElim. It is leaving some arguments unevaluated before calculating the motive.

[Leonardo de Moura]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/elabAselim.20issue/near/301653783

[Mario Carneiro]

@Leonardo de Moura Sorry for not elaborating, it's not just that. Here's the MWE:

import Lean
open Lean Meta Elab Term

@[elabAsElim] theorem Eq.subst' : type_of% @Eq.subst := @Eq.subst

example {f : α → β} (h : a = a') : f a = f a' := by
  refine Eq.subst' h ?_
  -- goal is f a = f a', should be f a = f a

I narrowed the issue down to this:

elab "test1" t:term : tactic => do
  let e ← elabAppArgs (← mkConstWithFreshMVarLevels ``Eq.subst')
    #[] #[.stx t, .stx (← `(?_))] (← Elab.Tactic.getMainTarget) false false
  logInfo m!"{← instantiateMVars e}"

elab "test2" t:term : tactic => do
  let e ← elabAppArgs (← mkConstWithFreshMVarLevels ``Eq.subst')
    #[] #[.expr (← elabTerm t none), .stx (← `(?_))] (← Elab.Tactic.getMainTarget) false false
  logInfo m!"{← instantiateMVars e}"

set_option pp.all true
example {f : α → Prop} (h : a = a') : f a' := by
  test1 h -- @Eq.subst'.{?u.31628} ?m.31642 (fun (x : ?m.31642) => f a') ?m.31644 ?m.31645 ?m.31646 ?m.31647
  test2 h -- @Eq.subst'.{?u.31611} α (fun (x : α) => f x) a a' h ?m.31670

It seems that the elaboration of all the arguments other than the motive and targets are delayed, which makes the kabstract fail to find anything because we need to use h in this example to determine that the target is a'. I looked into the lean 3 code and I think it has some auxiliary check of the dependencies between the arguments in the original type to figure out which one is the major premise (which should be elaborated eagerly) and which ones are minor premises (which we should delay until after we have the motive)

[Leonardo de Moura]

@Mario Carneiro Thanks for investigating. Let's create an issue with all these notes and analysis. I will take a look after I am done with the compiler. I am assuming this is not blocking anybody. One can use rw/simp in tactic mode, and ▸ in term mode.