-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDef.v
113 lines (85 loc) · 3.38 KB
/
Def.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
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.
Notation "W ↓" := (compile_whole _ _ _ W) (at level 50).
Section Preservation.
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 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 cmp := compile_whole Source Target compilation_chain.
Local Notation "W ↓" := (cmp W) (at level 50).
Variable σ : prop__T -> prop__S.
Variable τ : prop__S -> prop__T.
Definition σP (W : prg__S) (π__T : (trace__T -> Prop)) :=
sat__S W (σ π__T) -> sat__T (W ↓) π__T.
Definition σTP := forall W π__T, σP W π__T.
Lemma contra_σP (W : prg__S) (π__T : prop__T) :
(σP W π__T) <-> ((exists t, sem__T (W ↓) t /\ ~ (π__T t)) ->
(exists s, sem__S W s /\ ~ (σ π__T) s)).
Proof.
rewrite /σP. by rewrite [_ -> _] contra !neg_sat.
Qed.
Lemma contra_σTP :
σTP <-> (forall W π__T, (exists t, sem__T (W ↓) t /\ ~ (π__T t)) ->
(exists s, sem__S W s /\ ~ (σ π__T) s)).
Proof.
rewrite /σTP.
split => H W π__T; by move/contra_σP: (H W π__T).
Qed.
Definition τP (W : prg__S) (π__S : prop__S) :=
sat__S W π__S -> sat__T (W ↓) (τ π__S).
Definition τTP := forall W π__S, τP W π__S.
Lemma contra_τP (W : prg__S) (π__S : prop__S) :
(τP W π__S) <-> ((exists t, sem__T (W ↓) t /\ ~ (τ π__S) t) ->
(exists s, sem__S W s /\ ~ π__S s)).
Proof.
rewrite /τP. by rewrite [_ -> _] contra !neg_sat.
Qed.
Lemma contra_τTP :
τTP <-> (forall W π__S, (exists t, sem__T (W ↓) t /\ ~ (τ π__S) t) ->
(exists s, sem__S W s /\ ~ π__S s)).
Proof.
rewrite /τTP.
split => H W π__S; by move/contra_τP: (H W π__S).
Qed.
Theorem G_σTP_iff_τTP :
(Galois_fst τ σ) -> (Galois_snd τ σ) -> (σTP <-> τTP).
Proof.
move => G1 G2. split.
- move => Hσ P πs Hsat_src. apply: (Hσ P (τ πs)).
apply: sat_upper_closed. exact Hsat_src. by apply: G1.
- move => Hτ P πt Hrsat_tgt.
have H : sat__T (P ↓) (τ (σ πt)) by apply: Hτ.
apply: sat_upper_closed. exact H. by apply: G2.
Qed.
Corollary Adj_σTP_iff_τTP :
Adjunction_law τ σ -> (σTP <-> τTP).
Proof.
rewrite Galois_equiv. move => [ms [mt [G1 G2]]].
by apply: G_σTP_iff_τTP.
Qed.
End Preservation.