0 | ||| Properties of factorial functions
 1 | module Data.Nat.Fact
 2 |
 3 | import Data.Nat
 4 |
 5 | %default total
 6 |
 7 | ||| Recursive definition of factorial.
 8 | factRec : Nat -> Nat
 9 | factRec Z = 1
10 | factRec (S k) = (S k) * factRec k
11 |
12 | ||| Tail-recursive accumulator for factItr.
13 | factAcc : Nat -> Nat -> Nat
14 | factAcc Z acc = acc
15 | factAcc (S k) acc = factAcc k $ (S k) * acc
16 |
17 | ||| Iterative definition of factorial.
18 | factItr : Nat -> Nat
19 | factItr n = factAcc n 1
20 |
21 | ----------------------------------------
22 |
23 | ||| Multiplicand-shuffling lemma.
24 | multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)
25 | multShuffle a b c =
26 |   rewrite multAssociative a b c in
27 |     rewrite multCommutative a b in
28 |       sym $ multAssociative b a c
29 |
30 | ||| Multiplication of the accumulator.
31 | factAccMult : (a, b, c : Nat) ->
32 |   a * factAcc b c = factAcc b (a * c)
33 | factAccMult _ Z _ = Refl
34 | factAccMult a (S k) c =
35 |   rewrite factAccMult a k (S k * c) in
36 |     rewrite multShuffle a (S k) c in
37 |       Refl
38 |
39 | ||| Addition of accumulators.
40 | factAccPlus : (a, b, c : Nat) ->
41 |   factAcc a b + factAcc a c = factAcc a (b + c)
42 | factAccPlus Z _ _ = Refl
43 | factAccPlus (S k) b c =
44 |   rewrite factAccPlus k (S k * b) (S k * c) in
45 |     rewrite sym $ multDistributesOverPlusRight (S k) b c in
46 |       Refl
47 |
48 | ||| The recursive and iterative definitions are the equivalent.
49 | factRecItr : (n : Nat) -> factRec n = factItr n
50 | factRecItr Z = Refl
51 | factRecItr (S k) =
52 |   rewrite factRecItr k in
53 |     rewrite factAccMult k k 1 in
54 |       rewrite multOneRightNeutral k in
55 |         factAccPlus k 1 k
56 |