diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
commit | f402a7969a656eaf71f88c3413b991af1bbfab0a (patch) | |
tree | 9062dbbc1d226762fed5a9c324054c65de4002de | |
parent | af29dd0dc131674d1cb0007d86b2c12500556aad (diff) |
Avoid registering λ and Π as keywords just for some private Local Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Classes/Morphisms.v | 13 | ||||
-rw-r--r-- | theories/Classes/SetoidDec.v | 15 | ||||
-rw-r--r-- | theories/Program/Equality.v | 43 |
3 files changed, 33 insertions, 38 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 9b8301a5d..9a555e256 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -21,12 +21,6 @@ Require Export Coq.Classes.RelationClasses. Generalizable All Variables. Local Obligation Tactic := simpl_relation. -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. @@ -123,15 +117,16 @@ Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x. (** Dependent pointwise lifting of a relation on the range. *) -Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) := - λ f g, Π a : A, sig a (f a) (g a). +Definition forall_relation {A : Type} {B : A -> Type} + (sig : forall a, relation (B a)) : relation (forall x, B x) := + fun f g => forall a, sig a (f a) (g a). Arguments Scope forall_relation [type_scope type_scope signature_scope]. (** Non-dependent pointwise lifting *) Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := - Eval compute in forall_relation (B:=λ _, B) (λ _, R). + Eval compute in forall_relation (B:=fun _ => B) (fun _ => R). Lemma pointwise_pointwise A B (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R). diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 762b3fc7d..6708220ea 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -18,9 +18,6 @@ Unset Strict Implicit. Generalizable Variables A B . -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - (** Export notations. *) Require Export Coq.Classes.SetoidClass. @@ -93,7 +90,7 @@ Program Instance bool_eqdec : EqDec (eq_setoid bool) := bool_dec. Program Instance unit_eqdec : EqDec (eq_setoid unit) := - λ x y, in_left. + fun x y => in_left. Next Obligation. Proof. @@ -101,8 +98,9 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := reflexivity. Qed. -Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) := - λ x y, +Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) + : EqDec (eq_setoid (prod A B)) := + fun x y => let '(x1, x2) := x in let '(y1, y2) := y in if x1 == y1 then @@ -115,8 +113,9 @@ 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. *) -Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := - λ f g, +Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) + : EqDec (eq_setoid (bool -> A)) := + fun f g => if f true == g true then if f false == g false then in_left else in_right diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d678757d9..c41b8bffd 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -13,9 +13,6 @@ Require Export JMeq. Require Import Coq.Program.Tactics. -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - Ltac is_ground_goal := match goal with |- ?T => is_ground T @@ -169,15 +166,15 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. intros. apply proof_irrelevance. Qed. +Proof. apply proof_irrelevance. Qed. -Lemma UIP_refl_refl : Π A (x : A), +Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. -Proof. intros. apply UIP_refl. Qed. +Proof. apply UIP_refl. Qed. -Lemma inj_pairT2_refl : Π A (x : A) (P : A -> Type) (p : P x), +Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. -Proof. intros. apply UIP_refl. Qed. +Proof. apply UIP_refl. Qed. Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. @@ -277,27 +274,31 @@ Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p. (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *) -Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x). -Proof. intros; subst. apply X. Defined. +Lemma solution_left A (B : A -> Type) (t : A) : + B t -> (forall x, x = t -> B x). +Proof. intros; subst; assumption. Defined. -Lemma solution_right : Π A (B : A -> Type) (t : A), B t -> (Π x, t = x -> B x). -Proof. intros; subst; apply X. Defined. +Lemma solution_right A (B : A -> Type) (t : A) : + B t -> (forall x, t = x -> B x). +Proof. intros; subst; assumption. Defined. -Lemma deletion : Π A B (t : A), B -> (t = t -> B). +Lemma deletion A B (t : A) : B -> (t = t -> B). Proof. intros; assumption. Defined. -Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B). -Proof. intros; apply X; apply (JMeq_eq H). Defined. +Lemma simplification_heq A B (x y : A) : + (x = y -> B) -> (JMeq x y -> B). +Proof. intros H J; apply H; apply (JMeq_eq J). Defined. -Lemma simplification_existT2 : Π A (P : A -> Type) B (p : A) (x y : P p), +Lemma simplification_existT2 A (P : A -> Type) B (p : A) (x y : P p) : (x = y -> B) -> (existT P p x = existT P p y -> B). -Proof. intros. apply X. apply inj_pair2. exact H. Defined. +Proof. intros H E. apply H. apply inj_pair2. assumption. Defined. -Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q), +Lemma simplification_existT1 A (P : A -> Type) B (p q : A) (x : P p) (y : P q) : (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B). -Proof. intros. injection H. intros ; auto. Defined. - -Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B eq_refl -> (Π p : x = x, B p). +Proof. injection 2. auto. Defined. + +Lemma simplification_K A (x : A) (B : x = x -> Type) : + B eq_refl -> (forall p : x = x, B p). Proof. intros. rewrite (UIP_refl A). assumption. Defined. (** This hint database and the following tactic can be used with [autounfold] to |