blob: 9b1ff2c961514314cfbdfb7eb76f3fe4f38822da (
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
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
|
Require Import Crypto.Util.Equality.
Require Import Crypto.Util.GlobalSettings.
Section sigT.
Definition pr1_path {A} {P : A -> Type} {u v : sigT P} (p : u = v)
: projT1 u = projT1 v
:= f_equal (@projT1 _ _) p.
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.
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.
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).
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).
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.
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).
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.
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).
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.
|
