module EmptyFun where -- This file is about a strange definition of the empty set ⊥, and the -- implementation of its elimination rule (ex falsum quodlibet). Peter -- Hancock sent it to me as a riddle: it's indeed a funny brainteaser! -- In Dybjer & Setzer [Induction-recursion and initial algebras, -- 2003]*, the authors gave a (purely inductive, not -- inductive-recursive) definition of the unit type that does not rely -- on the LF empty set. -- *: http://www.cse.chalmers.se/~peterd/papers/InductionRecursionInitialAlgebras.pdf -- In essence, they define the following datatype: data ⊥ : Set where S : ⊥ → ⊥ -- That is, in their words: the empty set can be defined as "the set -- with only one constructor of type ⊥ → ⊥". The proof that this type -- satisfies ex falsum quodlibet is given in Appendix B of that paper. -- The game is the following. Let P : ⊥ → Set be a predicate over ⊥: module ExFalso (P : ⊥ → Set) where -- Prove that from any b : ⊥, we can build an inhabitant of P b: exfalso : (b : ⊥) → P b exfalso = {!!} -- **************************************************************** -- Answer below -- **************************************************************** -- Intuitively, an inhabitant of P b is an absurd program, ie. a -- non-terminating program. So, the game is to craft a non-terminating -- program. Luckily for us, ⊥ provides an infinite supply of -- inhabitants of ⊥! Thus, we define a function that recurses -- (infinitely!) over an inhabitant of ⊥ to provide a proof that -- *another* inhabitant satisfies P: infinite : ⊥ → (b : ⊥) → P b infinite (S x) b = infinite x b -- We get a proof of P b for any b through a diagonal argument: ⊥-elim : (b : ⊥)-> P b ⊥-elim b = infinite b b -- In particular, assuming ⊥, we can prove that true ≡ false: open import Relation.Binary.PropositionalEquality data Bool : Set where true false : Bool test : ⊥ → true ≡ false test b = ExFalso.⊥-elim (λ _ → true ≡ false) b