typedef unsigned int uint;

//@rc::inlined
//@ Fixpoint factorial' (n: nat) :=
//@   match n with
//@   | 0 | 1 => 1
//@   | S n'  => n * factorial' n'
//@   end%nat.
//@ Lemma factorial_grows: forall (n: nat), factorial' (S n) >= factorial' n.
//@ Proof.
//@   intros n.
//@   unfold factorial'.
//@   induction n as [|n' Hn'].
//@    - lia.
//@    - lia.
//@ Qed.
//@ Lemma factorial_replace: (forall (n: nat), n > 1 -> n * factorial' (n - 1) = factorial' n)%nat.
//@ Proof.
//@   intros n H.
//@   destruct n as [|n'].
//@    - simpl. lia.
//@    - induction n' as [|n'' Hn''].
//@      + lia.
//@      + simpl. reflexivity.
//@ Qed.
//@rc::end

[[rc::parameters("n: nat"),
  rc::args("n@int<u32>"),
  rc::requires("{factorial' n <= max_int u32}"),
  rc::returns("{factorial' n} @ int<u32>"),
  rc::tactics("unfold factorial'.\
               destruct n as [|n'].\
                -- reflexivity.\
                -- replace n' with 0%nat.\
                  ++ reflexivity.\
                  ++ lia.",
              "destruct n as [|n'].\
                -- unfold factorial'. lia.\
                -- replace (S n' - 1)%nat with n'.\
                  ++ pose proof (factorial_grows n') as Hfg. lia.\
                  ++ lia.",
              "pose proof (factorial_replace n) as Hfr.\
               assert (Hn: (n > 1)%nat) by lia.\
               specialize (Hfr Hn).\
               lia.",
              "pose proof (factorial_replace n) as Hfr.\
               assert (Hn: (n > 1)%nat) by lia.\
               specialize (Hfr Hn).\
               lia."
  )
]] uint
factorial(uint n)
{
	if (n <= 1)
		return 1;
	return n * factorial(n-1);
}