Port over some contrib stuff

I didn't add any export labels because none of this is actually useful
for anything, but the proofs are cool.

libs/contrib/Data/Logic/Propositional.idr

@@ -0,0 +1,160 @@
+module Data.Logic.Propositional
+
+%default total
+
+-- Idris uses intuitionistic logic, so it does not validate the
+-- principle of excluded middle (PEM) or similar theorems of classical
+-- logic. But it does validate certain relations among these
+-- propositions, and that's what's in this file.
+
+||| The principle of excluded middle
+PEM : Type -> Type
+PEM p = Either p (Not p)
+
+||| Double negation elimination
+DNE : Type -> Type
+DNE p = Not $ Not p -> p
+
+||| The consensus theorem (at least, the interesting part)
+Consensus : Type -> Type -> Type -> Type
+Consensus p q r = (q, r) -> Either (p, q) (Not p, r)
+
+||| Peirce's law
+Peirce : Type -> Type -> Type
+Peirce p q = ((p -> q) -> p) -> p
+
+||| Not sure if this one has a name, so call it Frege's law
+Frege : Type -> Type -> Type -> Type
+Frege p q r = (p -> r) -> (q -> r) -> ((p -> q) -> q) -> r
+
+||| The converse of contraposition: (p -> q) -> Not q -> Not p
+Transposition : Type -> Type -> Type
+Transposition p q = (Not q -> Not p) -> p -> q
+
+||| This isn't a good name.
+Switch : Type -> Type
+Switch p = (Not p -> p) -> p
+
+-- PEM and the others can't be proved outright, but it is possible to
+-- prove the double negations (DN) of all of them.
+
+||| The double negation of a proposition
+DN : Type -> Type
+DN p = Not $ Not p
+
+pemDN : DN $ PEM p
+pemDN f = f $ Right $ \x => f $ Left x
+
+dneDN : DN $ DNE p
+dneDN f = f $ \g => void $ g $ \x => f $ \_ => x
+
+consensusDN : DN $ Consensus p q r
+consensusDN f = f $ \(y, z) => Right (\x => f $ \(_, _) => Left (x, y), z)
+
+peirceDN : DN $ Peirce p q
+peirceDN f = f $ \g => g $ \x => void $ f $ \_ => x
+
+fregeDN : DN $ Frege p q r
+fregeDN f = f $ \g, h, i => h $ i $ \x => void $ f $ \_, _, _ => g x
+
+transpositionDN : DN $ Transposition p q
+transpositionDN f = f $ \g, x => void $ g (\y => f $ \_, _ => y) x
+
+switchDN : DN $ Switch p
+switchDN f = f $ \g => g $ \x => f $ \_ => x
+
+-- It's easy to prove all these theorems assuming PEM.
+
+dnePEM : PEM p -> DNE p
+dnePEM (Left l) _ = l
+dnePEM (Right r) f = void $ f r
+
+consensusPEM : PEM p -> Consensus p q r
+consensusPEM (Left l) (y, _) = Left (l, y)
+consensusPEM (Right r) (_, z) = Right (r, z)
+
+peircePEM : PEM p -> Peirce p q
+peircePEM (Left l) _ = l
+peircePEM (Right r) f = f $ \x => void $ r x
+
+fregePEM : PEM p -> Frege p q r
+fregePEM (Left l) f _ _ = f l
+fregePEM (Right r) _ g h = g $ h $ \x => void $ r x
+
+transpositionPEM : PEM p -> Transposition q p
+transpositionPEM (Left l) _ _ = l
+transpositionPEM (Right r) f x = void $ f r x
+
+switchPEM : PEM p -> Switch p
+switchPEM (Left l) _ = l
+switchPEM (Right r) f = f r
+
+-- It's trivial to prove these theorems assuming double negation
+-- elimination (DNE), since their double negations can all be proved.
+
+||| Eliminate double negations
+EDN : DN p -> DNE p -> p
+EDN f g = g f
+
+pemDNE : DNE $ PEM p -> PEM p
+pemDNE = EDN pemDN
+
+-- It's possible to prove the theorems assuming Peirce's law, but some
+-- thought must be given to choosing the right instances. Peirce's law
+-- is therefore weaker than PEM on an instance-by-instance basis, but
+-- all the instances together are equivalent.
+
+pemPeirce : Peirce (PEM p) Void -> PEM p
+pemPeirce f = f $ \g => Right $ \x => g $ Left x
+
+dnePeirce : Peirce p Void -> DNE p
+dnePeirce f g = f $ \h => void $ g h
+
+consensusPeirce : Peirce (Consensus p q r) Void -> Consensus p q r
+consensusPeirce f (y, z) =
+  f (\g, (_, _) => Right (\x => g (\_ => Left (x, y)), z)) (y, z)
+
+fregePeirce : Peirce (Frege p q r) Void -> Frege p q r
+fregePeirce f g h i =
+  f (\j, _, _, _ => h $ i $ \x => void $ j $ \_, _, _ => g x) g h i
+
+transpositionPeirce : Peirce (Transposition p q) Void -> Transposition p q
+transpositionPeirce f g x =
+  f (\h, _, _ => void $ g (\y => h $ \_, _ => y) x) (\j, _ => g j x) x
+
+-- There are a variety of single axioms sufficient for deriving all of
+-- classical logic. The earliest of these is known as Nicod's axiom,
+-- but it is written using only nand operators and doesn't lend itself
+-- to Idris's type system. Meredith's axiom, on the other hand, is
+-- written using implication and negation.
+
+||| Meredith's axiom, sufficient for deriving all of classical logic
+Meredith : (p, q, r, s, t : Type) -> Type
+Meredith p q r s t =
+  ((((p -> q) -> Not r -> Not s) -> r) -> t) -> (t -> p) -> s -> p
+
+-- The Meredith axiom implies all of classical logic, and so in
+-- particular it implies PEM, and therefore cannot be proved in
+-- intuitionistic logic. As usual, however, its double negation can be
+-- proved.
+
+meredithDN : DN $ Meredith p q r s t
+meredithDN f =
+  f $ \g, h, x =>
+    h $ g $ \i =>
+      void $ i
+        (\y => void $ f $ \_, _, _ => y)
+        (\z => f $ \_, _, _ => h $ g $ \_ => z)
+        x
+
+-- Meredith can be proved assuming PEM, since the type system itself
+-- takes care of the rest.
+
+meredithPEM : PEM p -> Meredith p q r s t
+meredithPEM (Left l) _ _ _ = l
+meredithPEM (Right r) f g x =
+  g $ f $ \h =>
+    void $ h
+      (\y => void $ r y)
+      (\z => r $ g $ f (\_ => z))
+      x

