diff options
Diffstat (limited to 'theories/Init/Wf.v')
| -rwxr-xr-x | theories/Init/Wf.v | 129 |
1 files changed, 71 insertions, 58 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index ee7da4ba67..476ec4a547 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -7,7 +7,6 @@ (***********************************************************************) Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. (*i $Id$ i*) @@ -17,24 +16,24 @@ V7only [Unset Implicit Arguments.]. from a well-founded ordering on a given set *) -Require Notations. -Require Logic. -Require Datatypes. +Require Import Notations. +Require Import Logic. +Require Import Datatypes. (** Well-founded induction principle on Prop *) -Chapter Well_founded. +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 : (x:A)((y:A)(R y x)->(Acc y))->(Acc x). + Inductive Acc : A -> Prop := + Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x. - Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y). - NewDestruct 1; Trivial. + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. + destruct 1; trivial. Defined. (** the informative elimination : @@ -42,50 +41,56 @@ Chapter Well_founded. Section AccRecType. Variable P : A -> Type. - Variable F : (x:A)((y:A)(R y x)->(Acc y))->((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)] : (P x) - := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rect y (Acc_inv x a y h)))). + 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). + Definition Acc_rec (P:A -> Set) := Acc_rect P. (** A simplified version of Acc_rec(t) *) Section AccIter. Variable P : A -> Type. - Variable F : (x:A)((y:A)(R y x)-> (P y))->(P x). + Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. - Fixpoint Acc_iter [x:A;a:(Acc x)] : (P x) - := (F x ([y:A][h:(R y x)](Acc_iter y (Acc_inv x a y h)))). + 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 := (a:A)(Acc a). + Definition well_founded := forall a:A, Acc a. (** well-founded induction on Set and Prop *) Hypothesis Rwf : well_founded. - Theorem well_founded_induction_type : - (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). + 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. + intros; apply (Acc_iter P); auto. Defined. Theorem well_founded_induction : - (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). + forall P:A -> Set, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. Proof. - Exact [P:A->Set](well_founded_induction_type P). + exact (fun P:A -> Set => well_founded_induction_type P). Defined. - Theorem well_founded_ind : - (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). + 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 [P:A->Prop](well_founded_induction_type P). + exact (fun P:A -> Prop => well_founded_induction_type P). Defined. (** Building fixpoints *) @@ -93,40 +98,41 @@ Chapter Well_founded. Section FixPoint. Variable P : A -> Set. -Variable F : (x:A)((y:A)(R y x)->(P y))->(P x). +Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. -Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := - (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))). +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 x (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 *) -Hypothesis F_ext : - (x:A)(f,g:(y:A)(R y x)->(P y)) - ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g). +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 - : (x:A)(r:(Acc x)) - (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r). -NewDestruct r using Acc_inv_dep; Auto. +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 : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s). -Intro x; NewInduction (Rwf x); Intros. -Rewrite <- (Fix_F_eq x r); Rewrite <- (Fix_F_eq x s); Intros. -Apply F_ext; Auto. +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 : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). -Intro x; Unfold fix. -Rewrite <- (Fix_F_eq x). -Apply F_ext; Intros. -Apply Fix_F_inv. +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. @@ -135,24 +141,31 @@ End Well_founded. (** A recursor over pairs *) -Chapter Well_founded_2. +Section Well_founded_2. - Variable A,B : Set. + Variables A B : Set. Variable R : A * B -> A * B -> Prop. Variable P : A -> B -> Type. - Variable F : (x:A)(x':B)((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'))] : (P x x') - := (F x x' ([y:A][y':B][h:(R (y,y') (x,x'))](Acc_iter_2 y y' (Acc_inv ? ? (x,x') a (y,y') h)))). - - Hypothesis Rwf : (well_founded ? R). - - Theorem well_founded_induction_type_2 : - ((x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))->(P y y'))->(P x x'))->(a:A)(b:B)(P a b). + 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. + intros; apply Acc_iter_2; auto. Defined. End Well_founded_2. - |