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