diff options
Diffstat (limited to 'theories/Init/Wf.v')
| -rw-r--r-- | theories/Init/Wf.v | 69 |
1 files changed, 31 insertions, 38 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 4e0f3745..f46b2b11 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,12 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ i*) +(*i $Id: Wf.v 10712 2008-03-23 11:38:38Z herbelin $ i*) -(** This module proves the validity of - - well-founded recursion (also called course of values) +(** * This module proves the validity of + - well-founded recursion (also known as course of values) - well-founded induction - from a well-founded ordering on a given set *) Set Implicit Arguments. @@ -40,6 +39,7 @@ Section Well_founded. [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. @@ -51,17 +51,6 @@ Section Well_founded. Definition Acc_rec (P:A -> Set) := Acc_rect P. - (** A simplified version of [Acc_rect] *) - - 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 (Acc_inv a h)). - - End AccIter. - (** A relation is well-founded if every element is accessible *) Definition well_founded := forall a:A, Acc a. @@ -74,7 +63,7 @@ Section Well_founded. 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. + intros; apply Acc_rect; auto. Defined. Theorem well_founded_induction : @@ -91,16 +80,26 @@ Section Well_founded. exact (fun P:A -> Prop => well_founded_induction_type P). Defined. -(** Building fixpoints *) +(** Well-founded fixpoints *) Section FixPoint. Variable P : A -> Type. Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. - Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *) + Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x := + F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)). + + 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 (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. - Definition Fix (x:A) := Acc_iter P F (Rwf x). + 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 *) @@ -110,16 +109,7 @@ Section Well_founded. 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 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. + Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s. Proof. intro x; induction (Rwf x); intros. rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros. @@ -129,7 +119,7 @@ Section Well_founded. 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)). + rewrite <- Fix_F_eq. apply F_ext; intros. apply Fix_F_inv. Qed. @@ -138,27 +128,29 @@ Section Well_founded. End Well_founded. -(** A recursor over pairs *) +(** Well-founded fixpoints over pairs *) Section Well_founded_2. - Variables A B : Set. + Variables A B : Type. Variable R : A * B -> A * B -> Prop. Variable P : A -> B -> Type. - Section Acc_iter_2. + Section FixPoint_2. + 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} : + Fixpoint Fix_F_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)). - End Acc_iter_2. + Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)). + + End FixPoint_2. Hypothesis Rwf : well_founded R. @@ -167,9 +159,10 @@ Section Well_founded_2. (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. + intros; apply Fix_F_2; auto. Defined. End Well_founded_2. -Notation Fix_F := Acc_iter (only parsing). (* compatibility *) +Notation Acc_iter := Fix_F (only parsing). (* compatibility *) +Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *) |