The Coq mailing list

[rusu AT irisa.fr]

Hi Russel,

 David Pichardie and I recently came up with this rather simple method for
defining and reasoning about general (non-structural) recursive functions.
We find it quite simple and systematic, and we plan to automate it, but for
now, here is an axample that hopefully shows how to use it.

  Vlad

PS I've been adding comments to a Coq file and do not have access to Coq
to parse it - hopefully haven't introduced any parse errors...
*****************************************************************
(*a simple method for defining general recursive functions*)
(*authors : David Pichardie, Vlad Rusu*)
(*contact : 
{dpichard|rusu}@irisa.fr*)

Require Import Wellfounded.
Require Import Wf_nat.
Require Import Even.
Require Import Div2.

(*example : power of two*)
(*one would like to define it in Coq as follows...*)

(*Fixpoint  pow2 (n: nat) : nat :=
match n with
|0 => 1
|S q =>
   match (even_odd_dec (S q)) with
        |left _ =>  (pow2 (div2 (S q)))*(pow2 (div2 (S q))) (*that's not
very efficient, but*)
        |right _ => n * (pow2 q)                            (*that's not
the point, either*)
   end
end
with measure (fun n:nat => n)
*)

(*here is the idea: *)

(*1. define a relation f_rel, which is the intended graph of the intended
function f*)

(*2. using wellfounded_induction & adequate order, define a function
f_rich with a rich type*)
    (*which basically says that the function satifies its graph f_rel*)
    (*then eliminate the logical information from f_rich, thus obtaining f*)

