-
Notifications
You must be signed in to change notification settings - Fork 9
/
index_uip.v
159 lines (135 loc) · 4.84 KB
/
index_uip.v
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
Add LoadPath "coq/examples".
Require Import Example.
Require Import Vector.
Require Import List.
Require Import Ornamental.Ornaments.
From Coq Require Import Arith.
(* syntax to match paper *)
Notation vector := Vector.t.
Notation consV n t v := (Vector.cons _ t n v).
Notation nilV := Vector.nil.
Set DEVOID search prove coherence.
Set DEVOID search prove equivalence.
Set DEVOID lift type.
(* Usually, we use this: *)
Definition vanilla_uip
: forall (x y : nat) (p1 p2 : x = y), p1 = p2
:= Eqdep_dec.UIP_dec Nat.eq_dec.
(*
* Okay, now let's try to state and prove a lemma that doens't
* depend on UIP on the type nat, but rather depends
* on the list and vector types. First:
*)
Find ornament list vector as ltv.
(*
* Next, define the adjoints:
*)
Definition section_adjoint T := Adjoint.fg_id' (ltv_inv T) (ltv T) (ltv_retraction T) (ltv_section T).
Definition retraction_adjoint T := Adjoint.fg_id' (ltv T) (ltv_inv T) (ltv_section T) (ltv_retraction T).
Lemma is_adjoint_section T (pv : sigT (vector T)) : ltv_section T (ltv_inv T pv) = f_equal (ltv_inv T) (retraction_adjoint T pv).
Proof.
apply Adjoint.g_adjoint.
Defined.
Lemma is_adjoint_retraction T (l : list T) : ltv_retraction T (ltv T l) = f_equal (ltv T) (section_adjoint T l).
Proof.
apply Adjoint.g_adjoint.
Defined.
(*
Lemma mocha_uip :
forall (T : Type) (n : nat) (l : list T) (p1 p2 : projT1 (ltv T l) = ltv_index T l),
p1 = p2.
Proof.
intros T n l. destruct (ltv_coh T l). remember (ltv T l) as s.
unfold ltv. simpl.
remember (ltv T l) as s. induction s.
Check ltv_coh.
apply (Eqdep_dec.UIP_dec Nat.eq_dec).*)
(* Try the Jason thing first: *)
Definition ltv_u (A : Type) (n : nat) (ll : { l : list A & ltv_index A l = n}) : vector A n :=
eq_rect
(ltv_index _ (projT1 ll))
(vector A)
(eq_rect
(projT1 (ltv _ (projT1 ll)))
(vector A)
(projT2 (ltv _ (projT1 ll)))
(ltv_index _ (projT1 ll))
(ltv_coh _ (projT1 ll)))
n
(projT2 ll). (* ltv_index A l = n *)
Definition ltv_inv_u (A : Type) (n : nat) (v : vector A n) : { l : list A & ltv_index A l = n} :=
existT
(fun (l : list A) => ltv_index _ l = n)
(ltv_inv _ (existT _ n v))
(eq_rect
(projT1 (ltv A (ltv_inv A (existT _ n v))))
(fun n0 : nat => n0 = n)
(eq_rect
(existT _ n v)
(fun s : sigT (vector A) => projT1 s = n)
(eq_refl (projT1 (existT _ n v)))
(ltv A (ltv_inv A (existT _ n v)))
(eq_sym (ltv_retraction _ (existT _ n v))))
(ltv_index _ (ltv_inv _ (existT _ n v)))
(ltv_coh _ (ltv_inv _ (existT _ n v)))).
Lemma section_u : forall A n v, ltv_inv_u A n (ltv_u A n v) = v.
Proof.
intros A n [l H]; apply eq_sigT_uncurried; subst n.
cbv [ltv_u ltv_inv_u ltv_coh].
cbn [projT1 projT2 eq_rect].
change (existT _ (ltv_index A l) (projT2 (ltv A l))) with (ltv A l).
exists (section_adjoint _ _).
rewrite (is_adjoint_retraction A l).
destruct (section_adjoint A l).
reflexivity.
Qed.
Lemma retraction_u : forall A n v, ltv_u A n (ltv_inv_u A n v) = v.
Proof.
cbv [ltv_u ltv_inv_u].
cbn [projT1 projT2].
intros.
set (p := ltv_retraction A (existT _ n v)).
set (q := ltv_coh _ _).
clearbody p q.
cbv beta in *.
generalize dependent (ltv A (ltv_inv A (existT _ n v))).
intros [x y] p q.
cbn [projT1 projT2] in *.
subst x.
inversion_sigma.
repeat match goal with H : _ = ?v |- _ => is_var v; destruct H end.
reflexivity.
Qed.
(* So, what variant of UIP do we get this way? It should be in the proof of section somewhere. *)
(* TODO WIP, see issue 39 *)
Definition zip := packed_list.zip.
Definition zip_with := packed_list.zip_with.
Lemma uip_instance:
forall (A B : Type) (n : nat)
(l : list A) (H : hs_to_coqV_p.list_to_t_index A l = n)
(pl2 : {l2 : list B & length l2 = n}),
eq_rect
(hs_to_coq.zip_with A B (A * B) pair l (projT1 pl2))
(fun l3 : list (A * B) => length l3 = n)
(packed_list.zip_with_length A B (A * B) pair n l (projT1 pl2) (id H) (projT2 pl2))
(hs_to_coq.zip A B l (projT1 pl2))
(hs_to_coq.zip_with_is_zip A B l (projT1 pl2)) =
packed_list.zip_length A B n l (projT1 pl2) (id H) (projT2 pl2).
Proof.
intros.
apply (Eqdep_dec.UIP_dec Nat.eq_dec). (* <- what we want to replace *)
Defined.
Lemma zip_with_is_zip :
forall A B n (pl1 : { l1 : list A & length l1 = n }) (pl2 : { l2 : list B & length l2 = n }),
zip_with A B (A * B) pair n pl1 pl2 = zip A B n pl1 pl2.
Proof.
intros A B n pl1.
apply packed_list_rect with (P := fun (pl1 : {l1 : list A & length l1 = n}) => forall pl2 : {l2 : list B & length l2 = n}, zip_with A B (A * B) pair n pl1 pl2 = zip A B n pl1 pl2).
intros l H pl2.
unfold zip_with, zip, packed_list_rect, hs_to_coqV_p.list_to_t_rect, packed_rect. simpl.
apply eq_existT_uncurried.
(* list proof: *)
exists (hs_to_coq.zip_with_is_zip A B l (projT1 pl2)).
(* length invariant: *)
apply uip_instance.
Defined.