private: Yes

Set Implicit Arguments.

Require Import Arith.
Require Import Lia.
Require Import Recdef.

(* The factorial function. *)
Fixpoint fact n :=
  match n with
  | 0 => 1
  | S n => (S n) * (fact n)

(* Helper for the inverse factorial. Since it is counting up, we have
   to manually prove that it terminates. For this, we prove that the
   distance between n and a (i.e., n - a) decreases with each
   recursive call. If a was zero it would loop forever, so we reject
   it. *)
Function invfact_i n i a {measure (Nat.sub n) a} :=
  if a =? 0 then None else
    match n ?= a with
    | Lt => None
    | Eq => Some (1 + i)
    | Gt => invfact_i n (1 + i) (a * S (S i))
  apply nat_compare_Gt_gt in teq0.
  apply beq_nat_false in teq.

(* The actual definition of the inverse factorial. *)
Definition invfact n := invfact_i n 0 1.

(* Convenience lemma that reverses a step of computation. *)
Lemma invfact_back: forall n i a,
    a > 0 -> n > a -> invfact_i n (S i) (a * S (S i)) = invfact_i n i a.
  intros. rewrite (invfact_i_equation _ i).
  replace (a =? 0) with false by (symmetry; rewrite Nat.eqb_neq; lia).
  replace (n ?= a) with Gt by (symmetry; now rewrite <- nat_compare_gt).

(* Lemma: if the inverse of a is n, then the inverse of (n+1)*a must
   be n+1. *)
Lemma invfact_step: forall n a,
    n > 0 -> invfact a = Some n -> invfact (S n * a) = Some (S n).
  unfold invfact. intros n a H.
  apply invfact_i_ind; try easy; intros.
  - apply nat_compare_eq in e0. inversion H0. subst.
    rewrite invfact_i_equation.
    rewrite e. apply beq_nat_false in e.
    replace (S (S i) * a0 ?= a0) with Gt by (symmetry; apply nat_compare_gt; lia).
    rewrite invfact_i_equation.
    replace (a0 * S (S i) =? 0) with false by (symmetry; rewrite Nat.eqb_neq; lia).
    now rewrite Nat.mul_comm, Nat.compare_refl. 
  - specialize (H0 H1). apply nat_compare_gt in e0. apply beq_nat_false in e.
    rewrite invfact_back in H0; auto; lia.

(* Theorem: for all n > 0, the inverse of n! is n. *)
Theorem invfact_correct: forall n, n > 0 -> invfact (fact n) = Some n.
  induction n; [easy|]; destruct n; [easy|].
  assert (S n > 0) by lia. specialize (IHn H0).
  replace (fact (S (S n))) with (S (S n) * (fact (S n))) by easy.
  now apply invfact_step.

(* Theorem: our invfact will never produce a zero. *)
Lemma invfact_i_zero: forall n i a, invfact_i n i a <> Some 0.
Proof. intros. apply invfact_i_ind; easy. Qed.

Theorem invfact_zero: forall n, invfact n <> Some 0.
Proof. intros. apply invfact_i_zero. Qed.