Zulip Chat Archive

Stream: general

Topic: How does one prove unit ≠ bool


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shing Tak Lam (Apr 23 2020 at 13:17):

(Is this to do with the Kata?)

view this post on Zulip Shing Tak Lam (Apr 23 2020 at 13:27):

(deleted)

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 13:28):

yeah this might be a kata spoiler

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 13:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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