Inductive types, recursion and fuel in F*

Sandbox.fst

module Sandbox

#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"

type unat = 
  | Z : unat
  | S : (prev: unat) -> unat
   
#set-options "--ifuel 1 --fuel 0"
let rec unat_to_nat (x: unat) : nat = 
  match x with
  | Z -> 0
  | S s -> 1 + unat_to_nat s  

#set-options "--ifuel 0 --fuel 2" 
let _ = assert (unat_to_nat (S Z) == 1) 
 
#set-options "--ifuel 1 --fuel 0"
let order_lemma (x: unat) 
  : Lemma (requires S? x)
          (ensures S? x /\ ((S?.prev x) << x)) = ()
  
let nonzero_unat_lemma (x:unat)
  : Lemma ((x =!= Z) <==> S? x) = ()
  
#set-options "--ifuel 0 --fuel 0" 
let rec unat_to_nat_zerofuel (x: unat) : nat =   
  nonzero_unat_lemma x;
  match x with
  | Z -> 0
  | _ -> order_lemma x;
        1 + unat_to_nat_zerofuel (S?.prev x) 
 
let _ = assert_norm (unat_to_nat_zerofuel (S Z) == 1) 
let _ = assert_norm (unat_to_nat (S Z) == 1)