Constructors are injective?

Stream: lean4

[François G. Dorais]

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?

[Mario Carneiro]

it's probably the only currently existing way

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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 :)

[François G. Dorais]

Ah! But the injection tactic does exist!

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

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

I think they get used by simp

[Jannis Limperg]

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

[Jacques Carette]

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.