1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
(** * Definition and classification of the [Σ] Type, with primitive projections *)
(** In this file, we classify the basic structure of Σ types ([sigT]
in Coq). In particular, we classify equalities of dependent pairs
(inhabitants of Σ types), so that when we have an equality between
two such pairs, or when we want such an equality, we have a
systematic way of reducing such equalities to equalities at
simpler types. *)
Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.IffT.
Require Import Crypto.Util.Equality.
Require Import Crypto.Util.GlobalSettings.
Local Set Primitive Projections.
Delimit Scope primproj_type_scope with primproj_type.
Delimit Scope primproj_scope with primproj.
Import EqNotations.
Module Import Primitive.
Record sigT {A} P := existT { projT1 : A ; projT2 : P projT1 }.
Global Arguments existT {_} _ _ _.
Global Arguments projT1 {_ _} _.
Global Arguments projT2 {_ _} _.
Module Import Notations.
Notation "{ x & P }" := (sigT (fun x => P)) : type_scope.
Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope.
Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
Add Printing Let sigT.
End Notations.
Add Printing Let sigT.
Local Set Implicit Arguments.
Definition sigT_beq A P (eq_A : A -> A -> bool) (eq_P : forall a a', P a -> P a' -> bool) (X Y : @sigT A P) : bool
:= let (a, b) := X in let (a', b') := Y in (eq_A a a' && eq_P _ _ b b')%bool.
Global Arguments sigT_beq / .
Lemma sigT_dec_bl A P eq_A eq_P
(A_bl : forall x y : A, eq_A x y = true -> x = y)
(P_bl : forall a a' x y (pf : eq_A a a' = true), eq_P a a' x y = true -> rew [P] (A_bl _ _ pf) in x = y)
(x y : @sigT A P)
: sigT_beq eq_A eq_P x y = true -> x = y.
Proof.
destruct x as [a b], y as [a' b'].
specialize (P_bl a a' b b'); cbn.
generalize dependent (A_bl a a'); clear A_bl; intros A_bl P_bl H.
edestruct eq_A; cbn in *;
destruct (eq_A a a');
first [ specialize (P_bl eq_refl); generalize dependent (A_bl eq_refl)
| specialize (P_bl H); generalize dependent (A_bl H) ];
clear A_bl; intros A_bl P_bl; try specialize (P_bl H); subst;
cbn [eq_rect] in *;
try reflexivity.
all: edestruct eq_P; first [ specialize (P_bl eq_refl) | specialize (P_bl H) ]; subst;
reflexivity.
Defined.
Lemma sigT_dec_bl_nd A P eq_A eq_P
(A_bl : forall x y : A, eq_A x y = true -> x = y)
(P_bl : forall a a' x y (pf : a = a'), rew [P] pf in x = y)
(x y : @sigT A P)
: sigT_beq eq_A eq_P x y = true -> x = y.
Proof.
apply (@sigT_dec_bl A P eq_A eq_P A_bl); intros; apply P_bl.
Defined.
Lemma sigT_dec_lb A P eq_A (eq_P : forall a a', P a -> P a' -> bool)
(A_lb : forall x y : A, x = y -> eq_A x y = true)
(P_lb : forall a (x y : P a), x = y -> eq_P a a x y = true)
(x y : @sigT A P)
: x = y -> sigT_beq eq_A eq_P x y = true.
Proof.
intro; subst y; specialize (A_lb _ _ (eq_refl (projT1 x))); specialize (P_lb _ _ _ (eq_refl (projT2 x))); cbn in *.
edestruct eq_A, eq_P; (reflexivity + assumption).
Defined.
Definition sigT_eq_dec A P eq_A eq_P
(A_bl : forall x y : A, eq_A x y = true -> x = y)
(P_bl : forall a a' x y (pf : eq_A a a' = true), eq_P a a' x y = true -> rew [P] (A_bl _ _ pf) in x = y)
(A_lb : forall x y : A, x = y -> eq_A x y = true)
(P_lb : forall a (x y : P a), x = y -> eq_P a a x y = true)
(x y : @sigT A P)
: {x = y} + {x <> y}.
Proof.
refine (let H := let b := @sigT_beq A P eq_A eq_P x y in if b as b0 return ({b0 = true} + {b0 = false}) then left eq_refl else right eq_refl in
match H with
| left e => left (@sigT_dec_bl A P eq_A eq_P A_bl P_bl x y e)
| right H' => right (fun e => _ (@sigT_dec_lb A P eq_A eq_P A_lb P_lb x y e))
end).
congruence.
Defined.
End Primitive.
Notation "{ x & P }" := (sigT (fun x => P%primproj_type)) : primproj_type_scope.
Notation "{ x : A & P }" := (sigT (A:=A%primproj_type) (fun x => P%primproj_type)) : primproj_type_scope.
Notation "{ ' pat : A & P }" := (sigT (A:=A%primproj_type) (fun pat => P%primproj_type)) : primproj_type_scope.
Add Printing Let sigT.
Import Primitive.Notations.
Local Arguments f_equal {_ _} _ {_ _} _.
Definition projT1_existT {A B} (a:A) (b:B a) : projT1 (existT B a b) = a := eq_refl.
Definition projT2_existT {A B} (a:A) (b:B a) : projT2 (existT B a b) = b := eq_refl.
Create HintDb cancel_primsig discriminated. Hint Rewrite @projT1_existT @projT2_existT : cancel_primsig.
(** ** Equality for [sigT] *)
Section sigT.
(** *** Projecting an equality of a pair to equality of the first components *)
Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
: projT1 u = projT1 v
:= f_equal (@projT1 _ _) p.
(** *** Projecting an equality of a pair to equality of the second components *)
Definition pr2_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
: eq_rect _ _ (projT2 u) _ (pr1_path p) = projT2 v.
Proof.
destruct p; reflexivity.
Defined.
(** *** Equality of [sigT] is itself a [sigT] *)
Definition path_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))
: u = v.
Proof.
destruct u as [u1 u2], v as [v1 v2]; simpl in *.
destruct pq as [p q].
destruct q; simpl in *.
destruct p; reflexivity.
Defined.
(** *** Curried version of proving equality of sigma types *)
Definition path_sigT {A : Type} {P : A -> Type} (u v : sigT P)
(p : projT1 u = projT1 v) (q : eq_rect _ _ (projT2 u) _ p = projT2 v)
: u = v
:= path_sigT_uncurried u v (existT _ p q).
(** *** Equality of [sigT] when the property is an hProp *)
Definition path_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : @sigT A P)
(p : projT1 u = projT1 v)
: u = v
:= path_sigT u v p (P_hprop _ _ _).
(** *** Equivalence of equality of [sigT] with a [sigT] of equality *)
(** We could actually use [IsIso] here, but for simplicity, we
don't. If we wanted to deal with proofs of equality of Σ types
in dependent positions, we'd need it. *)
Definition path_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)).
Proof.
split; [ intro; subst; exists eq_refl; reflexivity | apply path_sigT_uncurried ].
Defined.
(** *** Induction principle for [@eq (sigT _)] *)
Definition path_sigT_rect {A P} {u v : @sigT A P} (Q : u = v -> Type)
(f : forall p q, Q (path_sigT u v p q))
: forall p, Q p.
Proof. intro p; specialize (f (pr1_path p) (pr2_path p)); destruct p; exact f. Defined.
Definition path_sigT_rec {A P u v} (Q : u = v :> @sigT A P -> Set) := path_sigT_rect Q.
Definition path_sigT_ind {A P u v} (Q : u = v :> @sigT A P -> Prop) := path_sigT_rec Q.
(** *** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
Definition path_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : @sigT A P)
: u = v <-> (projT1 u = projT1 v)
:= conj (f_equal projT1) (path_sigT_hprop P_hprop u v).
(** *** Non-dependent classification of equality of [sigT] *)
Definition path_sigT_nondep {A B : Type} (u v : @sigT A (fun _ => B))
(p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
: u = v
:= @path_sigT _ _ u v p (eq_trans (transport_const _ _) q).
(** *** 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
= 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
| eq_refl => projT2 u
end.
Proof.
destruct H; reflexivity.
Defined.
(** *** η Principle for [sigT] *)
Definition sigT_eta {A P} (p : { a : A & P a })
: p = existT _ (projT1 p) (projT2 p)
:= eq_refl.
End sigT.
(** ** Useful Tactics *)
(** *** [inversion_sigma] *)
(** The built-in [inversion] will frequently leave equalities of
dependent pairs. When the first type in the pair is an hProp or
otherwise simplifies, [inversion_sigma] is useful; it will replace
the equality of pairs with a pair of equalities, one involving a
term casted along the other. This might also prove useful for
writing a version of [inversion] / [dependent destruction] which
does not lose information, i.e., does not turn a goal which is
provable into one which requires axiom K / UIP. *)
Ltac simpl_proj_exist_in H :=
repeat match type of H with
| context G[projT1 (existT _ ?x ?p)]
=> let G' := context G[x] in change G' in H
| context G[projT2 (existT _ ?x ?p)]
=> let G' := context G[p] in change G' in H
end.
Ltac induction_sigma_in_as_using H H0 H1 rect :=
induction H as [H0 H1] using (rect _ _ _ _);
simpl_proj_exist_in H0;
simpl_proj_exist_in H1.
Ltac induction_sigma_in_using H rect :=
let H0 := fresh H in
let H1 := fresh H in
induction_sigma_in_as_using H H0 H1 rect.
Ltac inversion_sigma_step :=
match goal with
| [ H : _ = existT _ _ _ |- _ ]
=> induction_sigma_in_using H @path_sigT_rect
| [ H : existT _ _ _ = _ |- _ ]
=> induction_sigma_in_using H @path_sigT_rect
end.
Ltac inversion_sigma := repeat inversion_sigma_step.
|
