-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRobust2relSSCHPreservation.v
143 lines (117 loc) · 5.19 KB
/
Robust2relSSCHPreservation.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
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 PropExtensionality.
Definition prop_extensionality := propositional_extensionality.
Section Robust2relSSCHPreservation.
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 : Type.
Local Definition prop__S := prop trace__S.
Local Definition prop__T := prop 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 par__S := par Source.
Local Definition par__T := par Target.
Local Definition ctx__S := ctx Source.
Local Definition ctx__T := ctx Target.
Local Definition rsat__S := rhsat2 Source_Semantics.
Local Definition rsat__T := rhsat2 Target_Semantics.
Local Definition cmp := compile_par Source Target compilation_chain.
Local Notation "P ↓" := (cmp P) (at level 50).
(* CA: don't understand why this does not work
Local Notation " C [ P ] " := (plug _ P C) (at level 50).
*)
Local Definition plug__S:= plug Source.
Local Definition plug__T := plug Target.
(* still mappings on trace properties *)
Variable σ__π : (trace__T -> Prop) -> (trace__S -> Prop).
Variable τ__π : (trace__S -> Prop) -> (trace__T -> Prop).
Definition prod_σ : (prop__T * prop__T -> Prop) -> (prop__S * prop__S -> Prop) :=
fun T =>
fun Π => exists π__T π__T', fst Π = σ__π π__T /\
snd Π = σ__π π__T' /\
T (π__T, π__T').
Definition prod_τ : (prop__S * prop__S -> Prop) -> (prop__T * prop__T -> Prop) :=
fun S =>
fun Π => exists π__S π__S', fst Π = τ__π π__S /\
snd Π = τ__π π__S' /\
S (π__S, π__S').
Definition sCl_σ : ((trace__T -> Prop) * (trace__T -> Prop) -> Prop) ->
((trace__S -> Prop) * (trace__S -> Prop) -> Prop) :=
sCl2 ∘ prod_σ.
Definition sCl_τ : ((trace__S -> Prop) * (trace__S -> Prop) -> Prop) ->
((trace__T -> Prop) * (trace__T -> Prop) -> Prop) :=
sCl2 ∘ prod_τ.
Definition sCl_σR2rhP (P1 P2 : par__S) (T : prop__T * prop__T -> Prop) :=
rsat__S P1 P2 (sCl_σ T) -> rsat__T (P1 ↓) (P2 ↓) T.
Definition sCl_τR2rhP (P1 P2 : par__S) (S : prop__S * prop__S -> Prop) :=
rsat__S P1 P2 S -> rsat__T (P1 ↓) (P2 ↓) (sCl_τ S).
Lemma contra_τR2rhP (P1 P2 : par__S) (S : prop__S * prop__S -> Prop) :
(sCl_τR2rhP P1 P2 S) <-> ((exists C__T, ~ (sCl_τ S) (beh__T (plug__T (P1 ↓) C__T),
beh__T (plug__T (P2 ↓) C__T ))) ->
(exists C__S, ~ S (beh__S (plug__S P1 C__S), beh__S (plug__S P2 C__S)))).
Proof.
rewrite /sCl_τR2rhP. by rewrite [_ -> _] contra !neg_rhsat2.
Qed.
Lemma Galois_fst_lift (Hadj : Adjunction_law τ__π σ__π) :
forall T, SCH2 T ->
(sCl_τ (sCl_σ (T)) ⊆ T).
Proof.
move => T SCH2T [b__T1 b__T2] [b__t1 [b__t2 [Hτ [H1 H2]]]].
move: Hτ. move => [b__s1 [b__s2 [H11 [H22 Hσ]]]].
destruct Hσ as [b__s1' [b__s2' [Hσ' [H1' H2']]]].
destruct Hσ' as [bt1'[ bt2' [H11' [H22' HT]]]].
simpl in *. subst.
apply: SCH2T.
exact HT.
apply: subset_trans. exact H1. by rewrite Hadj.
apply: subset_trans. exact H2. by rewrite Hadj.
Qed.
Lemma Galois_snd_lift (Hadj : Adjunction_law τ__π σ__π) :
forall S, SCH2 S ->
S ⊆ (sCl_σ (sCl_τ S)).
Proof.
move => S SCH2S [bs1 bs2] HS.
exists (σ__π (τ__π bs1)), (σ__π (τ__π bs2)). split.
+ exists (τ__π bs1), (τ__π bs2). repeat (split; auto).
++ exists (τ__π bs1), (τ__π bs2). repeat (split; auto).
+++ now exists bs1, bs2.
rewrite /=. by repeat rewrite -Hadj.
Qed.
Theorem Adj_sCl_σR2rSCHP_iff_sCl_τR2rSCHP :
Adjunction_law τ__π σ__π ->
(forall P1 P2 T, SCH2 T -> sCl_σR2rhP P1 P2 T) <->
(forall P1 P2 S, SCH2 S -> sCl_τR2rhP P1 P2 S).
Proof.
move => H_adj. split.
- move => Hσ P1 P2 S S_ssc Hrsat_src.
have Hfoo: SCH2 (sCl_τ S) by apply: sCl2_SCH2.
have Hfoo': rsat__S P1 P2 (sCl_σ (sCl_τ S)).
{ apply: rhsat2_upper_closed.
exact Hrsat_src.
by apply: Galois_snd_lift. }
by move: (Hσ P1 P2 (sCl_τ S) Hfoo Hfoo') => Hsat__T.
- move => Hτ P1 P2 T T_ssc Hrrsat_tgt.
have H : rsat__T (P1 ↓) (P2 ↓) (sCl_τ (sCl_σ T)).
{ apply: Hτ. apply: sCl2_SCH2. assumption. }
apply: rhsat2_upper_closed. exact H.
by apply: Galois_fst_lift.
Qed.
End Robust2relSSCHPreservation.