diff options
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Specif.v | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e1d8991d1..2b4cc745f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -220,6 +220,12 @@ Qed. (** Equality of sigma types *) Import EqNotations. +Local Notation "'rew' 'dependent' [ Q ] H 'in' H'" + := (match H as p in (_ = y) return Q y (rew p in _) with + | eq_refl => H' + end) + (at level 10, H' at level 10, + format "'[' 'rew' 'dependent' [ Q ] '/ ' H in '/' H' ']'"). (** Equality for [sigT] *) Section sigT. @@ -303,9 +309,7 @@ Section sigT. = existT (Q y) (rew H in projT1 u) - match H in (_ = y) return Q y (rew H in projT1 u) with - | eq_refl => projT2 u - end. + (rew dependent [Q] H in (projT2 u)). Proof. destruct H, u; reflexivity. Defined. @@ -376,9 +380,7 @@ Section sig. = exist (Q y) (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. + (rew dependent [Q] H in proj2_sig u). Proof. destruct H, u; reflexivity. Defined. @@ -492,12 +494,8 @@ Section sigT2. (Q y) (R y) (rew H in projT1 u) - match H in (_ = y) return Q y (rew H in projT1 u) with - | eq_refl => projT2 u - end - match H in (_ = y) return R y (rew H in projT1 u) with - | eq_refl => projT3 u - end. + (rew dependent [Q] H in projT2 u) + (rew dependent [R] H in projT3 u). Proof. destruct H, u; reflexivity. Defined. @@ -611,12 +609,8 @@ Section sig2. (Q y) (R y) (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 - match H in (_ = y) return R y (rew H in proj1_sig u) with - | eq_refl => proj3_sig u - end. + (rew dependent [Q] H in proj2_sig u) + (rew dependent [R] H in proj3_sig u). Proof. destruct H, u; reflexivity. Defined. |