-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHyperCriterion.v
178 lines (141 loc) · 5.9 KB
/
HyperCriterion.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
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Printing Implicit Defensive.
Require Import ClassicalExtras.
Require Import MyNotation.
Require Import Setoid.
Require Import FunctionalExtensionality.
Require Import Galois.
Require Import LanguageModel.
Require Import TraceModel.
Require Import Properties.
Require Import ChainModel.
Require Import Def.
Require Import HyperDef.
Require Import TraceCriterion.
Require Import PropExtensionality.
Definition prop_extensionality := propositional_extensionality.
Section HyperCriterion.
Variable Source Target: Language.
Variable compilation_chain : CompilationChain Source Target.
(*CA: we don't need a particular structure of traces to define preservation
e.g. traces = values or our defn of traces both make sense
*)
Variable trace__S trace__T : Set.
Local Definition prop__S := prop trace__S.
Local Definition prop__T := prop trace__T.
Local Definition hprop__S := hprop trace__S.
Local Definition hprop__T := hprop trace__T.
Variable Source_Semantics : Semantics Source trace__S.
Variable Target_Semantics : Semantics Target trace__T.
Local Definition sem__S := sem Source_Semantics.
Local Definition sem__T := sem Target_Semantics.
Local Definition beh__S := beh Source_Semantics.
Local Definition beh__T := beh Target_Semantics.
Local Definition prg__S := prg Source.
Local Definition prg__T := prg Target.
Local Definition sat__S := sat Source_Semantics.
Local Definition sat__T := sat Target_Semantics.
Local Definition hsat__S := hsat Source_Semantics.
Local Definition hsat__T := hsat Target_Semantics.
Local Definition cmp := compile_whole Source Target compilation_chain.
Local Notation "W ↓" := (cmp W) (at level 50).
Variable rel : trace__S -> trace__T -> Prop.
Local Definition adjunction := induced_connection rel.
Local Definition τ' : prop__S -> prop__T := α adjunction.
Local Definition σ' : prop__T -> prop__S := γ adjunction.
Local Definition rel_adjunction_law : Adjunction_law τ' σ' := adjunction_law adjunction.
Local Definition τP := τTP compilation_chain
Source_Semantics Target_Semantics
τ'.
Local Definition σP := σTP compilation_chain
Source_Semantics Target_Semantics
σ'.
Local Definition τHP := τHP compilation_chain
Source_Semantics Target_Semantics
τ'.
Local Definition σHP := σHP compilation_chain
Source_Semantics Target_Semantics
σ'.
Definition rel_HC := forall W t__T, beh__T (W ↓) t__T <-> (exists t__S, rel t__S t__T /\ beh__S W t__S).
Lemma rel_HC' : rel_HC <-> forall W, beh__T (W ↓) = τ' (beh__S W).
split => Hrel W.
apply functional_extensionality => t__T. apply: prop_extensionality.
rewrite (Hrel W). by firstorder.
rewrite (Hrel W). by firstorder.
Qed.
Theorem rel_HC_τHP : rel_HC <-> τHP.
Proof.
rewrite rel_HC'. split.
- move => H_rel W h__S. now exists (beh__S W).
- move => H_τHP W. specialize (H_τHP W (fun π__S => π__S = beh__S W)).
have Hfoo : hsat__S W (fun π__S => π__S = beh__S W) by auto.
destruct (H_τHP Hfoo) as [bs [Heq H]]. subst. exact H.
Qed.
(*CA: if τ ⇆ σ is an insertion then
tilde_HC => σHP
but not able to prove the vicerversa holds
(quite convinced it is not true)
*)
Lemma rel_HC_σHP : (Insertion_snd τ' σ') ->
rel_HC -> σHP.
Proof.
rewrite rel_HC' => HIns Hrel W H__T [b__T [bt_HT Heq]].
move: (Hrel W). rewrite /beh__T /beh__S Heq HIns.
move => Heq__T. now subst.
Qed.
Lemma σHP_rel_HC : (Reflection_fst τ' σ') ->
σHP -> rel_HC.
Proof.
rewrite rel_HC' => Hrefl Hσpres W.
move: (Hσpres W (fun π__T => π__T = τ' (beh__S W))).
rewrite /σhP => σ_pres_behW. apply: σ_pres_behW.
have: (HyperDef.σ__h σ' (eq^~ (τ' (beh__S W)))) = (fun π__S => π__S = (beh__S W)).
{ rewrite /HyperDef.σ__h /lift.
apply: functional_extensionality => x.
apply: prop_extensionality.
split.
move => [b2 [H1 H2]]. subst. apply: Hrefl.
move => Heq. rewrite Heq. exists (τ' (beh__S W)).
split; [reflexivity | by rewrite Hrefl]. }
move => Heq. by rewrite Heq.
Qed.
(****************************************************************)
(* rel_TC /\ rel_TC_fwd -> rel_HC ? *)
Local Definition rel_TC := rel_TC compilation_chain
Source_Semantics Target_Semantics
rel.
Local Definition rel_FC1 := rel_FC1 compilation_chain
Source_Semantics Target_Semantics
rel.
Local Definition rel_FC2 := rel_FC2 compilation_chain
Source_Semantics Target_Semantics
rel.
(* under the assumption rel is a total function from source to target traces
HC comes as consequence of TC and FC
*)
Theorem rel_total_map_TC_plus_FC1_HC :
(forall s, exists! t, rel s t) ->
rel_TC -> rel_FC1 -> rel_HC.
Proof.
setoid_rewrite rel_TC'. setoid_rewrite rel_FC1'.
rewrite rel_HC' => rel_map bcc fcc W.
apply: mutual_inclusion.
+ by apply: bcc.
+ rewrite rel_adjunction_law => s behWs t rel_s_t.
move: (fcc W s behWs). move => [t' [rel_s_t' beh_cmpW_t']].
have Heq: t = t'.
{ move: (rel_map s). move => [t0 [rel_s_t0 eq_t0]].
by rewrite -(eq_t0 t rel_s_t) -(eq_t0 t' rel_s_t'). }
by rewrite Heq.
Qed.
Theorem TC_plus_FC2_HC :
rel_TC -> rel_FC2 -> rel_HC.
Proof.
setoid_rewrite rel_TC'. setoid_rewrite rel_FC2'.
rewrite rel_HC' => bcc fcc W.
apply: mutual_inclusion.
+ exact (bcc W).
+ rewrite rel_adjunction_law. exact (fcc W).
Qed.
End HyperCriterion.