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
|
(** * Classification of the [×] Type *)
(** In this file, we classify the basic structure of [×] types ([prod]
in Coq). In particular, we classify equalities of non-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 Arguments fst {_ _} _.
Local Arguments snd {_ _} _.
Local Arguments f_equal {_ _} _ {_ _} _.
Scheme Equality for prod.
Definition fst_pair {A B} (a:A) (b:B) : fst (a,b) = a := eq_refl.
Definition snd_pair {A B} (a:A) (b:B) : snd (a,b) = b := eq_refl.
Create HintDb cancel_pair discriminated. Hint Rewrite @fst_pair @snd_pair : cancel_pair.
(** ** Equality for [prod] *)
Section prod.
(** *** Projecting an equality of a pair to equality of the first components *)
Definition fst_path {A B} {u v : prod A B} (p : u = v)
: fst u = fst v
:= f_equal fst p.
(** *** Projecting an equality of a pair to equality of the second components *)
Definition snd_path {A B} {u v : prod A B} (p : u = v)
: snd u = snd v
:= f_equal snd p.
(** *** Equality of [prod] is itself a [prod] *)
Definition path_prod_uncurried {A B : Type} (u v : prod A B)
(pq : prod (fst u = fst v) (snd u = snd v))
: u = v.
Proof.
destruct u as [u1 u2], v as [v1 v2]; simpl in *.
destruct pq as [p q].
destruct p, q; simpl in *.
reflexivity.
Defined.
(** *** Curried version of proving equality of sigma types *)
Definition path_prod {A B : Type} (u v : prod A B)
(p : fst u = fst v) (q : snd u = snd v)
: u = v
:= path_prod_uncurried u v (pair p q).
(** *** Equivalence of equality of [prod] with a [prod] 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_prod_uncurried_iff {A B}
(u v : @prod A B)
: u = v <-> (prod (fst u = fst v) (snd u = snd v)).
Proof.
split; [ intro; subst; split; reflexivity | apply path_prod_uncurried ].
Defined.
(** *** Eta-expansion of [@eq (prod _ _)] *)
Definition path_prod_eta {A B} {u v : @prod A B} (p : u = v)
: p = path_prod_uncurried u v (fst_path p, snd_path p).
Proof. destruct u, p; reflexivity. Defined.
(** *** Induction principle for [@eq (prod _ _)] *)
Definition path_prod_rect {A B} {u v : @prod A B} (P : u = v -> Type)
(f : forall p q, P (path_prod_uncurried u v (p, q)))
: forall p, P p.
Proof. intro p; specialize (f (fst_path p) (snd_path p)); destruct u, p; exact f. Defined.
Definition path_prod_rec {A B u v} (P : u = v :> @prod A B -> Set) := path_prod_rect P.
Definition path_prod_ind {A B u v} (P : u = v :> @prod A B -> Prop) := path_prod_rec P.
End prod.
Lemma prod_iff_and (A B : Prop) : (A /\ B) <-> (A * B).
Proof. repeat (intros [? ?] || intro || split); assumption. Defined.
Global Instance iff_prod_Proper
: Proper (iff ==> iff ==> iff) (fun A B => prod A B).
Proof. repeat intro; tauto. Defined.
Global Instance iff_iffTp_prod_Proper
: Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
Proof.
intros ?? [?] ?? [?]; constructor; tauto.
Defined.
Global Instance iffTp_iff_prod_Proper
: Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1.
Proof.
intros ?? [?] ?? [?]; constructor; tauto.
Defined.
Global Instance iffTp_iffTp_prod_Proper
: Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
Proof.
intros ?? [?] ?? [?]; constructor; tauto.
Defined.
Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances.
Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances.
Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances.
(** ** Useful Tactics *)
(** *** [inversion_prod] *)
Ltac simpl_proj_pair_in H :=
repeat match type of H with
| context G[fst (pair ?x ?p)]
=> let G' := context G[x] in change G' in H
| context G[snd (pair ?x ?p)]
=> let G' := context G[p] in change G' in H
end.
Ltac induction_path_prod H :=
let H0 := fresh H in
let H1 := fresh H in
induction H as [H0 H1] using path_prod_rect;
simpl_proj_pair_in H0;
simpl_proj_pair_in H1.
Ltac inversion_prod_step :=
match goal with
| [ H : _ = pair _ _ |- _ ]
=> induction_path_prod H
| [ H : pair _ _ = _ |- _ ]
=> induction_path_prod H
end.
Ltac inversion_prod := repeat inversion_prod_step.
(** This turns a goal like [x = let v := p in let '(x, y) := f v in x
+ y)] into a goal like [x = fst (f p) + snd (f p)]. Note that it
inlines [let ... in ...] as well as destructuring lets. *)
Ltac only_eta_expand_and_contract_step :=
match goal with
| [ |- context[let '(x, y) := ?e in _] ]
=> rewrite (surjective_pairing e)
| [ H : context[let '(x, y) := ?e in _] |- _ ]
=> rewrite (surjective_pairing e) in H
| _ => rewrite <- !surjective_pairing
| [ H : context[(fst ?e, snd ?e)] |- _ ]
=> rewrite <- !surjective_pairing in H
end.
Ltac only_eta_expand_and_contract := repeat only_eta_expand_and_contract_step.
Ltac eta_expand :=
repeat first [ progress cbv beta iota zeta
| only_eta_expand_and_contract_step ].
(** *** [subst_prod] *)
(** The tactic [subst_prod] is like [subst], but it works on equations
of the form [_ = (x, y)] and [(x, y) = _] for [x] and [y]
identifiers. *)
Ltac do_subst_prod A B x y :=
is_var x; is_var y;
let H := fresh in
let xy := fresh x in
remember (@pair A B x y) as xy eqn:H;
assert (fst xy = x) by (subst xy; reflexivity);
assert (snd xy = y) by (subst xy; reflexivity);
subst x y;
clear H; try subst xy.
Ltac subst_prod_step :=
match goal with
| [ H : _ = @pair ?A ?B ?x ?y |- _ ] => do_subst_prod A B x y
| [ H : @pair ?A ?B ?x ?y = _ |- _ ] => do_subst_prod A B x y
end.
Ltac subst_prod := repeat subst_prod_step.
|
