(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

Set Implicit Arguments.

(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)

(** 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 Import Notations.
Require Import Logic.
Require Import Datatypes.

(** Well-founded induction principle on Prop *)

Section Well_founded.

 Variable A : Set.
 Variable R : A -> A -> Prop.

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

 Inductive Acc : A -> Prop :=
     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.

 Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
  destruct 1; trivial.
 Defined.

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

 Section AccRecType.
  Variable P : A -> Type.
  Variable
    F :
      forall x:A,
        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.

  Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).

 End AccRecType.

 Definition Acc_rec (P:A -> Set) := Acc_rect P.

 (** A simplified version of Acc_rec(t) *)

 Section AccIter.
  Variable P : A -> Type. 
  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.

  Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).

 End AccIter.

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

 Definition well_founded := forall a:A, Acc a.

 (** well-founded induction on Set and Prop *)

 Hypothesis Rwf : well_founded.

 Theorem well_founded_induction_type :
  forall P:A -> Type,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  intros; apply (Acc_iter P); auto.
 Defined.

 Theorem well_founded_induction :
  forall P:A -> Set,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  exact (fun P:A -> Set => well_founded_induction_type P).
 Defined.

 Theorem well_founded_ind :
  forall P:A -> Prop,
    (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 Proof.
  exact (fun P:A -> Prop => well_founded_induction_type P).
 Defined.

(** Building fixpoints  *) 

Section FixPoint.

Variable P : A -> Set.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.

Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).

Definition Fix (x:A) := Fix_F (Rwf x).

(** Proof that [well_founded_induction] satisfies the fixpoint equation. 
    It requires an extra property of the functional *)

Hypothesis
  F_ext :
    forall (x:A) (f g:forall y:A, R y x -> P y),
      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.

Scheme Acc_inv_dep := Induction for Acc Sort Prop.

Lemma Fix_F_eq :
 forall (x:A) (r:Acc x),
   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
destruct r using Acc_inv_dep; auto.
Qed.

Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
intro x; induction (Rwf x); intros.
rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
apply F_ext; auto.
Qed.


Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
intro x; unfold Fix in |- *.
rewrite <- (Fix_F_eq (x:=x)).
apply F_ext; intros.
apply Fix_F_inv.
Qed.

End FixPoint.

End Well_founded. 

(** A recursor over pairs *)

Section Well_founded_2.

  Variables A B : Set.
  Variable R : A * B -> A * B -> Prop.

  Variable P : A -> B -> Type. 
  Variable
    F :
      forall (x:A) (x':B),
        (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.

  Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
   P x x' :=
    F
      (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).

  Hypothesis Rwf : well_founded R.

  Theorem well_founded_induction_type_2 :
   (forall (x:A) (x':B),
      (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
   forall (a:A) (b:B), P a b.
  Proof.
   intros; apply Acc_iter_2; auto.
  Defined.

End Well_founded_2.