intro to proof by reflection in idris

reflection.idr

%default total
-- because we're doing proofs

-- This file demonstrates a simple example of proof by reflection
-- mentioned in: http://ftp.science.ru.nl/CompMath.Found/buchberger.pdf

infix 5 <-->

(<-->) : Type -> Type -> Type
p <--> q = (p -> q, q -> p)

a : Type -> Nat -> Type
a p Z = p
a p (S n) = a p n <--> p

lemma1 : (p : Type) -> a p (S Z)
lemma1 p = (id, id)

-- we have a proof of m and want to construct
-- a proof of (m <--> p) <--> p
--
-- (m <--> p) -> p
-- p -> (m <--> p)
lemma2 : (p : Type) -> a p n -> a p (S (S n))
lemma2 p prf = ( (\prf' => fst prf' prf)
               , (\p' => ( (\_ => p') , (\_ => prf ))) )

-- We want to be able to say that something is odd
-- and make use of reduction to prove it trivially

odd : Nat -> Type
odd Z = _|_
odd (S Z) = ()
odd (S (S n)) = odd n

example1 : odd Z -> 1 + 1 = 3
example1 m = absurd m

example2 : odd (S (S (S (S (S Z)))))
example2 = ()

-- relate oddness to provability

odd_lemma : (n : Nat) -> odd (S (S n)) -> odd n
odd_lemma Z m = absurd m
odd_lemma (S Z) () = ()
odd_lemma (S (S n)) m = m

lemma : (n : Nat) -> odd n -> (p : Type) -> a p n
lemma Z m _ = absurd m
lemma (S Z) () p = lemma1 p
lemma (S (S n)) m p = lemma2 p (lemma n (odd_lemma n m) p)

-- Now we can prove these theorems simply by letting idris check that the number is infact odd

theorem : (p : Type) ->
  ((((((((p <--> p) <--> p) <--> p) <--> p) <--> p) <--> p) <--> p) <--> p) <--> p
theorem = lemma (S (S (S (S (S (S (S (S (S Z))))))))) () -- takes a while!