Fact.fst

module Fact

open FStar.Mul

val factorial : x:int{x>=0} -> Tot int
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

val fact_tlrec_aux : int -> x:int{x>=0} -> Tot int (decreases x)
let rec fact_tlrec_aux store n =
  if n = 0 then store
  else fact_tlrec_aux (n * store) (n - 1)

val lemma_fact_tlrec_aux_correct : store:int -> n:int{n>=0} -> GTot (u:unit{fact_tlrec_aux store n = store * factorial n}) (decreases n)
let rec lemma_fact_tlrec_aux_correct store n =
  match n with
  | 0 -> ()
  | _ -> lemma_fact_tlrec_aux_correct (n * store) (n - 1)

val fact_tlrec : x:int{x>=0} -> Tot int
let fact_tlrec n = fact_tlrec_aux 1 n

val lemma_fact_tlrec_correct : n:nat ->
    GTot (u:unit{fact_tlrec n == factorial n})
let lemma_fact_tlrec_correct n =
    lemma_fact_tlrec_aux_correct 1 n