@@ -0,0 +1,56 @@
1+||| Properties of factorial functions.
8+||| Recursive definition of factorial.
11+factRec (S k) = (S k) * factRec k
13+||| Tail-recursive accumulator for factItr.
14+factAcc : Nat -> Nat -> Nat
16+factAcc (S k) acc = factAcc k $ (S k) * acc
18+||| Iterative definition of factorial.
20+factItr n = factAcc n 1
22+----------------------------------------
24+||| Multiplicand-shuffling lemma.
25+multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)
27+ rewrite multAssociative a b c in
28+ rewrite multCommutative a b in
29+ sym $ multAssociative b a c
31+||| Multiplication of the accumulator.
32+factAccMult : (a, b, c : Nat) ->
33+ a * factAcc b c = factAcc b (a * c)
34+factAccMult _ Z _ = Refl
35+factAccMult a (S k) c =
36+ rewrite factAccMult a k (S k * c) in
37+ rewrite multShuffle a (S k) c in
40+||| Addition of accumulators.
41+factAccPlus : (a, b, c : Nat) ->
42+ factAcc a b + factAcc a c = factAcc a (b + c)
43+factAccPlus Z _ _ = Refl
44+factAccPlus (S k) b c =
45+ rewrite factAccPlus k (S k * b) (S k * c) in
46+ rewrite sym $ multDistributesOverPlusRight (S k) b c in
49+||| The recursive and iterative definitions are the equivalent.
50+factRecItr : (n : Nat) -> factRec n = factItr n
53+ rewrite factRecItr k in
54+ rewrite factAccMult k k 1 in
55+ rewrite multOneRightNeutral k in