diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 13:40:45 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-16 13:40:45 +0000 |
commit | a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 (patch) | |
tree | 07f989e72b672b508e09f820ab3c32a4016698fe /theories/Program/Combinators.v | |
parent | b149e6e21f68d0851f4387dd7182aaca2021041d (diff) |
Reorganize Program and Classes theories. Requiring Setoid no longer sets
implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Combinators.v')
-rw-r--r-- | theories/Program/Combinators.v | 71 |
1 files changed, 71 insertions, 0 deletions
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. |