Zulip Chat Archive

Stream: lean4

Topic: Constructors are injective?


view this post on Zulip François G. Dorais (Jan 05 2021 at 12:42):

What is the Lean 4 way to get injectivity of constructors for inductive types? Browsing through Init, it seems that noConfusion is used directly in lots of places where I would normally use injectivity. Is this the preferred way in Lean 4?

view this post on Zulip Mario Carneiro (Jan 05 2021 at 13:33):

it's probably the only currently existing way

view this post on Zulip Mario Carneiro (Jan 05 2021 at 13:33):

Back before the injection tactic existed that's how you would do it

view this post on Zulip Mario Carneiro (Jan 05 2021 at 13:35):

(fyi no_confusion is injectivity of constructors, it just has a more confusing type)

view this post on Zulip François G. Dorais (Jan 05 2021 at 13:41):

I'm used to having generated .inj theorems. noConfusion works but unfortunately it's not named after what's happening in my brain when I try to use it :)

view this post on Zulip François G. Dorais (Jan 05 2021 at 13:56):

Ah! But the injection tactic does exist!

example (m n : Nat) : m.succ = n.succ  m = n := by {intro h; injection h; assumption}

view this post on Zulip Mario Carneiro (Jan 05 2021 at 14:32):

If it was named after what was happening in your brain when you try to use it it should be called confusion :)

view this post on Zulip François G. Dorais (Jan 05 2021 at 14:42):

Wouldn't deConfusion be a great tactic name? Thanks Mario for deConfusing the fun from what I wrote :)

view this post on Zulip Mario Carneiro (Jan 05 2021 at 14:44):

I'm not even sure the .inj theorems were originally intended for user use

view this post on Zulip Mario Carneiro (Jan 05 2021 at 14:44):

I think they get used by simp

view this post on Zulip Jannis Limperg (Jan 05 2021 at 14:57):

Lean 3 tactic.injection is essentially 'find the correct inj lemma and apply it'.

view this post on Zulip Jacques Carette (Jan 05 2021 at 20:19):

You should look up work by Goguen, who popularized "no junk, no confusion" in CS a long time ago. That "no confusion" is related to injectivity of constructors came later. Goguen was trying to popularize initial algebra semantics, especially amongst people who were anti-category-theory. So nice slogans helped.


Last updated: May 18 2021 at 22:15 UTC