ATS proofs about factorial using threaded Z3 proofs

fact_z3_threaded.dats

// ATS factorial proof examples, based on F* tutorial examples at:
// https://www.fstar-lang.org/tutorial/
//
// patsopt -tc --constraint-export -d fact_z3_threaded.dats |patsolve_z3 -i
//
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

stacst fact: int -> int

extern praxi fact_base(): [fact(0) == 1] void
extern praxi fact_ind{n:pos}(): [fact(n)==n*fact(n-1)] void

fun fact {n:nat} (n: int n): int (fact(n)) = 
 if n > 0 then let
      prval () = fact_ind {n} ()
    in
      n * fact(n - 1)
    end
  else let
      prval () = fact_base()
     in
       1
     end

prfun factorial_is_positive{n:nat} .<n>.(n: int n):<> [fact(n) > 0] void =
  case n of
  | 0 => let 
           prval () = fact_base()
          in
          ()
         end
  | _ =>> let
           prval () = fact_ind {n} ()
         in
           factorial_is_positive (n - 1)
         end

prfun factorial_is_greater_than_arg{n:nat | n > 2} .<n>.(n: int n):<> [fact(n) > n] void =
  case n of
  | 3 => let
           prval () = fact_base()
           prval () = fact_ind {1} ()
           prval () = fact_ind {2} ()
           prval () = fact_ind {3} ()
          in
          ()
         end
  | _ =>> let
           prval () = fact_ind {n} ()
         in
           factorial_is_greater_than_arg (n - 1)
         end

implement main0() = let
  val r = fact(5)  
in
  println!("5! = ", r)
end