A bug in cases?

Stream: new members

[Victor Miller]

I've just started with the natural number game. In "Advanced Addition World" level 1 there is the following:

theorem succ_inj' {a b : mynat} (hs : succ(a) = succ(b)) : a = b :=

The initial state is:

a b : mynat,
hs : succ a = succ b
⊢ a = b

I started noodling with this, and did the following:

begin
cases hs with aa bb,
refl,
end

If you look at what this does, after the first cases the state is:

a : mynat,
hs : succ a = succ a
⊢ a = a

which definitely looks wrong! In retrospect, why was it able to apply cases at all?

[Johan Commelin]

What were you expecting to happen?

[Johan Commelin]

cases is pretty smart. It can figure out that if succ a = succ b, then this must force a = b.

[Johan Commelin]

So it will substitute a for b everywhere

[Kevin Buzzard]

Hi Victor! You can also use succ_injto prove this. You have inadvertently managed to persuade lean to be clever here

[Eric Wieser]

I'd never considered applying cases to an eq object (like hs) before

[Victor Miller]

Johan Commelin said:

So it will substitute a for b everywhere

Johan, Thanks. I assume that the full capabilities of cases are described in the big document.

Victor

[Bryan Gin-ge Chen]

Eric Wieser said:

I'd never considered applying cases to an eq object (like hs) before

I think we'd usually use subst hs instead (or preempt it by using rfl in rcases / rintro / obtain).