Skip to content

Instantly share code, notes, and snippets.

@mgritter
Last active November 10, 2021 18:01
Show Gist options
  • Save mgritter/462d81d678609423b0059b632f76c528 to your computer and use it in GitHub Desktop.
Save mgritter/462d81d678609423b0059b632f76c528 to your computer and use it in GitHub Desktop.
An F* program for computing factorial sums
module Factorial
open FStar.Mul // Give us * for multiplication instead of pairs
open FStar.IO
open FStar.Printf
let rec factorial (n:nat) : nat =
if n = 0 then 1
else n * factorial (n-1)
let rec sum (min:nat) (max:nat) (f:nat -> nat) : Tot nat (decreases max) =
if max < min then 0
else if max = min then f( min )
else (f max) + sum min (max-1) f
let rec sum_of_factorial_aux (n:nat) (k:nat{ k <= n}) (k_factorial:nat) (accum:nat): Tot nat (decreases (n-k))
= if k = n then accum + k_factorial
else sum_of_factorial_aux n (k+1) ((k+1) * k_factorial) (accum + k_factorial)
let rec sum_of_factorial_lemma (n:nat) (k:nat{k <= n && 1 <= k})
: Lemma (ensures sum_of_factorial_aux n k (factorial k) (sum 1 (k-1) factorial) =
(sum 1 n factorial))
(decreases (n-k))
= if n = k
then ()
else sum_of_factorial_lemma n (k+1)
val sum_of_factorials (n:nat{n >= 1}) : Tot (x:nat{x == sum 1 n factorial})
let sum_of_factorials n =
sum_of_factorial_lemma n 1;
sum_of_factorial_aux n 1 1 0
let _ =
let n = input_int() in
if n >= 1 then
print_string (sprintf "%d\n" (sum_of_factorials n))
else
print_string "Bad input\n"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment