## Stream: new members

### Topic: Is this type inhabited

#### 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 → β) → β


#### 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 ())


#### Pedro Minicz (Jul 15 2020 at 04:04):

Wow, the recursor for β is quite crazy.

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

#### 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.)

#### 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