how does equation compiler magic work?

Stream: general

[Eric Rodriguez]

recently, I've been seeing a lot of things like:

inductive asda
| foo | bar | baz

example : asda.foo ≠ asda.baz.

I understand the proof goes down to no_confusion, but how would I be able to write it directly as a match expression? As far as I know, something like intro h, cases h also does it in tactic mode (or even rintro (_|_|_)), but I'm not too sure how it's done automatically

[Kevin Buzzard]

What happens if you give the example a name and then #print it?

[Eric Rodriguez]

also, if you instead consider something like:

inductive even : ℕ → Prop
| zero : even 0
| succ_succ : ∀ n, even n → even (n + 2)

lemma not_even_three : ¬even 3 :=
begin
  rintro (a|d),
    -- ᾰ_ᾰ: 1.even
end

there's not even any way to name the new hypothesis?

[Eric Rodriguez]

Kevin Buzzard said:

What happens if you give the example a name and then #print it?

λ (ᾰ : asda.foo = asda.baz),
  ᾰ.dcases_on (λ (H_1 : asda.baz = asda.foo), asda.no_confusion H_1) (eq.refl asda.baz) (heq.refl ᾰ)

which makes sense and is the no_confusion proof I mentioned earlier; however, I don't know how to create it "manually" using match and so on, if you understand whast I mean

[Eric Wieser]

I think the answer is you can't, you need Lean 4's nomatch keyword

[Eric Wieser]

The syntax of match doesn't permit an empty list of expressions

[Eric Rodriguez]

i managed to get this:

lemma not_even_three : ¬even 3
| h := match h with | (even.succ_succ _ h) := match h with end end

for example, but it's atrocious

[Eric Wieser]

Isn't that the answer to your original question then?

example : asda.foo ≠ asda.baz := λ h, match h with end