-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathComposition.v
172 lines (139 loc) · 6.87 KB
/
Composition.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 Coq.Logic.ClassicalFacts.
Require Import MyNotation.
Require Import Setoid.
Require Import FunctionalExtensionality.
Require Import Setoid.
Require Import Galois.
Require Import LanguageModel.
Require Import TraceModel.
Require Import Properties.
Require Import ChainModel.
Require Import Def.
Require Import TraceCriterion.
Section Conjunction.
Axiom prop_ext : prop_extensionality.
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 beh__S := beh Source_Semantics.
Local Definition sem__T := sem Target_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 cmp := compile_whole Source Target compilation_chain.
Local Notation "W ↓" := (cmp W) (at level 50).
(* the two relations and their conjunction *)
Variable rel1 rel2 : trace__S -> trace__T -> Prop.
Definition rel_cap : trace__S -> trace__T -> Prop :=
fun s t => rel1 s t /\ rel2 s t.
(* the induced connections *)
Local Definition adjunction1 := induced_connection rel1.
Local Definition adjunction2 := induced_connection rel2.
Local Definition τ1 : prop__S -> prop__T := α adjunction1.
Local Definition σ1 : prop__T -> prop__S := γ adjunction1.
Local Definition τ2 : prop__S -> prop__T := α adjunction2.
Local Definition σ2 : prop__T -> prop__S := γ adjunction2.
Definition τ : prop__S -> prop__T := fun π__S => (fun t => τ1 π__S t /\ τ2 π__S t).
Definition rel : trace__S -> trace__T -> Prop :=
fun s t => (τ (fun x => x = s) t).
Lemma rel_is_relcap : rel = rel_cap.
Proof.
apply: functional_extensionality => s.
apply: functional_extensionality => t.
apply: prop_ext.
rewrite /rel /rel_cap /τ /τ1 /τ2 /α /= /low_rel. split.
- move => [[s1 [Heq1 Hrel1]] [s2 [Heq2 Hrel2]]]. by subst.
- by firstorder.
Qed.
(* Local Definition adjunction := induced_connection rel. *)
(* Lemma τ_induced_by_rel : τ = α adjunction. *)
(* Proof. *)
(* apply: functional_extensionality => π__S. *)
(* apply: functional_extensionality => t. *)
(* apply: prop_ext. *)
(* rewrite /α /τ /τ1 /τ2 /= /low_rel. *)
Local Definition CCtilde1 := rel_TC compilation_chain Source_Semantics Target_Semantics rel1.
Local Definition τTP1 := τTP compilation_chain Source_Semantics Target_Semantics τ1.
Local Definition trinity1 := rel_TC_τTP compilation_chain Source_Semantics Target_Semantics rel1.
Local Definition CCtilde2 := rel_TC compilation_chain Source_Semantics Target_Semantics rel2.
Local Definition τTP2 := τTP compilation_chain Source_Semantics Target_Semantics τ2.
Local Definition trinity2 := rel_TC_τTP compilation_chain Source_Semantics Target_Semantics rel2.
Local Definition CCtilde_cap := rel_TC compilation_chain Source_Semantics Target_Semantics rel_cap.
Local Definition τTP := τTP compilation_chain Source_Semantics Target_Semantics τ.
(* Lemma CCtilde_cap_τTP : CCtilde_cap <-> τTP. *)
(* Proof. *)
(* rewrite /CCtilde_cap -rel_is_relcap. *)
(* setoid_rewrite contra_τTP. split. *)
(* - move => Htilde W π [t [Hsemt Hτ]]. *)
(* destruct (Htilde W t Hsemt) as [s [Hrel_s_t Hsems]]. *)
(* exists s. split; auto. move => s_in_π. apply: Hτ. *)
(* move: Hrel_s_t. rewrite /rel /τ /τ1 /τ2 /α /= /low_rel => Hrel. *)
(* move: Hrel => [[y1 [Heq1 Hrel1]] [y2 [Heq2 Hrel2]]]. subst. *)
(* split; by exists s. *)
(* - move => Hτ W t HsemWt. *)
(* have H : (forall s1 s2, sem__S W s1 -> sem__S W s2 -> rel1 s1 t -> rel2 s2 t -> s1 <> s2) \/ *)
(* (exists s1 s2, sem__S W s1 /\ sem__S W s2 /\ rel1 s1 t /\ rel2 s2 t /\ s1 = s2). *)
(* { case: (classic (forall s1 s2, sem__S W s1 -> sem__S W s2 -> rel1 s1 t -> rel2 s2 t -> s1 <> s2)); auto. *)
(* rewrite not_forall_ex_not. move => [s1 H]. move /not_forall_ex_not : H => [s2 H]. *)
(* right. exists s1, s2. *)
(* repeat (move /not_imp: H => [h H]; split; auto; clear h). *)
(* by apply: NNPP. } *)
(* case: H. *)
(* move => H. exfalso. *)
(* have cc1 : CCtilde1. *)
(* { setoid_rewrite trinity1. setoid_rewrite contra_τTP. *)
(* move => Ws π__S [t0 [H1 H2]]. destruct (Hτ Ws π__S) as [s Hs]. *)
(* exists t0. split; auto. rewrite /τ. move => [Htau1 Htau2]. *)
(* by apply: H2. *)
(* exists s; auto. } *)
(* have cc2 : CCtilde2. *)
(* { setoid_rewrite trinity2. setoid_rewrite contra_τTP. *)
(* move => Ws π__S [t0 [H1 H2]]. destruct (Hτ Ws π__S) as [s Hs]. *)
(* exists t0. split; auto. rewrite /τ. move => [Htau1 Htau2]. *)
(* by apply: H2. *)
(* exists s; auto. } *)
(* destruct (cc1 W t HsemWt) as [s1 [HsemWs1 Hrel1]]. *)
(* destruct (cc2 W t HsemWt) as [s2 [HsemWs2 Hrel2]]. *)
(* have not_t : ~ (τ (fun s => rel s t )) t by admit. *)
(* case: (Hτ W (fun s => rel s t )). *)
(* { exists t. split; auto. } *)
(* move => s [HsemWs K]. move /de_morgan1: K. rewrite -dne. *)
(* rewrite rel_is_relcap /rel_cap. move => [[k11 k12]| k2]; try now auto. *)
(* by apply: (H s s). *)
(* (* 2nd case *) *)
(* by firstorder. *)
(* Admitted. *)
Theorem TPtau_for_conjunction :
CCtilde1 /\ CCtilde2 -> τTP.
Proof.
move => [H1 H2].
have Hτ1 : τTP1 by move /trinity1 : H1.
have Hτ2 : τTP2 by move /trinity2 : H2.
move => W π__S sat_src. rewrite /τ. split.
by apply: (Hτ1 W). by apply: (Hτ2 W).
Qed.
(* The problem is that τ does not coincide with the abstraction of
the galois connection induced by ~ So that in general no involution in possible
(see Lemma 2.9 in the paper) *)
(* Theorem conjunction_intersection : CCtilde1 /\ CCtilde2 <-> CCtilde_cap. *)
(* Proof. *)
(* rewrite CCtilde_cap_τTP. split. *)
(* - exact TPtau_for_conjunction. *)
(* - setoid_rewrite trinity1. setoid_rewrite trinity2. *)
(* by firstorder. *)
(* Qed. *)
End Conjunction.