diff options
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 305 |
1 files changed, 105 insertions, 200 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 2083e530..98b1c619 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -22,140 +22,57 @@ Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. Hypothesis Rwf : well_founded R. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := - F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) - (Acc_inv r (proj2_sig y))). - - Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - - Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. - - Lemma Fix_F_eq : - forall (x:A) (r:Acc R x), - F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. - Proof. - destruct r using Acc_inv_dep; auto. - Qed. - - Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. - Proof. - intro x; induction (Rwf x); intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. - Qed. - - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)). - Proof. - intro x; unfold Fix in |- *. - rewrite <- (Fix_F_eq ). - apply F_ext; intros. - apply Fix_F_inv. - Qed. - - Lemma fix_sub_eq : - forall x : A, - Fix_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun (y : A | R y x) => Fix (`y)). - exact Fix_eq. - Qed. - - End FixPoint. -End Well_founded. + Variable P : A -> Type. -Extraction Inline Fix_F_sub Fix_sub. + Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. -Require Import Wf_nat. -Require Import Lt. + Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x := + F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) + (Acc_inv r (proj2_sig y))). -Section Well_founded_measure. - Variable A : Type. - Variable m : A -> nat. - - Section Acc. - - Variable P : A -> Type. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. - - Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y - (@Acc_inv _ _ _ r (m y) (proj2_sig y))). - - Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). - - End Acc. - - Section FixPoint. - Variable P : A -> Type. - - Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x. - - Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) - - Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). - - Hypothesis - F_ext : - forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)), - (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. - - Program Lemma Fix_measure_F_eq : - forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r. - Proof. - intros x. - set (y := m x). - unfold Fix_measure_F_sub. - intros r ; case r ; auto. - Qed. - - Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. - Proof. - intros x r s. - rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. - Qed. - - Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). - Proof. - intro x; unfold Fix_measure in |- *. - rewrite <- (Fix_measure_F_eq ). - apply F_ext; intros. - apply Fix_measure_F_inv. - Qed. - - Lemma fix_measure_sub_eq : forall x : A, - Fix_measure_sub P F_sub x = - let f_sub := F_sub in - f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)). - exact Fix_measure_eq. - Qed. - - End FixPoint. - -End Well_founded_measure. - -Extraction Inline Fix_measure_F_sub Fix_measure_sub. + Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + + (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) + (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), + (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. + + Lemma Fix_F_eq : + forall (x:A) (r:Acc R x), + F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + + Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. + Proof. + intro x; induction (Rwf x); intros. + rewrite (proof_irrelevance (Acc R x) r s) ; auto. + Qed. + + Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)). + Proof. + intro x; unfold Fix_sub in |- *. + rewrite <- (Fix_F_eq ). + apply F_ext; intros. + apply Fix_F_inv. + Qed. + + Lemma fix_sub_eq : + forall x : A, + Fix_sub x = + let f_sub := F_sub in + f_sub x (fun (y : A | R y x) => Fix_sub (`y)). + exact Fix_eq. + Qed. + +End Well_founded. + +Extraction Inline Fix_F_sub Fix_sub. Set Implicit Arguments. @@ -189,38 +106,40 @@ Section Measure_well_founded. End Measure_well_founded. -Section Fix_measure_rects. +Hint Resolve measure_wf. + +Section Fix_rects. Variable A: Type. - Variable m: A -> nat. Variable P: A -> Type. - Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x. - + Variable R : A -> A -> Prop. + Variable Rwf : well_founded R. + Variable f: forall (x : A), (forall y: { y: A | R y x }, P (proj1_sig y)) -> P x. + Lemma F_unfold x r: - Fix_measure_F_sub A m P f x r = - f (fun y => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv r (proj2_sig y))). + Fix_F_sub A R P f x r = + f (fun y => Fix_F_sub A R P f (proj1_sig y) (Acc_inv r (proj2_sig y))). Proof. intros. case r; auto. Qed. - (* Fix_measure_F_sub_rect lets one prove a property of - functions defined using Fix_measure_F_sub by showing + (* Fix_F_sub_rect lets one prove a property of + functions defined using Fix_F_sub by showing that property to be invariant over single application of the function body (f in our case). *) - Lemma Fix_measure_F_sub_rect + Lemma Fix_F_sub_rect (Q: forall x, P x -> Type) (inv: forall x: A, - (forall (y: A) (H: MR lt m y x) (a: Acc lt (m y)), - Q y (Fix_measure_F_sub A m P f y a)) -> - forall (a: Acc lt (m x)), - Q x (f (fun y: {y: A | m y < m x} => - Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) - : forall x a, Q _ (Fix_measure_F_sub A m P f x a). + (forall (y: A) (H: R y x) (a: Acc R y), + Q y (Fix_F_sub A R P f y a)) -> + forall (a: Acc R x), + Q x (f (fun y: {y: A | R y x} => + Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) + : forall x a, Q _ (Fix_F_sub A R P f x a). Proof with auto. - intros Q inv. - set (R := fun (x: A) => forall a, Q _ (Fix_measure_F_sub A m P f x a)). - cut (forall x, R x)... - apply (well_founded_induction_type (measure_wf lt_wf m)). - subst R. + set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)). + cut (forall x, R' x)... + apply (well_founded_induction_type Rwf). + subst R'. simpl. intros. rewrite F_unfold... @@ -229,29 +148,29 @@ Section Fix_measure_rects. (* Let's call f's second parameter its "lowers" function, since it provides it access to results for inputs with a lower measure. - In preparation of lemma similar to Fix_measure_F_sub_rect, but - for Fix_measure_sub, we first + In preparation of lemma similar to Fix_F_sub_rect, but + for Fix_sub, we first need an extra hypothesis stating that the function body has the same result for different "lowers" functions (g and h below) as long as those produce the same results for lower inputs, regardless of the lt proofs. *) Hypothesis equiv_lowers: - forall x0 (g h: forall x: {y: A | m y < m x0}, P (proj1_sig x)), - (forall x p p', g (exist (fun y: A => m y < m x0) x p) = h (exist _ x p')) -> + forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)), + (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) -> f g = f h. (* From equiv_lowers, it follows that - [Fix_measure_F_sub A m P f x] applications do not not + [Fix_F_sub A R P f x] applications do not not depend on the Acc proofs. *) - Lemma eq_Fix_measure_F_sub x (a a': Acc lt (m x)): - Fix_measure_F_sub A m P f x a = - Fix_measure_F_sub A m P f x a'. + Lemma eq_Fix_F_sub x (a a': Acc R x): + Fix_F_sub A R P f x a = + Fix_F_sub A R P f x a'. Proof. - intros x a. - pattern x, (Fix_measure_F_sub A m P f x a). - apply Fix_measure_F_sub_rect. + revert a'. + pattern x, (Fix_F_sub A R P f x a). + apply Fix_F_sub_rect. intros. rewrite F_unfold. apply equiv_lowers. @@ -260,40 +179,42 @@ Section Fix_measure_rects. assumption. Qed. - (* Finally, Fix_measure_F_rect lets one prove a property of - functions defined using Fix_measure_F by showing that + (* Finally, Fix_F_rect lets one prove a property of + functions defined using Fix_F_sub by showing that property to be invariant over single application of the function body (f). *) - Lemma Fix_measure_sub_rect + Lemma Fix_sub_rect (Q: forall x, P x -> Type) (inv: forall (x: A) - (H: forall (y: A), MR lt m y x -> Q y (Fix_measure_sub A m P f y)) - (a: Acc lt (m x)), - Q x (f (fun y: {y: A | m y < m x} => Fix_measure_sub A m P f (proj1_sig y)))) - : forall x, Q _ (Fix_measure_sub A m P f x). + (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y)) + (a: Acc R x), + Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y)))) + : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. - unfold Fix_measure_sub. + unfold Fix_sub. intros. - apply Fix_measure_F_sub_rect. + apply Fix_F_sub_rect. intros. - assert (forall y: A, MR lt m y x0 -> Q y (Fix_measure_F_sub A m P f y (lt_wf (m y))))... + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))... set (inv x0 X0 a). clearbody q. - rewrite <- (equiv_lowers (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (lt_wf (m (proj1_sig y)))) (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... + rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => + Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) + (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... intros. - apply eq_Fix_measure_F_sub. + apply eq_Fix_F_sub. Qed. -End Fix_measure_rects. +End Fix_rects. (** Tactic to fold a definition based on [Fix_measure_sub]. *) Ltac fold_sub f := match goal with - | [ |- ?T ] => + | [ |- ?T ] => match T with - appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => + appcontext C [ @Fix_sub _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end @@ -308,7 +229,7 @@ Module WfExtensionality. (** The two following lemmas allow to unfold a well-founded fixpoint definition without restriction using the functional extensionality axiom. *) - + (** For a function defined with Program using a well-founded order. *) Program Lemma fix_sub_eq_ext : @@ -317,7 +238,7 @@ Module WfExtensionality. (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y). + F_sub x (fun (y : A | R y x) => Fix_sub A R Rwf P F_sub y). Proof. intros ; apply Fix_eq ; auto. intros. @@ -326,26 +247,10 @@ Module WfExtensionality. rewrite H0 ; auto. Qed. - (** For a function defined with Program using a measure. *) - - Program Lemma fix_sub_measure_eq_ext : - forall (A : Type) (f : A -> nat) (P : A -> Type) - (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x), - forall x : A, - Fix_measure_sub A f P F_sub x = - F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y). - Proof. - intros ; apply Fix_measure_eq ; auto. - intros. - assert(f0 = g). - extensionality y ; apply H. - rewrite H0 ; auto. - Qed. - - (** Tactic to unfold once a definition based on [Fix_measure_sub]. *) - - Ltac unfold_sub f fargs := - set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; - rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. + (** Tactic to unfold once a definition based on [Fix_sub]. *) + + Ltac unfold_sub f fargs := + set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; + rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. End WfExtensionality. |