(*3. using wellfounded_ind & same order, prove that the relation f_rel
defines a unique function f'*)
     (*NB here f' is a function is the usual math sense, it's not
computing anything*)

(*4.  hence, the functions  f and f' are equal in usual maths sense*)
      (*and by construction, f' satisfies the fixpoint equation of f*)
      (*hence, f also satisfies its own fixpoint equation*)

(*5. by copying the induction principle of f_rel you get an indiction
principle for f*)
     (*which can be directly used in proofs*)

(*here is the relation - intended graph ow pow2*)
Inductive pow2_rel : nat -> nat -> Prop :=
|pow2_0_intro : pow2_rel 0 1
| pow2_S_even_intro : forall n q  pow2_p,
  n = S q -> even (S q) ->
               pow2_rel (div2 (S q))  pow2_p -> (pow2_rel (S q)
(pow2_p*pow2_p))
|pow2_S_odd_intro : forall n q pow2_q, n = S q -> odd(S q) ->
                          pow2_rel q pow2_q -> pow2_rel (S q)  (2*pow2_q).

(*a rich type for our function*)
Definition pow2_type (n:nat) :=  {pow2_n: nat | pow2_rel n pow2_n}.

(*auxiliary definition for use with wellfounded_induction*)
(*it says that if you know how to define pow2 for smaller values*)
(*then you know how to define it for the current values. Of course*)
(*a well founded order is assumed, here, it's the usual < on nat*)

Definition pow2_wf  : forall n,  (forall m, m< n -> pow2_type m) ->
pow2_type n.
destruct n.
(* n = 0*)
intros.
unfold pow2_type.
exists 1.
constructor.
(* n = S n*)
intros.
case (even_odd_dec (S n)) ; intros.
(*S n - even *)
unfold pow2_type.
cut (div2 (S n) <  S n) ; intros.
generalize (H _ H0) ; intros.
unfold pow2_type in H1.
elim H1  ; intros.
exists (x*x).
constructor 2 with (S n); auto.
auto with arith.
(*Sn - odd *)
cut (n <  S n) ; intros.
generalize (H _ H0) ; intros.
unfold pow2_type in H1.
elim H1  ; intros.
unfold pow2_type.
exists (2 *x).
constructor 3 with (S n) ; auto.
auto with arith.
Defined.

(*standard use of wellfounded_induction*)
Definition pow2_rich :=
(well_founded_induction  lt_wf   (fun x => pow2_type x) pow2_wf ).

(*getting rid of the rich... type*)
Definition pow2 (n:nat) :  nat :=
let (f,_) := pow2_rich n in f.

(*cf. extraction: function seems to be all right*)
Extraction Inline pow2_rich.
Extraction pow2.


(*next, show that pow2_rel defines some function in the usual math sense*)
(*but first, auxiliary lemma: if that's true for smaller values, it's also*)
(*true for current values. Same well founded order as for definition of*)
(*f_rich should be used, and this proof is quite similar to that definition*)

Lemma pow2_ref_functional_wf : forall x,
 (forall x', x' < x -> forall y1 y2, pow2_rel x' y1 -> pow2_rel x' y2 ->
y1 = y2) ->
forall z1 z2, pow2_rel x z1 -> pow2_rel x z2 -> z1 = z2.
intros.
destruct  H0.
inversion_clear H1 ; auto.
destruct H1.
inversion_clear H3 ; auto with arith.
cut (div2 (S q0) < (S q0)) ; intros.
generalize (H _ H6 _ _ H3 H5) ; intros ; subst ; auto.
auto with arith.
apply False_ind ; eapply not_even_and_odd; eauto.
inversion_clear  H1.
apply False_ind ; eapply not_even_and_odd; eauto.
cut (q < S q) ; intros.
generalize (H _ H1 _ _ H3 H6) ; intros ; subst ; auto.
auto with arith.
Qed.

(*pow2_rel defines a function in usual maths sense*)
Lemma pow2_functional: forall x z1 z2,
pow2_rel x z1 -> pow2_rel x z2 -> z1 = z2.
generalize (well_founded_ind lt_wf
(fun x =>
forall z1 z2, pow2_rel x z1 -> pow2_rel x z2 -> z1 = z2)
pow2_ref_functional_wf
) ; intros.
eapply H ;  eauto.
Qed.


(*next three lemmas for fixpoint equation. Also useful for rewriting*)
(*case: argument = 0*)
Lemma pow2_0 : pow2 0 = 1.
unfold pow2.
unfold sig_rec.
unfold sig_rect.
destruct (pow2_rich 0).
inversion_clear p ; auto.
Qed.
Hint  Resolve pow2_0: base.


(*case: even, non-zero argument*)
Lemma pow2_S_even : forall q,  even (S q)->
 pow2 (S q) = (pow2 (div2 (S q) ))* (pow2 (div2 (S q))).
intros.
unfold pow2.
unfold sig_rec.
unfold sig_rect.
destruct (pow2_rich (S q)).
destruct (pow2_rich (div2 (S q))).
inversion_clear p.
rewrite  (pow2_functional _ _ _ p0 H2) ; auto.
apply False_ind; eapply not_even_and_odd ; eauto.
Qed.
Hint Resolve pow2_S_even: base.

(*case:  odd argument*)
Lemma pow2_S_odd : forall q, odd (S q) ->
 pow2 (S q) =  2* (pow2 ( q)).
intros.
unfold pow2.
unfold sig_rec.
unfold sig_rect.
destruct (pow2_rich (S q)).
destruct (pow2_rich q).
inversion_clear p.
apply False_ind ; eapply not_even_and_odd ; eauto.
rewrite  (pow2_functional _ _ _ p0 H2) ; auto.
Qed.
Hint Resolve pow2_S_odd: base.


(*Fixpoint equation*)
Lemma pow2_fixpoint : forall n, pow2 n  =
match n with
|0 => 1
|S q =>
   match (even_odd_dec (S q)) with
        |left _ =>  (pow2 (div2 (S q))) * (pow2 (div2 (S q)))
        |right _ => 2 * (pow2 q)
   end
end.
intros.
destruct n ; auto with base.
case (even_odd_dec (S n)) ; auto with base.
Qed.


(*let's now define an induction principle for pow2.*)
(*by drawing inspiration from that of pow2_rel, i.e.,*)
Check pow2_rel_ind.


Lemma pow2_ind : forall P : nat ->nat-> Prop,
P 0 (pow2 0) ->

(forall n q,  n = S q  -> even (S q) -> P (div2 (S q)) (pow2 (div2 (S q)))
-> P (S q) ((pow2 (div2 (S q)))* (pow2 (div2 (S q)))))->

(forall n q, n = S q -> odd (S q) -> P q (pow2 q) -> P (S q) (2*pow2 q)) ->

 forall n, P n (pow2 n).
intros.
apply (pow2_rel_ind (fun n _ => P n (pow2 n))) with (pow2 n); intros ; auto.
rewrite pow2_S_even ; auto.
eapply H0 ; eauto.
rewrite pow2_S_odd ; auto.
eapply H1 ; eauto.
unfold pow2.
destruct (pow2_rich n) ; auto.
Qed.


(*exercice : the induction principle has been used; complete the proof!
Lemma pow2_pow2_spec : forall q, pow2 (S q) = 2 *pow2 q.
apply (pow2_ind (fun q _ => pow2 (S q)  = 2 * pow2 q)).
rewrite (pow2_S_odd) ; auto with arith.
intros ; rewrite (pow2_S_odd) ; auto with arith.
intros.
rewrite (pow2_S_even) ; auto with arith.
....*)