diff options
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | theories/Classes/EquivDec.v | 5 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 | ||||
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 60 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 14 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 16 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 123 | ||||
| -rw-r--r-- | theories/Program/Program.v | 9 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 5 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 16 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 2 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 207 |
12 files changed, 307 insertions, 157 deletions
diff --git a/Makefile.common b/Makefile.common index cefdfd4e19..4ca7e2e45b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -543,7 +543,7 @@ LOGICVO:=$(addprefix theories/Logic/, \ EqdepFacts.vo ProofIrrelevanceFacts.vo ClassicalEpsilon.vo \ ClassicalUniqueChoice.vo DecidableType.vo DecidableTypeEx.vo \ Epsilon.vo ConstructiveEpsilon.vo Description.vo \ - IndefiniteDescription.vo SetIsType.vo ) + IndefiniteDescription.vo SetIsType.vo FunctionalExtensionality.vo ) ARITHVO:=$(addprefix theories/Arith/, \ Arith.vo Gt.vo Between.vo Le.vo \ @@ -740,8 +740,7 @@ CLASSESVO:=$(addprefix theories/Classes/, \ PROGRAMVO:=$(addprefix theories/Program/, \ Tactics.vo Equality.vo Subset.vo Utils.vo \ - Wf.vo Basics.vo FunctionalExtensionality.vo \ - Combinators.vo Syntax.vo Program.vo ) + Wf.vo Basics.vo Combinators.vo Syntax.vo Program.vo ) THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 91c417ce3d..b85d5d7d24 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -115,9 +115,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : Solve Obligations using unfold complement, equiv ; program_simpl. -(** Objects of function spaces with countable domains like bool have decidable equality. *) - -Require Import Coq.Program.FunctionalExtensionality. +(** Objects of function spaces with countable domains like bool have decidable equality. + Proving the reflection requires functional extensionality though. *) Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := equiv_dec f g := diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 5b44f68481..8504a06f43 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -107,8 +107,6 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq (** Objects of function spaces with countable domains like bool have decidable equality. *) -Require Import Coq.Program.FunctionalExtensionality. - Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v new file mode 100644 index 0000000000..865a465534 --- /dev/null +++ b/theories/Logic/FunctionalExtensionality.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. + It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) + +Set Manual Implicit Arguments. + +(** The converse of functional extensionality. *) + +Lemma equal_f : forall {A B : Type} {f g : A -> B}, + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + +(** Statements of functional extensionality for simple and dependent functions. *) + +Axiom functional_extensionality_dep : forall {A} {B : A -> Type}, + forall (f g : forall x : A, B x), + (forall x, f x = g x) -> f = g. + +Lemma functional_extensionality {A B} (f g : A -> B) : + (forall x, f x = g x) -> f = g. +Proof. + intros ; eauto using @functional_extensionality_dep. +Qed. + +(** Apply [functional_extensionality], introducing variable x. *) + +Tactic Notation "extensionality" ident(x) := + match goal with + [ |- ?X = ?Y ] => + (apply (@functional_extensionality _ _ X Y) || + apply (@functional_extensionality_dep _ _ X Y)) ; intro x + end. + +(** Eta expansion follows from extensionality. *) + +Lemma eta_expansion_dep {A} {B : A -> Type} (f : forall x : A, B x) : + f = fun x => f x. +Proof. + intros. + extensionality x. + reflexivity. +Qed. + +Lemma eta_expansion {A B} (f : A -> B) : f = fun x => f x. +Proof. + intros A B f. apply (eta_expansion_dep f). +Qed. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index d304b651f2..9335f48348 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -5,15 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id$ *) -(* Standard functions and combinators. - * Proofs about them require functional extensionality and can be found in [Combinators]. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Standard functions and combinators. + + Proofs about them require functional extensionality and can be found in [Combinators]. -(* $Id$ *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - Université Paris Sud + 91405 Orsay, France *) (** The polymorphic identity function is defined in [Datatypes]. *) diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index e267fbbe20..33ad3b556c 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -5,15 +5,16 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id$ *) -(* Proofs about standard combinators, exports functional extensionality. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Proofs about standard combinators, exports functional extensionality. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) Require Import Coq.Program.Basics. -Require Export Coq.Program.FunctionalExtensionality. +Require Export FunctionalExtensionality. Open Scope program_scope. @@ -40,7 +41,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. +Hint Rewrite @compose_id_left @compose_id_right : core. +Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v deleted file mode 100644 index 8bd2dfb905..0000000000 --- a/theories/Program/FunctionalExtensionality.v +++ /dev/null @@ -1,123 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. - It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. - - It also defines two lemmas for expansion of fixpoint defs using extensionnality and proof-irrelevance - to avoid a side condition on the functionals. *) - -Require Import Coq.Program.Utils. -Require Import Coq.Program.Wf. -Require Import Coq.Program.Equality. - -Set Implicit Arguments. -Unset Strict Implicit. - -(** The converse of functional extensionality. *) - -Lemma equal_f : forall A B : Type, forall (f g : A -> B), - f = g -> forall x, f x = g x. -Proof. - intros. - rewrite H. - auto. -Qed. - -(** Statements of functional extensionality for simple and dependent functions. *) - -Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), - forall (f g : forall x : A, B x), - (forall x, f x = g x) -> f = g. - -Lemma fun_extensionality : forall A B (f g : A -> B), - (forall x, f x = g x) -> f = g. -Proof. - intros ; apply fun_extensionality_dep. - assumption. -Qed. - -Hint Resolve fun_extensionality fun_extensionality_dep : program. - -(** Apply [fun_extensionality], introducing variable x. *) - -Tactic Notation "extensionality" ident(x) := - match goal with - [ |- ?X = ?Y ] => apply (@fun_extensionality _ _ X Y) || apply (@fun_extensionality_dep _ _ X Y) ; intro x - end. - -(** Eta expansion follows from extensionality. *) - -Lemma eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), - f = fun x => f x. -Proof. - intros. - extensionality x. - reflexivity. -Qed. - -Lemma eta_expansion : forall A B (f : A -> B), - f = fun x => f x. -Proof. - intros ; apply eta_expansion_dep. -Qed. - -(** 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 : - forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) - (P : A -> Set) - (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). -Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). - extensionality y ; apply H. - 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. - -(** Tactics to fold/unfold definitions based on [Fix_measure_sub]. *) - -Ltac fold_sub f := - match goal with - | [ |- ?T ] => - match T with - appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => - let app := context C [ f arg ] in - change app - end - end. - -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. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index b6c3031e73..cdfc785837 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,3 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id$ *) + Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index d021326a10..14dc473584 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,14 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id$ *) + +(** Tactics related to subsets and proof irrelevance. *) Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. Open Local Scope program_scope. -(** Tactics related to subsets and proof irrelevance. *) - (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 6cd75257b8..f45511823d 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,14 +5,15 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* $Id$ *) -(* Custom notations and implicits for Coq prelude definitions. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** Custom notations and implicits for Coq prelude definitions. -(** Notations for the unit type and value. *) + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + 91405 Orsay, France *) + +(** Notations for the unit type and value à la Haskell. *) Notation " () " := Datatypes.unit : type_scope. Notation " () " := tt. @@ -42,7 +42,7 @@ Notation " [ ] " := nil : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -(** n-ary exists *) +(** Treating n-ary exists *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) (at level 200, x ident, y ident, right associativity) : type_scope. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index a4eb8bbcc0..fbf0b03cf8 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -8,6 +8,8 @@ (*i $Id$ i*) +(** Various syntaxic shortands that are useful with [Program]. *) + Require Export Coq.Program.Tactics. Set Implicit Arguments. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index b6ba5d44ec..5d005d2739 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id$ *) + +(** Reformulation of the Wf module using subsets where possible, providing + the support for [Program]'s treatment of well-founded definitions. *) + Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. @@ -6,8 +18,6 @@ Open Local Scope program_scope. Implicit Arguments Acc_inv [A R x y]. -(** Reformulation of the Wellfounded module using subsets where possible. *) - Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. @@ -146,3 +156,196 @@ Section Well_founded_measure. End Well_founded_measure. Extraction Inline Fix_measure_F_sub Fix_measure_sub. + +Set Implicit Arguments. + +(** Reasoning about well-founded fixpoints on measures. *) + +Section Measure_well_founded. + + (* Measure relations are well-founded if the underlying relation is well-founded. *) + + Variables T M: Set. + Variable R: M -> M -> Prop. + Hypothesis wf: well_founded R. + Variable m: T -> M. + + Definition MR (x y: T): Prop := R (m x) (m y). + + Lemma measure_wf: well_founded MR. + Proof with auto. + unfold well_founded. + cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a). + intros. + apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). + intros. + apply Acc_intro. + intros. + unfold MR in H1. + rewrite H0 in H1. + apply (H (m y))... + Defined. + +End Measure_well_founded. + +Section Fix_measure_rects. + + Variable A: Set. + 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. + + 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))). + 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 + that property to be invariant over single application of the + function body (f in our case). *) + + Lemma Fix_measure_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). + 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. + simpl. + intros. + rewrite F_unfold... + Qed. + + (* 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 + 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')) -> + f g = f h. + + (* From equiv_lowers, it follows that + [Fix_measure_F_sub A m 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'. + Proof. + intros x a. + pattern x, (Fix_measure_F_sub A m P f x a). + apply Fix_measure_F_sub_rect. + intros. + rewrite F_unfold. + apply equiv_lowers. + intros. + apply H. + assumption. + Qed. + + (* Finally, Fix_measure_F_rect lets one prove a property of + functions defined using Fix_measure_F by showing that + property to be invariant over single application of the function + body (f). *) + + Lemma Fix_measure_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). + Proof with auto. + unfold Fix_measure_sub. + intros. + apply Fix_measure_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))))... + 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))))... + intros. + apply eq_Fix_measure_F_sub. + Qed. + +End Fix_measure_rects. + +(** Tactic to fold a definitions based on [Fix_measure_sub]. *) + +Ltac fold_sub f := + match goal with + | [ |- ?T ] => + match T with + appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => + let app := context C [ f arg ] in + change app + end + end. + +(** This module provides the fixpoint equation provided one assumes + functional extensionality. *) + +Module WfExtensionality. + + Require Import FunctionalExtensionality. + + (** 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 : + forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) + (P : A -> Set) + (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). + Proof. + intros ; apply Fix_eq ; auto. + intros. + assert(f = g). + extensionality y ; apply H. + 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. + +End WfExtensionality. |