Zulip Chat Archive

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

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

(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: Dec 20 2023 at 11:08 UTC