Is this type inhabited

Stream: new members

[Pedro Minicz]

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]

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]

Wow, the recursor for β is quite crazy.

[Pedro Minicz]

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]

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]

Even simpler:

inductive γ : Type
| mk : γ → γ

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