debug tactic 'apply' failed, failed to unify

Stream: lean4

[Chris Lovett]

I'm stuck on a difference in apply tactic between lean3 and lean4. Notice this lean3 proof uses apply hd, to apply the hypothesis hd: ∀ (b : MyNat), a * b = a * d → b = d to the goal ⊢ succ c = succ d but my lean4 version of this proof says

tactic 'apply' failed, failed to unify
  ?b = d
with
  succ c = succ d

Any ideas how to debug this? I wasn't sure if the have h := c = d was the correct port of have h : c = d, and weather that has anything to do with it, but how do you debug this type of error in general?

[Floris van Doorn]

Any ideas how to debug this? I wasn't sure if the have h := c = d was the correct port of have h : c = d, and weather that has anything to do with it, but how do you debug this type of error in general?

The problem lies here, not with the apply tactic. You can see that after the have the proof states are completely different.

[Floris van Doorn]

You want to have the same have and then indent the next line:

      have h : c = d
        apply hd

[Reid Barton]

have h := c = d means that h is defined to be the proposition c = d itself, whereas almost certainly you wanted h to be a proof of this proposition.

[Chris Lovett]

Thanks, yeah, this long thread I went through all the issues with have and ended up with using := in lean4, e.ghave h : c = d := apply hd. In the porting of NNG I ran into lots of issues with confusing intellisense, non-useful errors like this one, and needing help debugging things.

[Sebastian Ullrich]

I'm not sure how to improve this particular error tbh (without re-explaining what "unify" means). The two right-hand sides are clearly unequal.

[Floris van Doorn]

My recommendation is to have the Lean 3 proof and the Lean 4 proof side-by-side, and see what the first position is where the tactic states differ significantly. Then you at least know what tactic is the problematic one.

[Chris Lovett]

Yes, I did have to resort to loading the lean3 extension and look at the tactic states side by side a few times in the porting process.

[Sebastian Ullrich]

Sebastian Ullrich said:

I'm not sure how to improve this particular error tbh (without re-explaining what "unify" means). The two right-hand sides are clearly unequal.

Highlighting the non-matching parts as in the new goal diff would be cool, but that seems to boil down to basically re-implementing unification once again

[Chris Lovett]

I saw a vscode-lean4 PR titled feat: goal-diffs but I don't know what it does yet, sounds intriguing, is there a demo video I can see?

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1610

[Chris Lovett]

Amazing, can't wait to use it.