ATS proofs about factorial using dataprop

fact_prop.dats

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

dataprop FACT (int, int) =
  | FACTzero (0, 1)
  | {n,r1:int | n > 0} FACTsucc (n, r1 * n) of (FACT (n-1, r1))

fun fact {n:nat} (n: int n): [r:int] (FACT (n, r) | int r) =
  if n > 0 then let
    val (pf1 | r1) = fact (n - 1)
    val r = n * r1
  in
    (FACTsucc (pf1) | r)
  end else begin
    (FACTzero () | 1)
end

prfun factorial_is_positive{n:nat} .<n>.(n: int n):<> [r:int | r > 0] FACT(n,r) =
  case n of
  | 0 => FACTzero()
  | _ =>> FACTsucc(factorial_is_positive (n - 1))

prfun factorial_is_greater_than_arg{n:nat | n > 2} .<n>.(n: int n):<> [r:int | r > n] FACT(n,r) =
  case n of
  | 3 => FACTsucc(FACTsucc(FACTsucc(FACTzero())))
  | _ =>> FACTsucc(factorial_is_greater_than_arg (n - 1))

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