Zulip Chat Archive

Stream: general

Topic: cong_fst_arg


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Phiroc (Mar 15 2021 at 14:24):

That did it. Many thanks Ruben.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Phiroc (Mar 15 2021 at 14:41):

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

view this post on Zulip 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.

view this post on Zulip 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