How does cases work on Prop Equalities

Stream: lean4

[Shreyas Srinivas]

Why does this work?

inductive EG
| A
| B

example : EG.A ≠ EG.B := by
  intro H
  cases H
  done

I call cases on a hypothesis which is a Prop equality. This has precisely one constructor. Based on the docs this will result in a goal with one case Eq.refl. What further steps did cases do here? I understand that constructors are injective and disjoint. I just don't understand how cases was enough for this.

[Shreyas Srinivas]

I have tried a few more examples, and essentially cases seems to do what discriminate does in Coq

[Kevin Buzzard]

There aren't any cases, because lean knows that A and B are different constructors so are not equal, so it can't unify with x=x

[Kevin Buzzard]

What would you expect the goal to be if you are expecting a goal?

[Shreyas Srinivas]

what cases normally does, a case with the absurd expression as hypothesis and False as the goal

[Kevin Buzzard]

That's what the goal was before cases, right?

[Kevin Buzzard]

It's cases job to return every possibility for all the constructors which match, but none match here.

[Shreyas Srinivas]

okay so basically that is enough for cases to say "nothing to do here".

[Kevin Buzzard]

It returns a goal for each case which can work, and none work so it leaves no goals so you proved your theorem. rintro \<\> probably works too (for the same reason)

[Shreyas Srinivas]

I think I just stumbled on a difference between Lean's cases and Coq's destruct, although their documentation would suggest that they are the same. For the example I provided both of them do the same thing. But Lean's cases does something more. It tries some unification stuff
So while the following example from software foundations translated to lean perfectly works:

theorem discriminate_ex2 :
  ∀ (n : Nat), Nat.succ n = Nat.zero → 2 + 2 = 5:= by
    intros n H
    cases H
    done

In the coq proof from SF replacing discriminate with just destruct doesn't work:

Theorem discriminate_ex2 : ∀ (n : nat),
  S n = O →
  2 + 2 = 5.
Proof.
  intros n contra.
  discriminate contra. -- replacing this with  `destruct` doesn't work.
 Qed.

Therefore, Lean's cases $\sim$ Coq'sdestruct $\cup$ discriminate