-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathTrecord.v
197 lines (159 loc) · 6.41 KB
/
Trecord.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
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
Require Import SquiggleEq.list.
Require Import SquiggleEq.UsefulTypes.
Require Import common.
Require Import SquiggleEq.tactics.
Arguments memberb {_} {_} x l.
Set Implicit Arguments.
(* transparent lemma for computations. Move to SquiggleEq *)
Lemma subsetb_memberb {T:Type} {dt :Deq T} (l1 l2 : list T):
(subsetb _ l1 l2 = true)
-> forall t, (memberb t l1) = true -> (memberb t l2) = true.
Proof using.
intros Hs ? Hm.
remember (memberb t l2) as m2. symmetry in Heqm2.
destruct m2;[reflexivity|].
apply False_rect.
setoid_rewrite assert_subsetb in Hs.
setoid_rewrite assert_memberb in Hm.
apply Bool.not_true_iff_false in Heqm2.
setoid_rewrite assert_memberb in Heqm2.
eauto.
Defined.
(*Prop is also considered a type here.*)
Inductive Props : Set := Total | OneToOne (*| Irrel *).
Definition allProps : list Props := [Total; OneToOne (*; Irrel *) ].
Global Instance deq : Deq Props.
Proof using.
apply @deqAsSumbool.
unfold DeqSumbool. intros. unfold DecidableSumbool.
repeat decide equality.
Defined.
Notation univ := (Set) (only parsing).
Definition IndicesInvUniv := Type.
(* use IndUnivs here? *)
(*Polymorphic *) Record GoodRel (select: list Props)
(T₁ T₂: univ) : IndicesInvUniv (* nececcarily bigger than Set if univ, because of R*) :=
{
R : T₁ -> T₂ -> Prop (* Type ? *);
Rtot : if (memberb Total select) then TotalHeteroRel R else True;
Rone : if (memberb OneToOne select) then oneToOne R else True;
(* Proof irrelevance is not needed anymore, after changing Type to Prop in R.
This item is always deselected. Can be removed once we totatlly commit to Prop
and decide that assuming Proof irrelevance is acceptable.
About the latter, UIP was badly needed for the oneToOne of indexed inductives.
If UIP <-> Proof Irrelevance, then we will be forced to have Proof irrelevance
be acceptable
Rirrel : if (memberb Irrel select) then relIrrUptoEq R else True;
*)
}.
Check (GoodRel allProps (True:Prop) (True:Prop)):Type.
Fail Check (GoodRel allProps (nat:Set) (nat:Set)):Set (* because of R, this has to be atleast 1 bigger than Set*).
Definition eraseRP (sb ss: list Props)
(sub: subsetb _ ss sb=true) (T₁ T₂:univ) (gb: GoodRel sb T₁ T₂ ) :
(GoodRel ss T₁ T₂ ).
Proof.
(* projecting a goodrel should compute to a goodRel. So no matching before
returning a goodRel *)
apply Build_GoodRel with (R:= @R sb _ _ gb);
destruct gb; simpl in *;
apply' subsetb_memberb sub.
- specialize (sub Total).
destruct (memberb _ ss);[| exact I].
specialize (sub eq_refl). rewrite sub in Rtot0.
assumption.
- specialize (sub OneToOne).
destruct (memberb _ ss);[| exact I].
specialize (sub eq_refl). rewrite sub in Rone0.
assumption.
Defined.
Definition onlyTotal : list Props := [Total].
Definition cast_Good_onlyTotal (T₁ T₂:univ) (gb: GoodRel allProps T₁ T₂ ) :
(GoodRel onlyTotal T₁ T₂ ).
apply eraseRP with (sb:=allProps);[reflexivity| assumption].
Defined.
Definition BestRel : Set -> Set -> Type := GoodRel allProps (* [Total; OneToOne] *).
Definition BestR : forall T₁ T₂ : Set, GoodRel allProps T₁ T₂ -> T₁ -> T₂ -> Prop
:= @R allProps.
Lemma IsoRel_implies_iff (A B:Prop) (pb : BestRel A B) : A <-> B.
Proof using.
specialize (@Rtot allProps _ _ pb). simpl.
intros Ht.
apply Prop_RSpec in Ht.
apply fst in Ht.
unfold IffRel in Ht.
apply tiffIff in Ht.
apply Ht.
Qed.
Definition mkBestRel (A1 A2:Set) (AR : A1 -> A2 -> Prop)
(tot12 : TotalHeteroRelHalf AR)
(tot21 : TotalHeteroRelHalf (rInvSP AR))
(one12: oneToOneHalf AR)
(one21: oneToOneHalf (rInvSP AR))
: BestRel A1 A2.
Proof.
exists AR; simpl.
- split.
+ exact tot12.
+ exact tot21.
- split.
+ exact one12.
+ exact one21.
Defined.
Definition mkBestRelPropOld (A1 A2:Prop) (AR : A1 -> A2 -> Prop)
(tot12 : TotalHeteroRelHalf AR)
(tot21 : TotalHeteroRelHalf (rInvSP AR))
: BestRel A1 A2.
Proof.
exists AR; simpl.
- split.
+ exact tot12.
+ exact tot21.
- apply propeOneToOne.
Defined.
(* TODO: remove new *)
Definition mkBestRelProp (A1 A2:Prop) (AR : A1 -> A2 -> Prop)
(tot12 : iffCompleteHalf AR)
(tot21 : iffCompleteHalf (rInvSP AR))
: BestRel A1 A2.
Proof.
exists AR; simpl.
- apply iffHalfTotal; assumption.
- apply propeOneToOne.
Defined.
Definition BestTot12 (T₁ T₂ : Set) (T_R: GoodRel allProps T₁ T₂) (t1:T₁) : T₂
:= projT1 ((fst (Rtot T_R)) t1).
Definition BestTot12R (T₁ T₂ : Set) (T_R: GoodRel allProps T₁ T₂) (t1:T₁)
:= projT2 ((fst (Rtot T_R)) t1).
Definition BestTot21 (T₁ T₂ : Set) (T_R: GoodRel allProps T₁ T₂) (t2:T₂) : T₁
:= projT1 ((snd (Rtot T_R)) t2).
Definition BestTot21R (T₁ T₂ : Set) (T_R: GoodRel allProps T₁ T₂) (t2:T₂)
:= projT2 ((snd (Rtot T_R)) t2).
Definition BestOne12 (A B : Set) (T_R: GoodRel allProps A B) (a :A) (b1 b2 :B)
(r1 : R T_R a b1) (r2 : R T_R a b2) : b2=b1
:= eq_sym ((proj1 (Rone T_R)) a b1 b2 r1 r2).
Definition BestOne21 (A B : Set) (T_R: GoodRel allProps A B) (a1 :A) (b :B) (a2:A)
(r1 : R T_R a1 b) (r2 : R T_R a2 b) : a2 = a1
:= eq_sym ((proj2 (Rone T_R)) b a1 a2 r1 r2).
Definition BestOneijjo (A B : Set) (T_R: GoodRel allProps A B) (a :A) (b1 b2 :B)
(r1 : R T_R a b1) (r2 : R T_R a b2) : b1=b2
:= ((proj1 (Rone T_R)) a b1 b2 r1 r2).
Definition BestOneijjo21 (A B : Set) (T_R: GoodRel allProps A B) (b :B) (a1 a2:A)
(r1 : R T_R a1 b) (r2 : R T_R a2 b) : a1 = a2
:= ((proj2 (Rone T_R)) b a1 a2 r1 r2).
Definition BestRelP : Prop -> Prop -> Prop := iff.
Definition BestRP (T₁ T₂ : Prop) (t₁ : T₁) (t₂ : T₂) : Prop := True.
Require Import ProofIrrelevance.
(*
The relation for Prop cannot be (fun _ _ => True) as it breaks many things:
see the erasure section of onenote
https://onedrive.live.com/edit.aspx/Documents/Postdoc?cid=946e75b47b19a3b5&id=documents&wd=target%28parametricity%2Fpapers%2Flogic%2Ferasure.one%7CE3B57163-01F2-A447-8AD2-A7AA172DB692%2F%29
onenote:https://d.docs.live.net/946e75b47b19a3b5/Documents/Postdoc/parametricity/papers/logic/erasure.one#section-id={E3B57163-01F2-A447-8AD2-A7AA172DB692}&end
*)
Definition GoodPropAsSet {A1 A2:Prop} (bp: BestRelP A1 A2) : BestRel A1 A2.
unfold BestRelP in bp.
exists (fun _ _ => True); simpl.
- apply Prop_RSpec. unfold Prop_R,IffRel,CompleteRel.
apply tiffIff in bp.
split; [assumption|]. intros ? ?. exact I.
- split; intros ? ? ? ? ?; apply proof_irrelevance.
Defined.