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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
Require Import Coq.Lists.List Coq.Classes.RelationClasses Coq.Classes.Morphisms.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Wf.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.Sigma.
Local Open Scope ctype_scope.
Section language.
Context {base_type_code : Type}.
Let Tbase := (@Tbase base_type_code).
Local Coercion Tbase : base_type_code >-> flat_type.
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
Section type.
Context (interp_flat_type : flat_type -> Type)
(R : forall t, interp_flat_type t -> interp_flat_type t -> Prop).
Local Notation interp_type_gen := (interp_type_gen interp_flat_type).
Fixpoint interp_type_gen_rel_pointwise (t : type)
: interp_type_gen t -> interp_type_gen t -> Prop :=
match t with
| Tflat t => R t
| Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x)
end.
Global Instance interp_type_gen_rel_pointwise_Reflexive {H : forall t, Reflexive (R t)}
: forall t, Reflexive (interp_type_gen_rel_pointwise t).
Proof. induction t; repeat intro; reflexivity. Qed.
Global Instance interp_type_gen_rel_pointwise_Symmetric {H : forall t, Symmetric (R t)}
: forall t, Symmetric (interp_type_gen_rel_pointwise t).
Proof. induction t; simpl; repeat intro; symmetry; eauto. Qed.
Global Instance interp_type_gen_rel_pointwise_Transitive {H : forall t, Transitive (R t)}
: forall t, Transitive (interp_type_gen_rel_pointwise t).
Proof. induction t; simpl; repeat intro; etransitivity; eauto. Qed.
End type.
Section flat_type.
Context {interp_base_type : base_type_code -> Type}
(R : forall t, interp_base_type t -> interp_base_type t -> Prop).
Local Notation interp_flat_type := (interp_flat_type interp_base_type).
Fixpoint interp_flat_type_rel_pointwise (t : flat_type)
: interp_flat_type t -> interp_flat_type t -> Prop :=
match t with
| Syntax.Tbase t => R t
| Unit => fun _ _ => True
| Prod _ _ => fun x y => interp_flat_type_rel_pointwise _ (fst x) (fst y)
/\ interp_flat_type_rel_pointwise _ (snd x) (snd y)
end.
Definition interp_type_rel_pointwise
:= interp_type_gen_rel_pointwise _ interp_flat_type_rel_pointwise.
End flat_type.
Section rel_pointwise2.
Section type.
Section hetero_hetero.
Context (interp_src1 interp_src2 : base_type_code -> Type)
(interp_dst1 interp_dst2 : flat_type -> Type)
(Rsrc : forall t1 t2, interp_src1 t1 -> interp_src2 t2 -> Prop)
(Rdst : forall t1 t2, interp_dst1 t1 -> interp_dst2 t2 -> Prop).
Fixpoint interp_type_gen_rel_pointwise2_hetero_hetero (t1 t2 : type)
: interp_type_gen_hetero interp_src1 interp_dst1 t1
-> interp_type_gen_hetero interp_src2 interp_dst2 t2
-> Prop
:= match t1, t2 with
| Tflat t1, Tflat t2 => Rdst t1 t2
| Arrow src1 dst1, Arrow src2 dst2
=> @respectful_hetero _ _ _ _ (Rsrc src1 src2) (fun _ _ => interp_type_gen_rel_pointwise2_hetero_hetero dst1 dst2)
| Tflat _, _
| Arrow _ _, _
=> fun _ _ => False
end.
End hetero_hetero.
Section hetero.
Context (interp_src1 interp_src2 : base_type_code -> Type)
(interp_dst1 interp_dst2 : flat_type -> Type)
(Rsrc : forall t, interp_src1 t -> interp_src2 t -> Prop)
(Rdst : forall t, interp_dst1 t -> interp_dst2 t -> Prop).
Fixpoint interp_type_gen_rel_pointwise2_hetero (t : type)
: interp_type_gen_hetero interp_src1 interp_dst1 t
-> interp_type_gen_hetero interp_src2 interp_dst2 t
-> Prop
:= match t with
| Tflat t => Rdst t
| Arrow src dst => @respectful_hetero _ _ _ _ (Rsrc src) (fun _ _ => interp_type_gen_rel_pointwise2_hetero dst)
end.
End hetero.
Section homogenous.
Context (interp_flat_type1 interp_flat_type2 : flat_type -> Type)
(R : forall t, interp_flat_type1 t -> interp_flat_type2 t -> Prop).
Definition interp_type_gen_rel_pointwise2
: forall t,
interp_type_gen interp_flat_type1 t
-> interp_type_gen interp_flat_type2 t
-> Prop
:= interp_type_gen_rel_pointwise2_hetero interp_flat_type1 interp_flat_type2
interp_flat_type1 interp_flat_type2
R R.
End homogenous.
End type.
Section flat_type.
Context (interp_base_type1 interp_base_type2 : base_type_code -> Type).
Section gen_prop.
Context (P : Type)
(and : P -> P -> P)
(True : P)
(False : P).
Section hetero.
Context (R : forall t1 t2, interp_base_type1 t1 -> interp_base_type2 t2 -> P).
Fixpoint interp_flat_type_rel_pointwise2_hetero_gen_Prop (t1 t2 : flat_type)
: interp_flat_type interp_base_type1 t1 -> interp_flat_type interp_base_type2 t2 -> P
:= match t1, t2 with
| Syntax.Tbase t1, Syntax.Tbase t2 => R t1 t2
| Unit, Unit => fun _ _ => True
| Prod x1 y1, Prod x2 y2
=> fun a b => and (interp_flat_type_rel_pointwise2_hetero_gen_Prop x1 x2 (fst a) (fst b))
(interp_flat_type_rel_pointwise2_hetero_gen_Prop y1 y2 (snd a) (snd b))
| Syntax.Tbase _, _
| Unit, _
| Prod _ _, _
=> fun _ _ => False
end.
End hetero.
Section homogenous.
Context (R : forall t, interp_base_type1 t -> interp_base_type2 t -> P).
Fixpoint interp_flat_type_rel_pointwise2_gen_Prop (t : flat_type)
: interp_flat_type interp_base_type1 t -> interp_flat_type interp_base_type2 t -> P
:= match t with
| Syntax.Tbase t => R t
| Unit => fun _ _ => True
| Prod x y => fun a b => and (interp_flat_type_rel_pointwise2_gen_Prop x (fst a) (fst b))
(interp_flat_type_rel_pointwise2_gen_Prop y (snd a) (snd b))
end.
End homogenous.
End gen_prop.
Definition interp_flat_type_rel_pointwise2_hetero
:= @interp_flat_type_rel_pointwise2_hetero_gen_Prop Prop and True False.
Definition interp_flat_type_rel_pointwise2
:= @interp_flat_type_rel_pointwise2_gen_Prop Prop and True.
Definition interp_type_rel_pointwise2_hetero R
: forall t1 t2, interp_type interp_base_type1 t1
-> interp_type interp_base_type2 t2
-> Prop
:= interp_type_gen_rel_pointwise2_hetero_hetero _ _ _ _ (interp_flat_type_rel_pointwise2_hetero R) (interp_flat_type_rel_pointwise2_hetero R).
Definition interp_type_rel_pointwise2 R
: forall t, interp_type interp_base_type1 t
-> interp_type interp_base_type2 t
-> Prop
:= interp_type_gen_rel_pointwise2 _ _ (interp_flat_type_rel_pointwise2 R).
End flat_type.
End rel_pointwise2.
Section lifting.
Section flat_type.
Context {interp_base_type : base_type_code -> Type}.
Local Notation interp_flat_type := (interp_flat_type interp_base_type).
Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop)
(RUnit : R Unit tt tt).
Section RProd.
Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) -> R (Prod A B) x y)
(RProd' : forall A B x y, R (Prod A B) x y -> R A (fst x) (fst y) /\ R B (snd x) (snd y)).
Lemma lift_interp_flat_type_rel_pointwise1 t (x y : interp_flat_type t)
: interp_flat_type_rel_pointwise R t x y -> R t x y.
Proof. clear RProd'; induction t; simpl; destruct_head_hnf' unit; intuition. Qed.
Lemma lift_interp_flat_type_rel_pointwise2 t (x y : interp_flat_type t)
: R t x y -> interp_flat_type_rel_pointwise R t x y.
Proof. clear RProd; induction t; simpl; destruct_head_hnf' unit; split_and; intuition. Qed.
End RProd.
Section RProd_iff.
Context (RProd : forall A B x y, R A (fst x) (fst y) /\ R B (snd x) (snd y) <-> R (Prod A B) x y).
Lemma lift_interp_flat_type_rel_pointwise t (x y : interp_flat_type t)
: interp_flat_type_rel_pointwise R t x y <-> R t x y.
Proof.
split_iff; split; auto using lift_interp_flat_type_rel_pointwise1, lift_interp_flat_type_rel_pointwise2.
Qed.
End RProd_iff.
End flat_type.
End lifting.
Lemma interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2
{interp_base_type1 interp_base_type2 t1 t2 T1 T2} R' e1 e2 v1 v2
(H : List.In (existT _ (t1, t2)%core (v1, v2)%core) (flatten_binding_list2 e1 e2))
(HR : interp_flat_type_rel_pointwise2_hetero interp_base_type1 interp_base_type2 R' T1 T2 e1 e2)
: R' t1 t2 v1 v2.
Proof.
revert dependent T2; induction T1, T2;
repeat match goal with
| _ => intro
| [ H : False |- _ ] => exfalso; assumption
| _ => progress subst
| _ => assumption
| _ => progress inversion_sigma
| _ => progress inversion_prod
| _ => progress simpl in *
| _ => progress destruct_head_hnf' and
| [ H : context[List.In _ (_ ++ _)] |- _ ]
=> rewrite List.in_app_iff in H
| _ => progress destruct_head' or
| _ => solve [ eauto ]
end.
Qed.
End language.
Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _.
Global Arguments interp_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _.
Global Arguments interp_type_gen_rel_pointwise2_hetero_hetero {_ _ _ _ _} Rsrc Rdst {t1 t2} _ _.
Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc Rdst {t} _ _.
Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _.
Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and True R {t} _ _.
Global Arguments interp_flat_type_rel_pointwise2_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _.
Global Arguments interp_flat_type_rel_pointwise2_hetero {_ _ _} R {t1 t2} _ _.
Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _.
Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _.
Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _.
Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
|
