diff options
| -rw-r--r-- | Makefile.common | 7 | ||||
| -rw-r--r-- | contrib/rtauto/Bintree.v | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 25 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 5 | ||||
| -rw-r--r-- | theories/Classes/Functions.v | 2 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 12 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v (renamed from theories/Classes/Relations.v) | 18 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 2 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 2 | ||||
| -rw-r--r-- | theories/Program/Basics.v | 124 | ||||
| -rw-r--r-- | theories/Program/Combinators.v | 71 | ||||
| -rw-r--r-- | theories/Program/Program.v | 4 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 58 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 4 | ||||
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 6 | ||||
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 4 |
19 files changed, 204 insertions, 164 deletions
diff --git a/Makefile.common b/Makefile.common index 6fe218863..44271647e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -748,7 +748,7 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \ +CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \ theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \ theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo @@ -806,8 +806,9 @@ CCVO:= DPVO:=contrib/dp/Dp.vo SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \ - theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \ - theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo + theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Basics.vo \ + theories/Program/FunctionalExtensionality.vo theories/Program/Combinators.vo \ + theories/Program/Syntax.vo theories/Program/Program.vo RTAUTOVO:= \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v index d410606a7..cd0f1afe9 100644 --- a/contrib/rtauto/Bintree.v +++ b/contrib/rtauto/Bintree.v @@ -107,7 +107,7 @@ intro ne;right;congruence. left;reflexivity. Defined. -Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m). +Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m). fix 1;intros [mm|mm|]. simpl; rewrite pos_eq_dec_refl; reflexivity. simpl; rewrite pos_eq_dec_refl; reflexivity. @@ -116,7 +116,7 @@ Qed. Theorem pos_eq_dec_ex : forall m n, pos_eq m n =true -> exists h:m=n, - pos_eq_dec m n = left h. + pos_eq_dec m n = left _ h. fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence). simpl;intro e. elim (pos_eq_dec_ex _ _ e). diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 8f11989a1..71ab3a5f7 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -360,28 +360,25 @@ let impl = lazy (gen_constant ["Program"; "Basics"] "impl") let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow") let coq_id = lazy (gen_constant ["Program"; "Basics"] "id") -let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive") -let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive") +let reflexive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Reflexive") +let reflexive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "reflexive") -let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric") -let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric") +let symmetric_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Symmetric") +let symmetric_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "symmetric") -let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive") -let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive") +let transitive_type = lazy (gen_constant ["Classes"; "RelationClasses"] "Transitive") +let transitive_proof = lazy (gen_constant ["Classes"; "RelationClasses"] "transitive") -let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse") +let inverse = lazy (gen_constant ["Classes"; "RelationClasses"] "inverse") let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") -let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence") -let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation") +let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence") +let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation") -let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence") -let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence") - -(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *) -let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") +(* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *) +let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") let coq_relation a = mkApp (Lazy.force coq_relation, [| a |]) let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index a19f8da82..052d21019 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -8,7 +8,6 @@ (************************************************************************) (* Typeclass-based setoids, tactics and standard instances. - TODO: explain clrewrite, clsubstitute and so on. Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud @@ -17,10 +16,10 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) Require Export Coq.Program.Basics. -Require Import Coq.Program.Program. +Require Import Coq.Program.Tactics. Require Import Coq.Classes.Init. -Require Export Coq.Classes.Relations. +Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. Require Export Coq.Classes.SetoidTactics. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index c08dee76f..11c60a3aa 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -16,7 +16,7 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) Require Import Coq.Program.Program. -Require Export Coq.Classes.Relations. +Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. Set Implicit Arguments. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 37190ac75..eaf300fd2 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -15,8 +15,9 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) -Require Import Coq.Program.Program. -Require Export Coq.Classes.Relations. +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Export Coq.Classes.RelationClasses. Set Implicit Arguments. Unset Strict Implicit. @@ -53,6 +54,7 @@ Class Morphism A (R : relation A) (m : A) := Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := { morph : A -> B | respectful R R' morph morph }. + Ltac obligations_tactic ::= program_simpl. Program Instance [ Equivalence A R, Equivalence B R' ] => @@ -180,8 +182,6 @@ Hint Resolve @subrelation_morphism 4 : typeclass_instances. (* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *) - - (* Program Instance `A` (R : relation A) `B` (R' : relation B) *) (* [ ? Morphism (R ==> R' ==> iff) m ] => *) (* iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *) @@ -381,7 +381,7 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B) to get an [R y z] goal. *) Program Instance [ ! Transitive A R ] => - trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R. + trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R. Next Obligation. Proof with auto. @@ -390,7 +390,7 @@ Program Instance [ ! Transitive A R ] => Qed. Program Instance [ ! Transitive A R ] => - trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R. + trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. Next Obligation. Proof with auto. diff --git a/theories/Classes/Relations.v b/theories/Classes/RelationClasses.v index 326e97a41..659f9528c 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/RelationClasses.v @@ -17,15 +17,13 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) Require Export Coq.Classes.Init. -Require Import Coq.Program.Program. +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Export Coq.Relations.Relation_Definitions. Set Implicit Arguments. Unset Strict Implicit. -(* Notation "'relation' A " := (A -> A -> Prop) (at level 0). *) - -Definition relation A := A -> A -> Prop. - (** Default relation on a given support. *) Class DefaultRelation A (R : relation A). @@ -35,14 +33,12 @@ Class DefaultRelation A (R : relation A). Definition default_relation [ DefaultRelation A R ] : relation A := R. (** A notation for applying the default relation to [x] and [y]. *) -Notation " x ===def y " := (default_relation x y) (at level 70, no associativity). -Definition inverse A (R : relation A) : relation A := fun x y => R y x. +Notation " x ===def y " := (default_relation x y) (at level 70, no associativity). -Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R. -Proof. intros ; unfold inverse. apply (flip_flip R). Qed. +Definition inverse {A} : relation A -> relation A := flip. -Definition complement A (R : relation A) : relation A := fun x y => R x y -> False. +Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. (** These are convertible. *) @@ -355,7 +351,7 @@ Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] = (** Leibinz equality [eq] is an equivalence relation. *) -Program Instance eq_equivalence : Equivalence A eq. +Program Instance eq_equivalence : Equivalence A (@eq A). (** Logical equivalence [iff] is an equivalence relation. *) diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 9dd4f6181..86e9078e9 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -22,7 +22,7 @@ Require Import Coq.Classes.Init. Set Implicit Arguments. Unset Strict Implicit. -Require Export Coq.Classes.Relations. +Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. Require Export Coq.Classes.Functions. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index c71db6995..9f6dfab42 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -15,7 +15,7 @@ (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) -Require Export Coq.Classes.Relations. +Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. Set Implicit Arguments. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 832829135..6d77a6a0c 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -675,7 +675,7 @@ rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition. Qed. Add Morphism (@MapsTo elt) - with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m. + with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m. Proof. unfold Equal; intros k k' Hk e m m' Hm. rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; @@ -689,19 +689,19 @@ rewrite <-Hm in H0; eauto. rewrite Hm in H0; eauto. Qed. -Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m. +Add Morphism (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m. Proof. intros m m' Hm. rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition. Qed. -Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m. +Add Morphism (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m. Proof. intros k k' Hk m m' Hm. rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition. Qed. -Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m. +Add Morphism (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m. Proof. intros k k' Hk m m' Hm. generalize (find_mapsto_iff m k)(find_mapsto_iff m' k') @@ -713,7 +713,7 @@ symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto. Qed. Add Morphism (@add elt) with signature - E.eq ==> Logic.eq ==> Equal ==> Equal as add_m. + E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m. Proof. intros k k' Hk e m m' Hm y. rewrite add_o, add_o; do 2 destruct eq_dec; auto. @@ -730,7 +730,7 @@ elim n; rewrite <-Hk; auto. elim n; rewrite Hk; auto. Qed. -Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m. +Add Morphism (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m. Proof. intros f m m' Hm y. rewrite map_o, map_o, Hm; auto. @@ -1104,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). End Elt. - Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m. + Add Morphism (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m. Proof. intros; apply Equal_cardinal; auto. Qed. End WProperties. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 27d9c72bd..fc2cc81eb 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *) Definition if_zero (A : Set) (a b : A) (n : N) : A := recursion a (fun _ _ => b) n. -Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd. +Add Morphism (if_zero A) with signature ((@eq (A:Set)) ==> (@eq A) ==> Neq ==> (@eq A)) as if_zero_wd. Proof. intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). reflexivity. unfold fun2_eq; now intros. assumption. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index ddc61a2dc..d6c276d16 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,133 +6,50 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Standard functions and proofs about them. +(* 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 *) (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) -Set Implicit Arguments. -Unset Strict Implicit. +(** The polymorphic identity function. *) -Require Export Coq.Program.FunctionalExtensionality. +Definition id {A} := fun x : A => x. -Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope. +(** Function composition. *) -Open Local Scope program_scope. - -Definition id {A} := λ x : A, x. - -Definition compose {A B C} (g : B -> C) (f : A -> B) := λ x : A , g (f x). +Definition compose {A B C} (f : A -> B) (g : B -> C) := fun x : A => g (f x). Hint Unfold compose. -Notation " g ∘ f " := (compose g f) (at level 50, left associativity) : program_scope. - -Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. -Proof. - intros. - unfold id, compose. - symmetry ; apply eta_expansion. -Qed. +Notation " g ∘ f " := (compose f g) (at level 50, left associativity) : program_scope. -Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. -Proof. - intros. - unfold id, compose. - symmetry ; apply eta_expansion. -Qed. - -Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), - h ∘ g ∘ f = h ∘ (g ∘ f). -Proof. - intros. - reflexivity. -Qed. +Open Local Scope program_scope. -Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. +(** [arrow A B] represents the non-dependent function space between [A] and [B]. *) Definition arrow (A B : Type) := A -> B. +(** [impl A B] represents the logical implication of [B] by [A]. *) + Definition impl (A B : Prop) : Prop := A -> B. -(* Notation " f x " := (f x) (at level 100, x at level 200, only parsing) : program_scope. *) +(** The constant function [const a] always returns [a]. *) -Definition const {A B} (a : A) := fun x : B => a. +Definition const {A B} (a : A) := fun _ : B => a. + +(** The [flip] combinator reverses the first two arguments of a function. *) Definition flip {A B C} (f : A -> B -> C) x y := f y x. -Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f. -Proof. - unfold flip. - intros. - extensionality x ; extensionality y. - reflexivity. -Qed. +(** [apply f x] simply applies [f] to [x]. *) Definition apply {A B} (f : A -> B) (x : A) := f x. -(** Notations for the unit type and value. *) - -Notation " () " := Datatypes.unit : type_scope. -Notation " () " := tt. - -(** Set maximally inserted implicit arguments for standard definitions. *) - -Implicit Arguments eq [[A]]. - -Implicit Arguments Some [[A]]. -Implicit Arguments None [[A]]. - -Implicit Arguments inl [[A] [B]]. -Implicit Arguments inr [[A] [B]]. - -Implicit Arguments left [[A] [B]]. -Implicit Arguments right [[A] [B]]. - -(** Curryfication. *) - -Definition curry {a b c} (f : a -> b -> c) (p : prod a b) : c := - let (x, y) := p in f x y. - -Definition uncurry {a b c} (f : prod a b -> c) (x : a) (y : b) : c := - f (x, y). - -Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f. -Proof. - simpl ; intros. - unfold uncurry, curry. - extensionality x ; extensionality y. - reflexivity. -Qed. - -Lemma curry_uncurry : forall a b c (f : prod a b -> c), curry (uncurry f) = f. -Proof. - simpl ; intros. - unfold uncurry, curry. - extensionality x. - destruct x ; simpl ; reflexivity. -Qed. - -(** 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. - -Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))))) - (at level 200, x ident, y ident, z ident, right associativity) : type_scope. - -Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) - (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. - -Tactic Notation "exist" constr(x) := exists x. -Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. -Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. -Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. - -(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *) -(* (at level 200, x ident, y ident, right associativity) : program_scope. *) +(** Curryfication of [prod] is defined in [Logic.Datatypes]. *) -(* Notation " 'Î ' x : T , p " := (forall x : T, p) *) -(* (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file +Implicit Arguments prod_curry [[A] [B] [C]]. +Implicit Arguments prod_uncurry [[A] [B] [C]]. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v new file mode 100644 index 000000000..e267fbbe2 --- /dev/null +++ b/theories/Program/Combinators.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* 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. + +Open Scope program_scope. + +(** Composition has [id] for neutral element and is associative. *) + +Lemma compose_id_left : forall A B (f : A -> B), id ∘ f = f. +Proof. + intros. + unfold id, compose. + symmetry. apply eta_expansion. +Qed. + +Lemma compose_id_right : forall A B (f : A -> B), f ∘ id = f. +Proof. + intros. + unfold id, compose. + symmetry ; apply eta_expansion. +Qed. + +Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), + h ∘ g ∘ f = h ∘ (g ∘ f). +Proof. + intros. + reflexivity. +Qed. + +Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core. + +(** [flip] is involutive. *) + +Lemma flip_flip : forall A B C, @flip A B C ∘ flip = id. +Proof. + unfold flip, compose. + intros. + extensionality x ; extensionality y ; extensionality z. + reflexivity. +Qed. + +(** [prod_curry] and [prod_uncurry] are each others inverses. *) + +Lemma prod_uncurry_curry : forall A B C, @prod_uncurry A B C ∘ prod_curry = id. +Proof. + simpl ; intros. + unfold prod_uncurry, prod_curry, compose. + extensionality x ; extensionality y ; extensionality z. + reflexivity. +Qed. + +Lemma prod_curry_uncurry : forall A B C, @prod_curry A B C ∘ prod_uncurry = id. +Proof. + simpl ; intros. + unfold prod_uncurry, prod_curry, compose. + extensionality x ; extensionality p. + destruct p ; simpl ; reflexivity. +Qed. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 4d92be3c5..b6c3031e7 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -2,4 +2,6 @@ Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. Require Export Coq.Program.Subset. -Require Export Coq.Program.Basics.
\ No newline at end of file +Require Export Coq.Program.Basics. +Require Export Coq.Program.Combinators. +Require Export Coq.Program.Syntax.
\ No newline at end of file diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v new file mode 100644 index 000000000..ecdacce64 --- /dev/null +++ b/theories/Program/Syntax.v @@ -0,0 +1,58 @@ +(* -*- 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 *) +(************************************************************************) + +(* Custom notations and implicits for Coq prelude definitions. + * + * Author: Matthieu Sozeau + * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud + * 91405 Orsay, France *) + +(** Unicode lambda abstraction, does not work with factorization of lambdas. *) + +Notation " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope. + +(** Notations for the unit type and value. *) + +Notation " () " := Datatypes.unit : type_scope. +Notation " () " := tt. + +(** Set maximally inserted implicit arguments for standard definitions. *) + +Implicit Arguments eq [[A]]. + +Implicit Arguments Some [[A]]. +Implicit Arguments None [[A]]. + +Implicit Arguments inl [[A] [B]]. +Implicit Arguments inr [[A] [B]]. + +Implicit Arguments left [[A] [B]]. +Implicit Arguments right [[A] [B]]. + +(** 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. + +Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))))) + (at level 200, x ident, y ident, z ident, right associativity) : type_scope. + +Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p)))))))) + (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope. + +Tactic Notation "exist" constr(x) := exists x. +Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. +Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. +Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. + +(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *) +(* (at level 200, x ident, y ident, right associativity) : program_scope. *) + +(* Notation " 'Π' x : T , p " := (forall x : T, p) *) +(* (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index cde670075..26638893a 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -775,7 +775,7 @@ Qed. Definition Qpower_positive (q:Q)(p:positive) : Q := pow_pos Qmult q p. -Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp. +Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp. Proof. intros x1 x2 Hx y. unfold Qpower_positive. @@ -794,7 +794,7 @@ Definition Qpower (q:Q) (z:Z) := Notation " q ^ z " := (Qpower q z) : Q_scope. -Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp. +Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp. Proof. intros x1 x2 Hx [|y|y]; try reflexivity; simpl; rewrite Hx; reflexivity. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 8162a702f..3f191c752 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -122,7 +122,7 @@ Qed. Hint Resolve Qceiling_resp_le : qarith. -Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp. +Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp. Proof. intros x y H. apply Zle_antisym. @@ -130,7 +130,7 @@ apply Zle_antisym. symmetry in H; auto with *. Qed. -Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp. +Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp. Proof. intros x y H. apply Zle_antisym. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 61b70ba68..a5ad269d4 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. Inductive le_AsB : A + B -> A + B -> Prop := - | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y) - | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y) - | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y). + | le_aa : forall x y:A, leA x y -> le_AsB (inl _ x) (inl _ y) + | le_ab : forall (x:A) (y:B), le_AsB (inl _ x) (inr _ y) + | le_bb : forall x y:B, leB x y -> le_AsB (inr _ x) (inr _ y). End Disjoint_Union. diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index a86d19c09..f6ce84f98 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -21,7 +21,7 @@ Section Wf_Disjoint_Union. Notation Le_AsB := (le_AsB A B leA leB). - Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x). + Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x). Proof. induction 1. apply Acc_intro; intros y H2. @@ -30,7 +30,7 @@ Section Wf_Disjoint_Union. Qed. Lemma acc_B_sum : - well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x). + well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x). Proof. induction 2. apply Acc_intro; intros y H3. |