Zulip Chat Archive

Stream: new members

Topic: Is this type inhabited


view this post on Zulip Pedro Minicz (Jul 15 2020 at 03:03):

I am sure its impossible to inhabit β, however, I cannot easily think of a proof for it (β → false). Is β really uninhabited? If so, is it provable in Lean that β → false.

inductive α : Type 1
| mk {β γ : Type} (l : β  α) (r : γ  α) : α

def a : α := α.mk empty.elim empty.elim

inductive β : Type
| mk : (unit  β)  β

view this post on Zulip Kyle Miller (Jul 15 2020 at 03:25):

It looks funny, but here's a proof:

lemma uninhabited : β  false
| (β.mk f) := uninhabited (f ())

Or, if you like recursors,

lemma uninhabited : β  false :=
λ x, β.rec_on x (λ _ f, f ())

view this post on Zulip Pedro Minicz (Jul 15 2020 at 04:04):

Wow, the recursor for β is quite crazy.

view this post on Zulip Pedro Minicz (Jul 15 2020 at 04:05):

Kyle Miller said:

It looks funny, but here's a proof:

lemma uninhabited : β  false
| (β.mk f) := uninhabited (f ())

How can Lean see that this terminates?

view this post on Zulip Kyle Miller (Jul 15 2020 at 04:10):

I think it sees that f () has less complexity than β.mk f, so it's able to work out a definition for uninhabited using recursors. (You can always #print uninhabited to see what term-mode proof it derived.)

view this post on Zulip Peter Bruin (Jul 15 2020 at 07:35):

Even simpler:

inductive γ : Type
| mk : γ  γ

lemma uninh : γ  false :=
  λ x, γ.rec_on x (λ _ y , y)

Last updated: May 16 2021 at 05:21 UTC