From a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 16 Mar 2008 13:40:45 +0000 Subject: 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 --- theories/Program/Basics.v | 124 +++++++---------------------------------- theories/Program/Combinators.v | 71 +++++++++++++++++++++++ theories/Program/Program.v | 4 +- theories/Program/Syntax.v | 58 +++++++++++++++++++ 4 files changed, 152 insertions(+), 105 deletions(-) create mode 100644 theories/Program/Combinators.v create mode 100644 theories/Program/Syntax.v (limited to 'theories/Program') 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 *) (* 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 *) +(* 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 *) +(* 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 -- cgit v1.2.3