mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
commit
10fd4e71f8
56
libs/contrib/Data/Nat/Fact.idr
Normal file
56
libs/contrib/Data/Nat/Fact.idr
Normal file
@ -0,0 +1,56 @@
|
||||
||| Properties of factorial functions.
|
||||
module Data.Nat.Fact
|
||||
|
||||
%access public export
|
||||
|
||||
%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
|
Loading…
Reference in New Issue
Block a user