libs/contrib/Data/Nat/Ack.idr

@@ -0,0 +1,58 @@
+||| Properties of Ackermann functions
+module Data.Nat.Ack
+
+%default total
+
+-- Primitive recursive functions are functions that can be calculated
+-- by programs that don't use unbounded loops. Almost all common
+-- mathematical functions are primitive recursive.
+
+-- Uncomputable functions are functions that can't be calculated by
+-- any programs at all. One example is the Busy Beaver function:
+--   BB(k) = the maximum number of steps that can be executed by a
+--           halting Turing machine with k states.
+-- The values of the Busy Beaver function are unimaginably large for
+-- any but the smallest inputs.
+
+-- The Ackermann function is the most well-known example of a total
+-- computable function that is not primitive recursive, i.e. a general
+-- recursive function. It grows strictly faster than any primitive
+-- recursive function, but also strictly slower than a function like
+-- the Busy Beaver.
+
+-- There are many variations of the Ackermann function. Here is one
+-- common definition
+-- (see https://sites.google.com/site/pointlesslargenumberstuff/home/2/ackermann)
+-- that uses nested recursion:
+
+ackRec : Nat -> Nat -> Nat
+-- Base rule
+ackRec Z m = S m
+-- Prime rule
+ackRec (S k) Z = ackRec k 1
+-- Catastrophic rule
+ackRec (S k) (S j) = ackRec k $ ackRec (S k) j
+
+-- The so-called "base rule" and "prime rule" work together to ensure
+-- termination. Happily, the Idris totality checker has no issues.
+
+-- An unusual "repeating" defintion of the function is given in the
+-- book The Little Typer:
+
+ackRep : Nat -> Nat -> Nat
+ackRep Z = (+) 1
+ackRep (S k) = repeat (ackRep k)
+  where
+    repeat : (Nat -> Nat) -> Nat -> Nat
+    repeat f Z = f 1
+    repeat f (S k) = f (repeat f k)
+
+-- These two definitions don't look like they define the same
+-- function, but they do:
+
+ackRepRec : (n, m : Nat) -> ackRep n m = ackRec n m
+ackRepRec Z _ = Refl
+ackRepRec (S k) Z = ackRepRec k 1
+ackRepRec (S k) (S j) =
+  rewrite sym $ ackRepRec (S k) j in
+    ackRepRec k $ ackRep (S k) j

libs/contrib/Data/Nat/Fact.idr

@@ -0,0 +1,56 @@
+||| Properties of factorial functions
+module Data.Nat.Fact
+
+import Data.Nat
+
+%default total
+
+||| Recursive definition of factorial.
+factRec : Nat -> Nat
+factRec Z = 1
+factRec (S k) = (S k) * factRec k
+
+||| Tail-recursive accumulator for factItr.
+factAcc : Nat -> Nat -> Nat
+factAcc Z acc = acc
+factAcc (S k) acc = factAcc k $ (S k) * acc
+
+||| Iterative definition of factorial.
+factItr : Nat -> Nat
+factItr n = factAcc n 1
+
+----------------------------------------
+
+||| Multiplicand-shuffling lemma.
+multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)
+multShuffle a b c =
+  rewrite multAssociative a b c in
+    rewrite multCommutative a b in
+      sym $ multAssociative b a c
+
+||| Multiplication of the accumulator.
+factAccMult : (a, b, c : Nat) ->
+  a * factAcc b c = factAcc b (a * c)
+factAccMult _ Z _ = Refl
+factAccMult a (S k) c =
+  rewrite factAccMult a k (S k * c) in
+    rewrite multShuffle a (S k) c in
+      Refl
+
+||| Addition of accumulators.
+factAccPlus : (a, b, c : Nat) ->
+  factAcc a b + factAcc a c = factAcc a (b + c)
+factAccPlus Z _ _ = Refl
+factAccPlus (S k) b c =
+  rewrite factAccPlus k (S k * b) (S k * c) in
+    rewrite sym $ multDistributesOverPlusRight (S k) b c in
+      Refl
+
+||| The recursive and iterative definitions are the equivalent.
+factRecItr : (n : Nat) -> factRec n = factItr n
+factRecItr Z = Refl
+factRecItr (S k) =
+  rewrite factRecItr k in
+    rewrite factAccMult k k 1 in
+      rewrite multOneRightNeutral k in
+        factAccPlus k 1 k

