Skip to content

Instantly share code, notes, and snippets.

@pelotom
Last active August 29, 2015 14:07
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pelotom/a6242a1b6f1e9e7dd46a to your computer and use it in GitHub Desktop.
Save pelotom/a6242a1b6f1e9e7dd46a to your computer and use it in GitHub Desktop.
Idris code for the problem posed in Joseph Abrahamson's type theory talk http://jspha.com/posts/papers_we_love_BOS_2/
-- Axioms
rec_N :
(P : Nat -> Type) ->
(ind : (n : Nat) -> P n -> P (S n)) ->
(base : P Z) ->
(m : Nat) ->
P m
Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z
succEven : Even n -> Odd (S n)
succOdd : Odd n -> Even (S n)
-- Proof
decideParity : (n : Nat) -> Either (Even n) (Odd n)
decideParity = rec_N P ind base
where
P : (n : Nat) -> Type
P n = Either (Even n) (Odd n)
ind : (n : Nat) -> P n -> P (S n)
ind n (Left p) = Right (succEven p)
ind n (Right p) = Left (succOdd p)
base : P Z
base = Left zeroIsEven
-- Same as above, but replacing Either with (\/) and giving it introduction
-- and elimination axioms similar to the other types being used
-- Axioms
ind_N :
(P : Nat -> Type) ->
(ind : (n : Nat) -> P n -> P (S n)) ->
(base : P Z) ->
(m : Nat) ->
P m
infixl 9 \/
(\/) : {A, B : Type} -> A -> B -> Type
inl : {A, B : Type} -> A -> A \/ B
inr : {A, B : Type} -> B -> A \/ B
rec_or : {A, B, C : Type} -> (A -> C) -> (B -> C) -> (A \/ B) -> C
Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z
succEven : Even n -> Odd (S n)
succOdd : Odd n -> Even (S n)
-- Proof
decideParity : (n : Nat) -> Even n \/ Odd n
decideParity = ind_N P ind base
where
P : (n : Nat) -> Type
P n = Even n \/ Odd n
ind : (n : Nat) -> P n -> P (S n)
ind n = rec_or (inr . succEven) (inl . succOdd)
base : P Z
base = inl zeroIsEven
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment