(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                   Wf.v                                   *)
(****************************************************************************)

(* This module proves the validity of
    - well-founded recursion (also called course of values)
    - well-founded induction
   from a well-founded ordering on a given set *)

Require Export Logic.

(* Well-founded induction principle on Prop *)

(* The accessibility predicate is defined to be non-informative *)

Inductive  WfTinf_Acc[A:Type;R:A->A->Prop] : A -> Type := 
 WfTinf_Acc_intro : (x:A)((y:A)(R y x)->(WfTinf_Acc A R y))->(WfTinf_Acc A R x).

Lemma WfTinf_Acc_inv : (A:Type)(R:A->A->Prop)
  (x:A)(WfTinf_Acc A R x) -> (y:A)(R y x) -> (WfTinf_Acc A R y).
Destruct 1; Trivial.
Defined.

(* the informative elimination :
   let Acc_rec F = let rec wf x = F x wf in wf *)

Fixpoint WfTinf_Acc_rec' 
    [A:Type;
     R:A->A->Prop;
     P:A->Type;
     F : (x:A)((y:A)(R y x)->(WfTinf_Acc A R y))->
         ((y:A)(R y x)->(P y))->(P x);
     x:A;
     a:(WfTinf_Acc A R x)] : (P x) := 
(F x (WfTinf_Acc_inv A R x a) 
     ([y:A][h:(R y x)](WfTinf_Acc_rec' A R P F y (WfTinf_Acc_inv A R x a y h)))).

(* A relation is well-founded if every element is accessible *)

Definition WfTinf_well_founded := [A:Type][R:A->A->Prop](a:A)(WfTinf_Acc A R a).

Theorem WfTinf_well_founded_induction : 
  (A:Type)(R:A->A->Prop)(WfTinf_well_founded A R) ->
  (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).

Intros.
Unfold WfTinf_well_founded in X.
Apply (WfTinf_Acc_rec' A R P).
Auto.
Trivial.
Qed.

(* Well-founded induction principle on Prop *)

Theorem WfTinf_well_founded_ind : 
  (A:Type)(R:A->A->Prop)(WfTinf_well_founded A R) ->
  (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a).

Intros.
Apply (WfTinf_Acc_rec' A R P).
Auto.
Trivial.
Qed.


(* $Id: WfTinf.v,v 1.2 1998/08/22 10:08:37 stehr Exp $ *)