(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 Wf_nat.v                                 *)
(****************************************************************************)
(* Well-founded relations and natural numbers *)

(*Require WfT.*)
Require Lt.

Chapter  Well_founded_Nat.

Variable A : Set.

Variable f : A -> nat.
Definition ltof := [a,b:A](lt (f a) (f b)).
Definition gtof := [a,b:A](gt (f b) (f a)).

Theorem well_founded_ltof : (WfT_well_founded A ltof).
Proof.
Red.
Cut (n:nat)(a:A)(lt (f a) n)->(WfT_Acc A ltof a).
Intros H a;  Apply (H (S (f a))); Auto with v62.
Induction n.
Intros; Absurd (lt (f a) O); Auto with v62.
Intros m Hm a ltSma.
Apply WfT_Acc_intro.
Unfold ltof; Intros b ltfafb.
Apply Hm.
Apply lt_le_trans with (f a); Auto with v62.
Qed.

Theorem  well_founded_gtof : (WfT_well_founded A gtof).
Proof well_founded_ltof.

(* It is possible to directly prove the induction principle going
   back to primitive recursion on natural numbers (induction_ltof1)
   or to use the previous lemmas to extract a program with a fixpoint
   (induction_ltof2) 
the ML-like program for induction_ltof1 is :
   let induction_ltof1 F a = indrec ((f a)+1) a 
   where rec indrec = 
        function 0    -> (function a -> error)
               |(S m) -> (function a -> (F a (function y -> indrec y m)));;
the ML-like program for induction_ltof2 is :
   let induction_ltof2 F a = indrec a
   where rec indrec a = F a indrec;;
*)

Theorem induction_ltof1 : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
Proof.
Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
Intros H a;  Apply (H (S (f a))); Auto with v62.
Induction n.
Intros; Absurd (lt (f a) O); Auto with v62.
Intros m Hm a ltSma.
Apply F.
Unfold ltof; Intros b ltfafb.
Apply Hm.
Apply lt_le_trans with (f a); Auto with v62.
Qed. 

Theorem induction_gtof1 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
Proof induction_ltof1.

Theorem induction_ltof2 
   : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
Proof (WfT_well_founded_induction A ltof well_founded_ltof).

Theorem induction_gtof2 : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
Proof induction_ltof2.

End Well_founded_Nat.

Lemma lt_wf : (WfT_well_founded nat lt).
Proof (well_founded_ltof nat [m:nat]m).

Lemma lt_wf_rec1 : (p:nat)(P:nat->Set)
              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Proof [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
     (induction_ltof1 nat [m:nat]m P F p).

Lemma lt_wf_rec : (p:nat)(P:nat->Set)
              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Proof [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
     (induction_ltof2 nat [m:nat]m P F p).

Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
              ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
Intros; Elim (lt_wf p); Auto with v62.
Save.

Lemma gt_wf_rec : (p:nat)(P:nat->Set)
              ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
Proof lt_wf_rec.

Lemma gt_wf_ind : (p:nat)(P:nat->Prop)
              ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
Proof lt_wf_ind.

Lemma lt_wf_double_rec : 
  (P:nat->nat->Set)
  ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
   -> (p,q:nat)(P p q).
Intros P Hrec p; Pattern p; Apply lt_wf_rec.
Intros; Pattern q; Apply lt_wf_rec; Auto with v62.
Save.

Lemma lt_wf_double_ind : 
  (P:nat->nat->Prop)
  ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
   -> (p,q:nat)(P p q).
Intros P Hrec p; Pattern p; Apply lt_wf_ind.
Intros; Pattern q; Apply lt_wf_ind; Auto with v62.
Save.


(* $Id: WfT_nat.v,v 1.1 1998/07/01 22:19:38 stehr Exp $ *)