From ea3763f3bc406dd3257e1d8ec4d489a0790ae713 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 8 Aug 2007 13:14:05 +0000 Subject: A better Program documentation. Include it in the generated stdlib doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Program/Equality.v | 63 ++++++++++++ theories/Program/FixSub.v | 148 ---------------------------- theories/Program/FunctionalExtensionality.v | 2 +- theories/Program/Heq.v | 63 ------------ theories/Program/Program.v | 4 +- theories/Program/Wf.v | 148 ++++++++++++++++++++++++++++ 6 files changed, 214 insertions(+), 214 deletions(-) create mode 100644 theories/Program/Equality.v delete mode 100644 theories/Program/FixSub.v delete mode 100644 theories/Program/Heq.v create mode 100644 theories/Program/Wf.v (limited to 'theories/Program') diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v new file mode 100644 index 0000000000..cd405219f6 --- /dev/null +++ b/theories/Program/Equality.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tac H + end. + +(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) + +Ltac simpl_one_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H) ; clear H ; rename H' into H). + +(** Repeat it for every possible hypothesis. *) + +Ltac simpl_JMeq := repeat simpl_one_JMeq. + +(** Just simplify an h.eq. without clearing it. *) + +Ltac simpl_one_dep_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H)). + +Require Import Eqdep. + +(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *) + +Ltac elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. + diff --git a/theories/Program/FixSub.v b/theories/Program/FixSub.v deleted file mode 100644 index 58ac9d90ee..0000000000 --- a/theories/Program/FixSub.v +++ /dev/null @@ -1,148 +0,0 @@ -Require Import Wf. -Require Import Coq.Program.Utils. -Require Import ProofIrrelevance. - -(** 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. diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index c6e5a64fb3..40356a9c49 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -1,5 +1,5 @@ Require Import Coq.Program.Utils. -Require Import Coq.Program.FixSub. +Require Import Coq.Program.Wf. (** The converse of functional equality. *) diff --git a/theories/Program/Heq.v b/theories/Program/Heq.v deleted file mode 100644 index cd405219f6..0000000000 --- a/theories/Program/Heq.v +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tac H - end. - -(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) - -Ltac simpl_one_JMeq := - on_JMeq - ltac:(fun H => let H' := fresh "H" in - assert (H' := JMeq_eq H) ; clear H ; rename H' into H). - -(** Repeat it for every possible hypothesis. *) - -Ltac simpl_JMeq := repeat simpl_one_JMeq. - -(** Just simplify an h.eq. without clearing it. *) - -Ltac simpl_one_dep_JMeq := - on_JMeq - ltac:(fun H => let H' := fresh "H" in - assert (H' := JMeq_eq H)). - -Require Import Eqdep. - -(** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *) - -Ltac elim_eq_rect := - match goal with - | [ |- ?t ] => - match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. - diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 4dc50694fa..39c5b77341 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,3 +1,3 @@ Require Export Coq.Program.Utils. -Require Export Coq.Program.FixSub. -Require Export Coq.Program.Heq. \ No newline at end of file +Require Export Coq.Program.Wf. +Require Export Coq.Program.Equality. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v new file mode 100644 index 0000000000..55784671f5 --- /dev/null +++ b/theories/Program/Wf.v @@ -0,0 +1,148 @@ +Require Import Coq.Init.Wf. +Require Import Coq.Program.Utils. +Require Import ProofIrrelevance. + +(** 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. -- cgit v1.2.3