diff options
Diffstat (limited to 'contrib/subtac/FixSub.v')
-rw-r--r-- | contrib/subtac/FixSub.v | 147 |
1 files changed, 0 insertions, 147 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v deleted file mode 100644 index f047b729..00000000 --- a/contrib/subtac/FixSub.v +++ /dev/null @@ -1,147 +0,0 @@ -Require Import Wf. -Require Import Coq.subtac.Utils. - -(** Reformulation of the Wellfounded module using subsets where possible. *) - -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 (proj1_sig y) (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:{ 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:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (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 <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. - apply F_ext; auto. - intros. - rewrite (proof_irrelevance (Acc R x) r s) ; auto. - Qed. - - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{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. - -Extraction Inline Fix_F_sub Fix_sub. - -Require Import Wf_nat. -Require Import Lt. - -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. - - Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (m (proj1_sig 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. - - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig 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. - - Lemma Fix_measure_F_eq : - forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (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. |