cong_fst_arg

Stream: general

[Phiroc]

Hello,
the Hitchhiker's Guide contains the following lemma :

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

... which I am trying to convert to Lean 4:

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

Unfortunately, both apply tactics fail.

Any help would be much appreciated.

Many thanks.

P

[Ruben Van de Velde]

I would've written rw ha for the first line in lean3; maybe that's easier to convert?

[Phiroc]

That did it. Many thanks Ruben.

[Jannis Limperg]

It seems like Lean 4's higher-order unification is weaker than Lean 3's. Here's a working proof:

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

Lean 4 apparently fails to infer the motive while Lean 3 manages. This is an example of higher-order unification (since motive is a function), which is undecidable in general. Dependently typed languages generally support limited forms of higher-order unification to deal with 'practical' examples like this, but it seems like Lean 4 has opted not to make it very strong.

[Sebastian Ullrich]

It's the elaborator that changed, not the unifier per se. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20mismatch.20error/near/225228721.

[Jannis Limperg]

Ah yes, thanks! So the canonical answer is to always use tactics to apply things that require higher-order unification?

[Sebastian Ullrich]

No, definitely not always. Even just calling a monadic function involves higher-order unification. But when there is something like a motive to be found, tactics are probably the correct answer, yes.

[Phiroc]

To summarize, what is the most efficient way to translate the above code to Lean 4?

[Jannis Limperg]

The idiomatic way is rw ha. I suspect that this example is meant to show what rw generates under the hood, so if you want to translate exactly that, my version with the explicit motive seems like the way to go.

[Leonardo de Moura]

In Lean 4, we have a custom elaborator for constructing Eq.rec: h1 ▸ h2

theorem cong_fst_arg {α : Type} (a a' b : α)
  (f : α → α → α) (ha : a = a') :
  f a b = f a' b :=
ha ▸ rfl