blob: 2d788aa32824cdfb10d4cca9b49dad6d0172a14a (
plain)
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
|
(** * 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 Crypto.Util.Equality.
Require Import Crypto.Util.GlobalSettings.
Local Arguments fst {_ _} _.
Local Arguments snd {_ _} _.
Local Arguments f_equal {_ _} _ {_ _} _.
Scheme Equality for prod.
(** ** 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.
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.
End prod.
(** ** 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 inversion_prod_step :=
match goal with
| [ H : pair _ _ = pair _ _ |- _ ]
=> apply path_prod_uncurried_iff in H; simpl_proj_pair_in H; destruct H
end.
Ltac inversion_prod := repeat inversion_prod_step.
|
