Stream: new members

Topic: A bug in cases?

Victor Miller (Dec 14 2020 at 19:25):

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 (Dec 14 2020 at 19:32):

What were you expecting to happen?

Johan Commelin (Dec 14 2020 at 19:32):

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

Johan Commelin (Dec 14 2020 at 19:32):

So it will substitute a for b everywhere

Kevin Buzzard (Dec 14 2020 at 19:40):

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

Eric Wieser (Dec 14 2020 at 20:22):

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

Victor Miller (Dec 14 2020 at 20:57):

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 (Dec 14 2020 at 21:01):

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

Last updated: May 13 2021 at 21:12 UTC