# Zulip Chat Archive

## 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