libs/contrib/Data/Nat/Fib.idr

@@ -0,0 +1,50 @@
+||| Properties of Fibonacci functions
+module Data.Nat.Fib
+
+import Data.Nat
+
+%default total
+
+||| Recursive definition of Fibonacci.
+fibRec : Nat -> Nat
+fibRec Z = Z
+fibRec (S Z) = S Z
+fibRec (S (S k)) = fibRec (S k) + fibRec k
+
+||| Accumulator for fibItr.
+fibAcc : Nat -> Nat -> Nat -> Nat
+fibAcc Z a _ = a
+fibAcc (S k) a b = fibAcc k b (a + b)
+
+||| Iterative definition of Fibonacci.
+fibItr : Nat -> Nat
+fibItr n = fibAcc n 0 1
+
+||| Addend shuffling lemma.
+plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
+plusLemma a b c d =
+  rewrite sym $ plusAssociative a b (c + d) in
+    rewrite plusAssociative b c d in
+      rewrite plusCommutative b c in
+        rewrite sym $ plusAssociative c b d in
+          plusAssociative a c (b + d)
+
+||| Helper lemma for fibacc.
+fibAdd : (n, a, b, c, d : Nat) ->
+  fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)
+fibAdd Z _ _ _ _ = Refl
+fibAdd (S Z) _ _ _ _ = Refl
+fibAdd (S (S k)) a b c d =
+  rewrite fibAdd k (a + b) (b + (a + b)) (c + d) (d + (c + d)) in
+    rewrite plusLemma b (a + b) d (c + d) in
+      rewrite plusLemma a b c d in
+        Refl
+
+||| Iterative and recursive Fibonacci definitions are equivalent.
+fibEq : (n : Nat) -> fibRec n = fibItr n
+fibEq Z = Refl
+fibEq (S Z) = Refl
+fibEq (S (S k)) =
+  rewrite fibEq k in
+    rewrite fibEq (S k) in
+      fibAdd k 1 1 0 1

libs/contrib/contrib.ipkg

@@ -11,8 +11,15 @@ modules = Control.Delayed,
           Data.List.Palindrome,
 
           Data.Fin.Extra,
+
+          Data.Logic.Propositional,
+
+          Data.Nat.Ack,
           Data.Nat.Equational,
+          Data.Nat.Fact,
           Data.Nat.Factor,
+          Data.Nat.Fib,
+
           Data.SortedMap,
           Data.SortedSet,
           Data.String.Extra,