## Stream: general

### Topic: cong_fst_arg

#### Phiroc (Mar 15 2021 at 12:50):

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 (Mar 15 2021 at 12:58):

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

#### Phiroc (Mar 15 2021 at 14:24):

That did it. Many thanks Ruben.

#### Jannis Limperg (Mar 15 2021 at 14:26):

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 (Mar 15 2021 at 14:30):

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 (Mar 15 2021 at 14:33):

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

#### Sebastian Ullrich (Mar 15 2021 at 14:35):

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 (Mar 15 2021 at 14:41):

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

#### Jannis Limperg (Mar 15 2021 at 14:49):

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 (Mar 16 2021 at 15:24):

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


Last updated: May 12 2021 at 23:13 UTC