diff options
Diffstat (limited to 'theories/Init/Wf.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Wf.v | 99 |
1 files changed, 50 insertions, 49 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 7ab3723d..fde70225 100755..100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,61 +6,59 @@ (* * 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*) +(*i $Id: Wf.v 8642 2006-03-17 10:09:02Z notin $ 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 *) + from a well-founded ordering on a given set *) + +Set Implicit Arguments. Require Import Notations. Require Import Logic. Require Import Datatypes. -(** Well-founded induction principle on Prop *) +(** Well-founded induction principle on [Prop] *) Section Well_founded. - Variable A : Set. + Variable A : Type. 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. + Inductive Acc (x: A) : Prop := + Acc_intro : (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 : + (** 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. + 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)). + F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)). End AccRecType. Definition Acc_rec (P:A -> Set) := Acc_rect P. - (** A simplified version of Acc_rec(t) *) + (** A simplified version of [Acc_rect] *) Section AccIter. - Variable P : A -> Type. + 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)). + F (fun (y:A) (h:R y x) => Acc_iter (Acc_inv a h)). End AccIter. @@ -68,7 +66,7 @@ Section Well_founded. Definition well_founded := forall a:A, Acc a. - (** well-founded induction on Set and Prop *) + (** Well-founded induction on [Set] and [Prop] *) Hypothesis Rwf : well_founded. @@ -95,47 +93,48 @@ Section Well_founded. (** Building fixpoints *) -Section FixPoint. + 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)). + Variable P : A -> Type. + Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. -Definition Fix (x:A) := Fix_F (Rwf x). + Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *) -(** Proof that [well_founded_induction] satisfies the fixpoint equation. - It requires an extra property of the functional *) + Definition Fix (x:A) := Acc_iter P F (Rwf x). -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. + (** Proof that [well_founded_induction] satisfies the fixpoint equation. + It requires an extra property of the functional *) -Scheme Acc_inv_dep := Induction for Acc Sort Prop. + 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. -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. + Scheme Acc_inv_dep := Induction for Acc Sort Prop. -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_F_eq : + forall (x:A) (r:Acc x), + F (fun (y:A) (p:R y x) => Fix_F y (Acc_inv r p)) = Fix_F x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. + Proof. + 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. + Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y). + Proof. + intro x; unfold Fix in |- *. + rewrite <- (Fix_F_eq (x:=x)). + apply F_ext; intros. + apply Fix_F_inv. + Qed. -End FixPoint. + End FixPoint. End Well_founded. @@ -169,3 +168,5 @@ Section Well_founded_2. Defined. End Well_founded_2. + +Notation Fix_F := Acc_iter (only parsing). (* compatibility *) |