(* G54DTP Dependently Typed Programming.
    General Recursion, Bove/Capretta method 
    Venanzio Capretta, March 2011.
*)

(*
  We want to represent the following function in Coq.
  But the argument doesn't decrease in the recursive calls.

  myfun : nat -> nat
  myfun 0 = 0
  myfun 1 = 1
  myfun n = myfun (n/2) + 1   if n is even
  myfun n = myfun (n+1)       if n is odd
*) 

Require Import Arith.
Require Import Even.
Require Import Div2.

(* First we define an inductive constructive predicate
   that characterizes the arguments for which we know
   how to compute the result of the function.
*)

Inductive Dom_myfun: nat -> Set :=
  dmf_zero: Dom_myfun 0
| dmf_one: Dom_myfun 1
| dmf_even: forall n, n>1 -> even n -> Dom_myfun (div2 n) -> Dom_myfun n
| dmf_odd: forall n, n>1 -> odd n -> Dom_myfun (S n) -> Dom_myfun n.

(* dmf_zero and dmf_one say that we know
     how to copute the function on 0 and 1.
   dmf_even says that for an even number larger than one
     we can compute the result if we already know how to compute
     it for (div2 n), that is n divided by two.
   dmf_odd says that for an odd number larger than one
     we can compute the result if we already know ho to compute
     it for n+1.
*)

(* The function ca be defined by recursion
   on a proof h of the domain predicate.
*)

Fixpoint myfun_aux (n:nat)(h:Dom_myfun n): nat :=
match h with
  dmf_zero => O
| dmf_one => S O
| dmf_even n p he h' => S (myfun_aux (div2 n) h')
| dmf_odd n q ho h' => myfun_aux (S n) h'
end.

(* (RecArg n) is a set containing the hypotheses that we need to prove
   to conclude that (Dom_myfun n) holds.
   For 0 and 1 is just unit because we don't need any hypotheses.
*)

Definition RecArg (n:nat): Set :=
if (le_lt_dec n 1)
  then unit
  else if (even_odd_dec n)
         then Dom_myfun (div2 n)
         else Dom_myfun (S n).

(* A "Definition" is just like a Lemma or a Theorem
   but it is used to prove something in Set instead of in Prop.
*)

Definition rec_arg_dom: forall n, RecArg n -> Dom_myfun n.
intros n; unfold RecArg.
case (le_lt_dec n 1).
intro hle1; case (le_lt_eq_dec n 1 hle1).

intro nlt1.
rewrite <- (le_n_O_eq n).
intros; apply dmf_zero.
apply le_S_n.
exact nlt1.

intros h1 _; rewrite h1; apply dmf_one.

intro p; case (even_odd_dec n).
apply dmf_even.
exact p.

apply dmf_odd.
exact p.
Defined.
(* Closing with "Defined" instead of "Qed" tells Coq not to forget
   the proof because it will be needed for computations.
*)

(* We have a uniform proof for the domain predicate:
   change 101 with any other number and the proof still works.
*)

Definition hdmf: Dom_myfun 101.
repeat (apply rec_arg_dom; compute).
exact tt.
Defined.

Eval compute in (myfun_aux 101 hdmf).

(* This is a little property of div2 that we are going to need later. *)

Lemma div2_pos: forall n, n>1 -> div2 n > 0.
Proof.
intro n; case n; simpl.
intro h; elim (lt_n_O 1 h).
intro n'; case n'; simpl.
intro h; apply lt_S_n; exact h.
intros; apply le_n_S.
apply le_O_n.
Qed.

(* The domain predicate is satisfied by every number. *)

Definition dom_myfun_all: forall n, Dom_myfun n.
intro n0.
apply (lt_wf_rec n0 Dom_myfun).

clear n0; intros n IH; apply (rec_arg_dom n).
red.
case (le_lt_dec n 1).
intros; exact tt.
intro h1; case (even_odd_dec n).
intro he; apply IH.
apply lt_div2.

apply lt_S_n.
apply le_S.
exact h1.

intro ho; apply dmf_even.
apply lt_S.
exact h1.
apply even_S; exact ho.
apply IH.
rewrite <- odd_div2.
rewrite (odd_double n ho) at 2.
apply lt_n_S.
apply plus_lt_compat_r with (n:=0).

apply div2_pos.
exact h1.
exact ho.
Defined.

(* Now we can define the function without the extra argument. *)

Definition myfun (n:nat): nat := myfun_aux n (dom_myfun_all n).

Eval compute in (myfun 101).