From 94958a408aac22f35165fb3eb571f1c3310f060b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Dec 2016 11:13:15 -0500 Subject: Use [rew] notations rather than [eq_rect] As per Hugo's suggestion in https://github.com/coq/coq/pull/384#issuecomment-264891011 --- theories/Init/Logic.v | 10 +++++----- theories/Init/Specif.v | 29 +++++++++++++++-------------- 2 files changed, 20 insertions(+), 19 deletions(-) (limited to 'theories/Init') diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 968922737..b855154ac 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -654,7 +654,7 @@ Declare Right Step iff_trans. Section ex. Local Unset Implicit Arguments. Definition eq_ex_uncurried' {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1} - (pq : exists p : u1 = v1, eq_rect _ _ u2 _ p = v2) + (pq : exists p : u1 = v1, rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2. Proof. destruct pq as [p q]. @@ -663,7 +663,7 @@ Section ex. Defined. Definition eq_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) - (p : u1 = v1) (q : eq_rect _ _ u2 _ p = v2) + (p : u1 = v1) (q : rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2 := eq_ex_uncurried' P (ex_intro _ p q). @@ -674,13 +674,13 @@ Section ex. := eq_ex' u1 v1 u2 v2 p (P_hprop _ _ _). Lemma eq_rect_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) - : eq_rect x (fun a => ex (Q a)) u y H + : rew [fun a => ex (Q a)] H in u = match u with | ex_intro _ u1 u2 => ex_intro (Q y) - (eq_rect x P u1 y H) - match H in (_ = y) return Q y (eq_rect x P u1 y H) with + (rew H in u1) + match H in (_ = y) return Q y (rew H in u1) with | eq_refl => u2 end end. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6f92358b..cdc918275 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -219,6 +219,7 @@ Proof. Qed. (** Equality of sigma types *) +Import EqNotations. (** Equality for [sigT] *) Section sigT. @@ -230,14 +231,14 @@ Section sigT. (** Projecting an equality of a pair to equality of the second components *) Definition projT2_eq {A} {P : A -> Type} {u v : sigT P} (p : u = v) - : eq_rect _ _ (projT2 u) _ (projT1_eq p) = projT2 v. + : rew projT1_eq p in projT2 u = projT2 v. Proof. destruct p; reflexivity. Defined. (** Equality of [sigT] is itself a [sigT] *) Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : sigT P) - (pq : sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v)) + (pq : sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -248,7 +249,7 @@ Section sigT. (** Curried version of proving equality of sigma types *) Definition eq_sigT {A : Type} {P : A -> Type} (u v : sigT P) - (p : projT1 u = projT1 v) (q : eq_rect _ _ (projT2 u) _ p = projT2 v) + (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v) : u = v := eq_sigT_uncurried u v (existT _ p q). @@ -265,7 +266,7 @@ Section sigT. in dependent positions, we'd need it. *) Definition eq_sigT_uncurried_iff {A P} (u v : @sigT A P) - : u = v <-> (sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v)). + : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)). Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. @@ -292,11 +293,11 @@ Section sigT. (** Classification of transporting across an equality of [sigT]s *) Lemma eq_rect_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sigT (Q x)) {y} (H : x = y) - : eq_rect x (fun a => sigT (Q a)) u y H + : rew [fun a => sigT (Q a)] H in u = existT (Q y) - (eq_rect x P (projT1 u) y H) - match H in (_ = y) return Q y (eq_rect x P (projT1 u) y H) with + (rew H in projT1 u) + match H in (_ = y) return Q y (rew H in projT1 u) with | eq_refl => projT2 u end. Proof. @@ -312,13 +313,13 @@ Section sig. := f_equal (@proj1_sig _ _) p. Definition proj2_sig_eq {A} {P : A -> Prop} {u v : sig P} (p : u = v) - : eq_rect _ _ (proj2_sig u) _ (proj1_sig_eq p) = proj2_sig v. + : rew proj1_sig_eq p in proj2_sig u = proj2_sig v. Proof. destruct p; reflexivity. Defined. Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : sig P) - (pq : {p : proj1_sig u = proj1_sig v | eq_rect _ _ (proj2_sig u) _ p = proj2_sig v}) + (pq : {p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v}) : u = v. Proof. destruct u as [u1 u2], v as [v1 v2]; simpl in *. @@ -328,7 +329,7 @@ Section sig. Defined. Definition eq_sig {A : Type} {P : A -> Prop} (u v : sig P) - (p : proj1_sig u = proj1_sig v) (q : eq_rect _ _ (proj2_sig u) _ p = proj2_sig v) + (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v) : u = v := eq_sig_uncurried u v (exist _ p q). @@ -347,7 +348,7 @@ Section sig. Definition eq_sig_uncurried_iff {A} {P : A -> Prop} (u v : @sig A P) - : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => eq_rect _ _ (proj2_sig u) _ p = proj2_sig v)). + : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => rew p in proj2_sig u = proj2_sig v)). Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ]. Defined. @@ -358,11 +359,11 @@ Section sig. := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v). Lemma eq_rect_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : sig (Q x)) {y} (H : x = y) - : eq_rect x (fun a => sig (Q a)) u y H + : rew [fun a => sig (Q a)] H in u = exist (Q y) - (eq_rect x P (proj1_sig u) y H) - match H in (_ = y) return Q y (eq_rect x P (proj1_sig u) y H) with + (rew H in proj1_sig u) + match H in (_ = y) return Q y (rew H in proj1_sig u) with | eq_refl => proj2_sig u end. Proof. -- cgit v1.2.3