Stream: general

Topic: How does one prove unit ≠ bool

Slavomir Kaslev (Apr 23 2020 at 13:11):

I'm trying to prove

def unit_ne_bool : unit ≠ bool := sorry


and hoping there's a easy proof of this.

One possible direction is to prove that unit->unit is singleton but bool->bool is not but I was hoping for something more trivial.

Reid Barton (Apr 23 2020 at 13:14):

I don't see how introducing these functions could help because it's presumably simpler to prove that unit is a singleton but bool is not.

Shing Tak Lam (Apr 23 2020 at 13:17):

(Is this to do with the Kata?)

(deleted)

Kevin Buzzard (Apr 23 2020 at 13:28):

yeah this might be a kata spoiler

Slavomir Kaslev (Apr 23 2020 at 13:46):

It's not from the kata, I needed it for this proof https://github.com/skaslev/papers/blob/94950c7b7be5278561eab639d82b391872c3e042/kan.lean#L370

(kata spoilers ahead) this is what I came up with:

def iscontr (α : Type) := ∃ x : α, ∀ y : α, x = y

def iscontr_unit : iscontr unit :=
⟨unit.star, λ y, y.rec rfl⟩

def notcontr_bool : ¬iscontr bool
| ⟨bool.ff, h⟩ := bool.no_confusion (h bool.tt)
| ⟨bool.tt, h⟩ := bool.no_confusion (h bool.ff)

def unit_ne_bool : unit ≠ bool :=
λ h, notcontr_bool (h ▸ iscontr_unit)


Is there an easier proof?

Reid Barton (Apr 23 2020 at 13:47):

I think it would be slightly shorter to instead use the property forall x y, x = y but otherwise I think the answer is no.

Kevin Buzzard (Apr 23 2020 at 13:50):

You could use the subsingleton typeclass in Lean I guess, but your proof looks pretty direct.

Kevin Buzzard (Apr 23 2020 at 13:50):

Another proof, if you were prepared to use mathlib machinery, would be to use the fact that both bool and unit were known to be finite types, and bool has cardinality 2 whereas unit has cardinality 1.

Rob Lewis (Apr 23 2020 at 14:00):

Also if you're willing to use mathlib machinery, iscontr_unit and notcontr_bool are decidable, so proved by dec_trivial.

Mario Carneiro (Apr 23 2020 at 14:03):

theorem unit_ne_bool : unit ≠ bool :=
have ∀ {α} (h : unit = α) a, cast h () = a,
by intros; cases h; cases a; refl,
λ h, by cases (this h tt).symm.trans (this h ff)


Last updated: May 15 2021 at 00:39 UTC