TheEvolutionOfACoqProgrammer.v

(** * Draft: The evolution of a Coq programmer *)

(** ** Freshman Coq programmer *)
Fixpoint fac n :=
  match n with
  | O => 1
  | S p => n * fac p
  end.

(* begin hide *) Reset fac. (* end hide *)


(** ** General Recursion by Iteration *)
Require Import Arith.
Fixpoint iter {A:Set} (n:nat) (F:A->A) (g:A) :=
  match n with
  | 0 => g
  | S p => F (iter p F g)
  end.

Definition fac_it_F (f: nat -> nat)(n: nat) :=
  match Nat.eq_dec n 0 with
  | left _ => 1
  | right _ => n * f (n-1)
  end.

Definition fac_it_terminates:
  forall n:nat, {y | exists p:nat,
                    forall k:nat, p<k -> forall g:nat->nat,
                        iter k fac_it_F g n = y}.
  intros n. induction n using (well_founded_induction lt_wf).
  case_eq (Nat.eq_dec n 0); intros eq_neq Heq_test.
  - (* n = 0 のとき *)
    exists 1. exists 0. intros k. case k; [now auto|].
    intros k' Hlt g. subst n. now unfold fac_it_F.
  - (* n <> 0 のとき *)
    destruct H with (y := n-1) as [y Hex]; [now destruct n; auto with arith |].
    exists (n * y). destruct Hex as [p IH'].
    exists (S p). intros k. case k.
    + now auto with arith.
    + intros k' Hlt g. simpl. unfold fac_it_F at 1.
      simpl. rewrite Heq_test.
      f_equal.
      rewrite IH'; [reflexivity|].
      now auto with arith.
Defined.

Definition fac_it n :=
  let (y, _) := fac_it_terminates n in
  y.

Theorem fac_it_fix_eqn : forall n,
    fac_it n = match Nat.eq_dec n 0 with
            | left H => 1
            | right H =>
              n * fac_it (n-1)
            end.
Proof.
  intros n. unfold fac_it. destruct (fac_it_terminates n) as [v [p Hp]].
  destruct (fac_it_terminates (n-1)) as [v' [p' Hp']].
  rewrite <- Hp with (k := S (S (max p p')))(g := fun x => v).
  - rewrite <- Hp' with (k := S (max p p'))(g := fun x => v); [reflexivity |].
    now apply le_lt_n_Sm, Nat.le_max_r.
  - now apply Nat.lt_lt_succ_r, le_lt_n_Sm, Nat.le_max_l.
Qed.



(* begin hide *) Reset fac. (* end hide *)


(** ** Recursion on an Ad Hoc predicate *)
Inductive fac_domain : nat -> Prop :=
| fac_domain_1 : fac_domain 1
| fac_domain_2 : forall n,
  n <> 0 -> n <> 1 -> fac_domain (n - 1) -> fac_domain n.

Lemma fac_domain_inv :
  forall n, fac_domain n -> n <> 0 -> n <> 1 -> fac_domain (n-1).
Proof.
  intros n dom. now destruct dom.
Defined.

Fixpoint fac (n: nat) (h: fac_domain n) {struct h} : nat.
  refine
    (match n as x return n = x -> nat with
     | 0 => (fun h' => False_rec nat _)
     | 1 => (fun h' => 1)
     | S (S p) => (fun h' =>
         n * fac (n - 1) _)
     end _).
  - subst n. now inversion h.
  - subst n. now apply fac_domain_inv.
  - reflexivity.
Defined.