Reference · Algorithm guarantees

rainbow.algorithms.proofs.factorial

Algorithm guaranteessrc/rainbow/algorithms/proofs/factorial.clj1 definitions, 4 theorems

AHoF factorial n! -- the permutation count underlying combinatorial design sizes, permutation-based search spaces, and Bayesian model-structure counts. Defined by recursion on n, multiplying by the current index at each step: fact 0 = 1 fact (succ n) = (succ n) * fact n. Exact naturals, so the count is proved data. Proved native and axiom-free: the step recurrence (Nat.rec computation rule, which reads the predecessor to form the multiplier), and worked values (0! = 1, 4! = 24, 5! = 120). The enumeration of the permutations themselves is an executable concern; what is proved here is the factorial recurrence and its worked counts. Requires nat and nat/multiply (carried by the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.factorial` prints this classification.

factorial/fact :
  (x₁ : ℕ)
  → ℕ

factorial/fact-step-unfold :
  (n : ℕ)
  → factorial/fact (data/succ n) = nat/multiply (data/succ n) (factorial/fact n)

factorial/fact-zero :
  → factorial/fact 0 = 1

factorial/fact-four :
  → factorial/fact 4 = 24

factorial/fact-five :
  → factorial/fact 5 = 120