-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRobustTraceProperty.v
172 lines (130 loc) · 5.51 KB
/
RobustTraceProperty.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
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 RobustPreservation.
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 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 := rsat Source_Semantics.
Local Definition rsat__T := rsat 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.
Variable σ : prop__T -> prop__S.
Variable τ : prop__S -> prop__T.
Definition σRP (P : par__S) (π__T : (trace__T -> Prop)) :=
rsat__S P (σ π__T) -> rsat__T (P ↓) π__T.
Definition σRTP := forall P π__T, σRP P π__T.
Lemma contra_σRP (P : par__S) (π__T : prop__T) :
(σRP P π__T) <-> ((exists C__T t, sem__T ( plug__T (P↓) C__T) t /\ ~ (π__T t)) ->
(exists C__S s, sem__S ( plug__S P C__S) s /\ ~ (σ π__T) s)).
Proof.
rewrite /σRP. by rewrite [_ -> _] contra !neg_rsat.
Qed.
Lemma contra_σRTP :
σRTP <-> (forall P π__T, (exists C__T t, sem__T (plug__T (P ↓) C__T) t /\ ~ (π__T t)) ->
(exists C__S s, sem__S (plug__S P C__S) s /\ ~ (σ π__T) s)).
Proof.
rewrite /σRTP.
split => H P π__T; by move/contra_σRP: (H P π__T).
Qed.
Definition τRP (P : par__S) (π__S : prop__S) :=
rsat__S P π__S -> rsat__T (P ↓) (τ π__S).
Definition τRTP := forall P π__S, τRP P π__S.
Lemma contra_τRP (P : par__S) (π__S : prop__S) :
(τRP P π__S) <-> ((exists C__T t, sem__T ( plug__T (P↓) C__T) t /\ ~ (τ π__S) t) ->
(exists C__S s, sem__S (plug__S P C__S) s /\ ~ π__S s)).
Proof.
rewrite /τRP. by rewrite [_ -> _] contra !neg_rsat.
Qed.
Lemma contra_τRTP :
τRTP <-> (forall P π__S, ((exists C__T t, sem__T ( plug__T (P↓) C__T) t /\ ~ (τ π__S) t) ->
(exists C__S s, sem__S (plug__S P C__S) s /\ ~ π__S s))).
Proof.
rewrite /τRTP.
split => H P π__S; by move/contra_τRP: (H P π__S).
Qed.
Theorem G_σRTP_iff_τRTP :
(Galois_fst τ σ) -> (Galois_snd τ σ) -> (σRTP <-> τRTP).
Proof.
move => G1 G2. split.
- move => Hσ P πs Hrsat_src. apply: (Hσ P (τ πs)).
apply: rsat_upper_closed. exact Hrsat_src. by apply: G1.
- move => Hτ P πt Hrrsat_tgt.
have H : rsat__T (P ↓) (τ (σ πt)) by apply: Hτ.
apply: rsat_upper_closed. exact H. by apply: G2.
Qed.
Corollary Adj_σRTP_iff_τRTP :
Adjunction_law τ σ -> (σRTP <-> τRTP).
Proof.
rewrite Galois_equiv. move => [ms [mt [G1 G2]]].
by apply: G_σRTP_iff_τRTP.
Qed.
Section General.
(*
Here we show that for arbitraty X ⊆ prop__S and Y ⊆ prop__T
if α : X ⇆ Y : γ is a Galois connection then
αRXP ↔ γRYP
*)
Local Definition hprop__S : Type := hprop trace__S.
Local Definition hprop__T : Type := hprop trace__T.
Variable X : hprop__S.
Variable Y : hprop__T.
Variable α : prop__S -> prop__T.
Variable γ : prop__T -> prop__S.
Variable αXY : forall π__S, X π__S -> Y (α π__S).
Variable γYX : forall π__T, Y π__T -> X (γ π__T).
Hypothesis Galois_fst_X_Y :
forall π__S, X π__S -> π__S ⊆ γ (α π__S).
Hypothesis Galois_snd_X_Y :
forall π__T, Y π__T -> α (γ π__T) ⊆ π__T.
Definition γRP (P : par__S) (π__T : (trace__T -> Prop)) :=
rsat__S P (γ π__T) -> rsat__T (P ↓) π__T.
Definition γRYP := forall P π__T, Y π__T -> γRP P π__T.
Definition αRP (P : par__S) (π__S : prop__S) :=
rsat__S P π__S -> rsat__T (P ↓) (α π__S).
Definition αRXP := forall P π__S, X π__S -> αRP P π__S.
Theorem Generalization_σRTP_iff_τRTP : γRYP <-> αRXP.
Proof.
split.
- move => HγRYP P π__S Xπ__S Hsrc.
have γHsrc : rsat__S P (γ (α π__S)).
{ apply: rsat_upper_closed. exact: Hsrc.
by apply: Galois_fst_X_Y. }
move: (HγRYP P (α π__S) (αXY Xπ__S) γHsrc).
by [].
- move => Hα P π__T Yπ__T Hrrsat_tgt.
have H : rsat__T (P ↓) (α (γ π__T)).
{ apply: Hα. by apply: γYX. exact: Hrrsat_tgt. }
apply: rsat_upper_closed. exact H. by apply: Galois_snd_X_Y.
Qed.
End General.
End RobustPreservation.