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
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
|
(** * Classification of the Σ Type *)
(** In this file, we classify the basic structure of Σ types ([sigT],
[sig], and [ex], 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 Crypto.Util.Equality.
Require Import Crypto.Util.GlobalSettings.
Local Arguments projT1 {_ _} _.
Local Arguments projT2 {_ _} _.
Local Arguments proj1_sig {_ _} _.
Local Arguments proj1_sig {_ _} _.
Local Arguments f_equal {_ _} _ {_ _} _.
(** ** 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 u, 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, u; reflexivity.
Defined.
End sigT.
(** ** Equality for [sig] *)
Section sig.
Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
: proj1_sig u = proj1_sig v
:= f_equal (@proj1_sig _ _) p.
Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v)
: eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v.
Proof.
destruct p; reflexivity.
Defined.
Definition path_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})
: 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.
Definition path_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)
: u = v
:= path_sig_uncurried u v (exist _ p q).
Definition path_sig_rect {A P} {u v : @sig A P} (Q : u = v -> Type)
(f : forall p q, Q (path_sig u v p q))
: forall p, Q p.
Proof. intro p; specialize (f (proj1_sig_path p) (proj2_sig_path p)); destruct u, p; exact f. Defined.
Definition path_sig_rec {A P u v} (Q : u = v :> @sig A P -> Set) := path_sig_rect Q.
Definition path_sig_ind {A P u v} (Q : u = v :> @sig A P -> Prop) := path_sig_rec Q.
Definition path_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : @sig A P)
(p : proj1_sig u = proj1_sig v)
: u = v
:= path_sig u v p (P_hprop _ _ _).
Definition path_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)).
Proof.
split; [ intro; subst; exists eq_refl; reflexivity | apply path_sig_uncurried ].
Defined.
Definition path_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
(u v : @sig A P)
: u = v <-> (proj1_sig u = proj1_sig v)
:= conj (f_equal proj1_sig) (path_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
= 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
| eq_refl => proj2_sig u
end.
Proof.
destruct H, u; reflexivity.
Defined.
End sig.
(** ** Equality for [ex] *)
Section ex.
Definition path_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)
: ex_intro P u1 u2 = ex_intro P v1 v2.
Proof.
destruct pq as [p q].
destruct q; simpl in *.
destruct p; reflexivity.
Defined.
Definition path_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
(p : u1 = v1) (q : eq_rect _ _ u2 _ p = v2)
: ex_intro P u1 u2 = ex_intro P v1 v2
:= path_ex_uncurried' P (ex_intro _ p q).
Definition path_ex'_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
(u1 v1 : A) (u2 : P u1) (v2 : P v1)
(p : u1 = v1)
: ex_intro P u1 u2 = ex_intro P v1 v2
:= path_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
= 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
| eq_refl => u2
end
end.
Proof.
destruct H, u; reflexivity.
Defined.
End ex.
(** ** 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[proj1_sig (exist _ ?x ?p)]
=> let G' := context G[x] in change G' in H
| context G[proj2_sig (exist _ ?x ?p)]
=> let G' := context G[p] in change G' in H
| 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_using H rect :=
let H0 := fresh H in
let H1 := fresh H in
induction H as [H0 H1] using (rect _ _ _ _);
simpl_proj_exist_in H0;
simpl_proj_exist_in H1.
Ltac inversion_sigma_step :=
match goal with
| [ H : _ = exist _ _ _ |- _ ]
=> induction_sigma_in_using H @path_sig_rect
| [ H : _ = existT _ _ _ |- _ ]
=> induction_sigma_in_using H @path_sigT_rect
| [ H : exist _ _ _ = _ |- _ ]
=> induction_sigma_in_using H @path_sig_rect
| [ H : existT _ _ _ = _ |- _ ]
=> induction_sigma_in_using H @path_sigT_rect
end.
Ltac inversion_sigma := repeat inversion_sigma_step.
|
