lean claims theorem uses sorry

Stream: lean4

[Kevin Buzzard]

This came up on the Xena Discord:

inductive Tree : Type
| K : Tree
| pair : Tree → Tree → Tree

open Tree

inductive cut : Tree → Tree → Prop
| Kpair {x y : Tree} : cut (pair (pair K x) y) x
| pairL {x y z : Tree} : cut x y → cut (pair x z) (pair y z)
| pairR {x y z : Tree} : cut x y → cut (pair z x) (pair z y)

theorem cut.ne {x y : Tree} : cut x y → x ≠ y
-- | Kpair, h => by cases h
| pairL xy, h => xy.ne (pair.inj h).1
| pairR xy, h => xy.ne (pair.inj h).2

With the commented-out line the theorem compiles and complains that we used sorry (as opposed to giving an error saying not all cases are covered). I thought this was surprising.

[Jon Eugster]

it surprises me that some cases of cut take 3 variables x y z without complaining even though the type suggests it should only take 2.

[Jon Eugster]

nevermind, that didn't make sense.

but the following message seems equally weird:

inductive Tree : Type
| K : Tree
| pair : Tree → Tree → Tree

open Tree

inductive cut : Tree → Tree → Prop
| Kpair {x y : Tree} : cut (pair (pair K x) y) x
| pairL {x y z : Tree} : cut x y → cut (pair x z) (pair y z)
| pairR {x y z : Tree} : cut x y → cut (pair z x) (pair z y)


theorem cut.ne {a b : Tree} : cut a b → a ≠ b := fun w => match w with
/-
missing cases:
_, _, (@Kpair _ _)
-/
| pairL xy => fun h => xy.ne (pair.inj h).1
| pairR xy => fun h => xy.ne (pair.inj h).2

why is there the _, _, part in the suggestion?

[Kyle Miller]

It's probably the a and b arguments being included into the match. Technically a match needs match a, b, w with, but Lean can add the extra arguments.

[Bhavik Mehta]

Kevin Buzzard said:

This came up on the Xena Discord:

inductive Tree : Type
| K : Tree
| pair : Tree → Tree → Tree

open Tree

inductive cut : Tree → Tree → Prop
| Kpair {x y : Tree} : cut (pair (pair K x) y) x
| pairL {x y z : Tree} : cut x y → cut (pair x z) (pair y z)
| pairR {x y z : Tree} : cut x y → cut (pair z x) (pair z y)

theorem cut.ne {x y : Tree} : cut x y → x ≠ y
-- | Kpair, h => by cases h
| pairL xy, h => xy.ne (pair.inj h).1
| pairR xy, h => xy.ne (pair.inj h).2

With the commented-out line the theorem compiles and complains that we used sorry (as opposed to giving an error saying not all cases are covered). I thought this was surprising.

For what it's worth, I'm pretty sure the error shouldn't be that not all cases are covered, since the equation compiler should be smart enough to notice the KPair case can't occur.