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 --- doc/Makefile | 2 +- doc/refman/AddRefMan-pre.tex | 10 +- doc/refman/Program.tex | 6 +- doc/refman/RefMan-add.tex | 6 ++ doc/stdlib/Library.tex | 2 + doc/stdlib/index-list.html.template | 12 +++ doc/stdlib/make-library-files | 2 +- doc/stdlib/make-library-index | 2 +- 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 ++++++++++++++++++++++++++++ 14 files changed, 245 insertions(+), 225 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 diff --git a/doc/Makefile b/doc/Makefile index 143fc2e29f..99e075f0a5 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -214,7 +214,7 @@ faq/html/index.html: faq/FAQ.v.html GLOBDUMP=$(COQTOP)/glob.dump -LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals +LIBDIRS= Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Program # We avoid Strings as String.v contains unicode caracters that make latex fail LIBDIRS+= Ints Ints/num diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex index 15776690ce..85811c1450 100644 --- a/doc/refman/AddRefMan-pre.tex +++ b/doc/refman/AddRefMan-pre.tex @@ -28,6 +28,11 @@ Manual. files from $\FW$ terms. It is contributed by Jean-Christophe Filliâtre and Pierre Letouzey. +\item[Program] This chapter explains the use of the \texttt{Program} + vernacular which allows the development of certified + programs in \Coq. It is contributed by Matthieu Sozeau and replaces + the previous \texttt{Program} tactic by Catherine Parent. + %\item[Natural] This chapter is due to Yann Coscoy. It is the user % manual of the tools he wrote for printing proofs in natural % language. At this time, French and English languages are supported. @@ -35,11 +40,6 @@ Manual. \item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole class of arithmetic problems. -%\item[Program] The \texttt{Program} technology intends to inverse the -% extraction mechanism. It allows the developments of certified -% programs in \Coq. This chapter is due to Catherine Parent. {\bf This -% feature is not available in {\Coq} version 7.} - \item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This chapter explains how to use it and how it works. The chapter is contributed by Patrick Loiseleur. diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index c564346a4e..7d70a7205f 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -211,9 +211,9 @@ tactic is replaced by the default one if not specified. obligations (does not work with structurally recursive programs). \end{itemize} -The module {\tt Coq.subtac.Utils} defines the default tactic for solving -obligations called {\tt subtac\_simpl}. Importing it also adds some -useful notations, as documented in the file itself. +The module {\tt Coq.Program.Tactics} defines the default tactic for solving +obligations called {\tt program\_simpl}. Importing +{\tt Coq.Program.Program} also adds some useful notations, as documented in the file itself. %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex index e21070d14e..52746fad6e 100644 --- a/doc/refman/RefMan-add.tex +++ b/doc/refman/RefMan-add.tex @@ -21,6 +21,12 @@ extract ML program files. It is described in the separate document {\tt Extraction.dvi} \index{Extraction of programs} +\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}} +{\tt Program} is a package offering some special facilities to +extract ML program files. It is described in the separate document +{\tt Program.dvi} +\index{Program-ing} + \section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}} {\tt Natural} is a tool to print proofs in natural language. It is described in the separate document {\tt Natural.dvi}. diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index fffcddc853..81fdd2a6ea 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -45,6 +45,8 @@ The standard library is composed of the following subdirectories: \item[Wellfounded] Well-founded relations (basic results). \item[IntMap] Representation of finite sets by an efficient structure of map (trees indexed by binary integers). + \item[Program] Tactcis to deal with dependently-typed programs and + their proofs. \end{description} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 2a8693438b..65d69a1d8e 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -402,5 +402,17 @@ through the Require Import command.

theories/Ints/num/ZnZ.v + +
Program: + Support for dependently-typed programming. +
+
+ theories/Program/Wf.v + theories/Program/Equality.v + theories/Program/Tactics.v + theories/Program/Utils.v + theories/Program/Program.v + theories/Program/FunctionalExtensionality.v +
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index 91e3cc3f45..6eb1333a5e 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -10,7 +10,7 @@ # En supposant que make fait son boulot, ca fait un tri topologique du # graphe des dépendances -LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids" +LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids Program" rm -f library.files.ls.tmp (cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index cbcd15ef33..27dfc434f1 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -7,7 +7,7 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num" +LIBDIRS="Init Logic Bool Arith NArith ZArith QArith Relations Sets Setoids Lists Sorting Wellfounded IntMap FSets Reals Ints Ints/num Program" for k in $LIBDIRS; do i=../theories/$k 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