diff options
Diffstat (limited to 'theories/Program')
| -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 |
4 files changed, 152 insertions, 105 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index ddc61a2dc0..d6c276d16a 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 0000000000..e267fbbe20 --- /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 4d92be3c5d..b6c3031e73 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 0000000000..ecdacce64a --- /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 |