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
|
Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Util.Tactics.
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.
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)
(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 gen_prop.
Definition interp_flat_type_rel_pointwise2
:= @interp_flat_type_rel_pointwise2_gen_Prop Prop and True.
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.
End language.
Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _.
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 {_ _ _} 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 {_} _ _ {_} _ _.
|
