This repository has been archived by the owner on Jul 23, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathtemp_commented_code.v
286 lines (278 loc) · 14.1 KB
/
temp_commented_code.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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(* Inductive LK : Node -> list prop -> list prop -> list prop -> list prop -> Prop :=
(* Axiom : A |- A *)
| LKA: forall p : prop, p +' [] ⇒ p +'' [] >< leaf
(* Structral Rules *)
(* Weakening *)
|LKrW: forall G1 G2 D1 D2 (a: prop) n, G1 +' G2 ⇒ D1 +'' D2 >< n-> G1 +' G2 ⇒ a :: D1 +'' D2 >< onen n
|LKlW: forall G1 G2 D1 D2 (a: prop) n, G1 +' G2 ⇒ D1 +'' D2 >< n -> a :: G1 +' G2 ⇒ D1 +'' D2 >< onen n
(* Exchange *)
|LKrE: forall G1 G2 D1 D2 (a b : prop) n, G1 +' G2 ⇒ (a :: b :: D1) +'' D2 >< n ->
G1 +' G2 ⇒ (b :: a :: D1) +'' D2 >< onen n
|LKlE: forall G1 G2 D1 D2 (a b : prop) n, (a :: b :: G1) +' G2 ⇒ D1 +'' D2 >< n ->
(b :: a :: G1) +' G2 ⇒ D1 +'' D2 >< onen n
(* Contraction *)
|LKrC: forall G1 G2 D1 D2 (a : prop) n, G1 +' G2 ⇒ (a :: a :: D1) +'' D2 >< n -> G1 +' G2 ⇒ (a :: D1) +'' D2 >< onen n
|LKlC: forall G1 G2 D1 D2 (a : prop) n, a :: a :: G1 +' G2 ⇒ D1 +'' D2 >< n -> a :: G1 +' G2 ⇒ D1 +'' D2 >< onen n
(* Logical Rules *)
(* Conjunction *)
|LKrA: forall G1 G2 D1 D2 (a b: prop) m n,
G1 +' G2 ⇒ a :: D1 +'' D2 >< m-> G1 +' G2⇒ b :: D1 +'' D2 >< n -> G1 +' G2 ⇒ (a ∧ b) :: D1 +'' D2 >< twon m n
|LKl1A: forall G1 G2 D1 D2 (a b : prop) n,
a :: G1 +' G2 ⇒ D1 +'' D2 >< n -> (a ∧ b) :: G1 +' G2 ⇒ D1 +'' D2 >< onen n
|LKl2A: forall G1 G2 D1 D2 (a b : prop) n,
b :: G1 +' G2 ⇒ D1 +'' D2 >< n -> (a ∧ b) :: G1 +' G2 ⇒ D1 +'' D2 >< onen n
(* Disjunction *)
|LKr1O: forall G1 G2 D1 D2 (a b : prop) n,
G1 +' G2 ⇒ a :: D1 +'' D2 >< n -> G1 +' G2 ⇒ (a ∨ b) :: D1 +'' D2 >< onen n
|LKr2O: forall G1 G2 D1 D2 (a b : prop) n,
G1 +' G2 ⇒ b :: D1 +'' D2 >< n -> G1 +' G2 ⇒ (a ∨ b) :: D1 +'' D2 >< onen n
|LKlO: forall G1 G2 D1 D2 (a b : prop) m n,
a :: G1 +' G2 ⇒ D1 +'' D2 >< m -> b :: G1 +' G2 ⇒ D1 +'' D2 >< n -> (a ∨ b) :: G1 +' G2 ⇒ D1 +'' D2 >< twon m n
(* Negation *)
|LKrN: forall G1 G2 D1 D2 (a : prop) n, a :: G1 +' G2 ⇒ D1 +'' D2 >< n -> G1 +' G2 ⇒ (¬ a) :: D1 +'' D2 >< onen n
|LKlN: forall G1 G2 D1 D2 (a : prop) n, G1 +' G2 ⇒ a :: D1 +'' D2 >< n -> (¬ a) :: G1 +' G2 ⇒ D1 +'' D2 >< onen n
(* Implication *)
|LKrI: forall G1 G2 D1 D2 (a b : prop) n, a :: G1 +' G2 ⇒ b :: D1 +'' D2 >< n ->
G1 +' G2 ⇒ (a ⊃ b) :: D1 +'' D2 >< onen n
|LKlI: forall G1 G2 D1 D2 (a b : prop) m n,
G1 +' G2 ⇒ a :: D1 +'' D2 >< m -> b :: G1 +' G2 ⇒ D1 +'' D2 >< n->
(a ⊃ b) :: G1 +' G2 ⇒ D1 +'' D2 >< twon m n
where "G1 +' G2 ⇒ D1 +'' D2 >< n" := (LK n G1 G2 D1 D2). *)
(* Theorem LK_Interpol_strong: forall n (G1 G2 D1 D2 : list prop),
G1 ++ G2 ⇒ D1 ++ D2 >< n ->
(exists (c : prop) m1 m2, G1 ⇒ c :: D1 >< m1 /\ c :: G2 ⇒ D2 >< m2
(* /\ lil (atom_lista c) (list_intersect (atom_list(G1 ++ G2)) (atom_list(D1 ++ D2)))). *)
(* /\ (forall (x : atom), (In_prop x c) -> ((In_list_prop x (G1 ++ G2) /\ In_list_prop x (D1 ++ D2))))). *)
/\ (atoms_of c) ⊆ ( (atoms_of_list (G1 ++ G2)) ∩ (atoms_of_list (D1 ++ D2)))).
induction n; intros G1 G2 D1 D2 H; inversion H.
- destruct G1, G2, D1, D2; try discriminate; simpl in *; inversion H0; inversion H1; subst; try (rewrite app_nil_r in *).
+ exists (p1 ∨ ¬ p1), (☉ (☉ (☉ (☉ (☉ leaf))))), (☉ leaf). repeat split.
* constructor 6. constructor 11.
apply (LKrE [] [] [] (p1 ∨ ¬ p1) (p1) (☉ (☉ leaf))). simpl.
constructor 12. constructor 14. constructor 1.
* constructor 3. constructor 1.
* simpl. rewrite union_idr.
rewrite union_refl. rewrite intersection_refl.
apply incl_reflexive.
+ subst.
exists (¬ p1), (☉ leaf), (☉ leaf). repeat split.
* constructor 14. apply H.
* constructor 15. apply H.
* simpl. rewrite union_idr. rewrite intersection_refl.
apply incl_reflexive.
+ destruct D1; inversion H6.
+ subst. exists p1, leaf, leaf. repeat split.
* constructor 1.
* constructor 1.
* rewrite union_idr. rewrite intersection_refl.
apply incl_reflexive.
+ subst; simpl in *.
exists (p1 ∧ ¬ p1), (☉ leaf), (☉ (☉ (☉ (☉ (☉ leaf))))). repeat split.
* constructor 2. constructor 1.
* constructor 7. constructor 9.
apply (LKlE [] [] [] (p1 ∧ ¬ p1) (p1) (☉ (☉ leaf))). simpl.
constructor 10. constructor 15. constructor 1.
* simpl. rewrite union_idr.
rewrite union_refl. rewrite intersection_refl.
apply incl_reflexive.
+ destruct D1; inversion H6.
+ destruct G1; inversion H4.
+ destruct G1; inversion H4.
+ destruct G1; inversion H4.
- destruct D1, D2; simpl in *; try discriminate; try inversion H1; subst; simpl in *.
+ rewrite <- app_nil_l in H3.
specialize (IHn G1 G2 [] (D2) H3) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, m1, (☉ m2). repeat split.
* apply IH1.
* constructor 2. apply IH2.
* apply incl_union_inter_absorb. simpl in IH3. auto.
+ specialize (IHn G1 G2 D1 [] H3) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, (☉ (☉ m1)), m2. repeat split.
* apply (LKrE G1 [] D1 p c (☉ m1)). simpl.
constructor 2. apply IH1.
* apply IH2.
* apply incl_union_inter_absorb. auto.
+ specialize (IHn G1 G2 D1 (p0 :: D2) H3) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, (☉ (☉ m1)), m2. repeat split.
* apply (LKrE G1 [] D1 p c (☉ m1)).
constructor 2. apply IH1.
* apply IH2.
* apply incl_union_inter_absorb. auto.
- destruct G1, G2; simpl in *; try discriminate; try inversion H1; subst; simpl in *.
+ specialize (IHn [] G2 D1 (D2) H2) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, m1, (☉ (☉ m2)). repeat split.
* apply IH1.
* apply (LKlE [] G2 D2 p c (☉ m2)). simpl.
constructor 3. apply IH2.
* apply incl_union_absorb_inter. auto.
+ specialize (IHn G1 [] D1 (D2) H2) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, (☉ m1), m2. repeat split.
* constructor 3. apply IH1.
* apply IH2.
* apply incl_union_absorb_inter. auto.
+ specialize (IHn G1 (p0 :: G2) D1 D2 H2) as H'.
destruct H' as [c [m1 [m2 [IH1 [IH2 IH3]]]]].
exists c, (☉ m1), m2. repeat split.
* constructor 3. apply IH1.
* apply IH2.
* apply incl_union_absorb_inter. auto.
- apply exchg_partition in H1.
destruct H1 as [[H1 H1'] | [[D3 [H1 H1']] | [[H1 H1'] | [[H1 H1']| [[H1 H1'] | [[D3 [H1 H1']] | [H1 H1'] ]]]]]].
--
specialize (IHn G1 G2 [] (D ++ a :: b :: D') H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c,m1 ,(☉ m2). repeat split.
+ subst. apply H6.
+ subst. constructor 4. apply H6'.
+ simpl. rewrite (atoms_list_app D (b :: a :: D')).
simpl. rewrite (union_assoc (^V b) (^V a) (atoms_of_list D')).
rewrite (union_comm (^V b) (^V a) ).
simpl in H7. rewrite (atoms_list_app D (a :: b :: D')) in H7.
simpl in H7. rewrite (union_assoc (^V a) (^V b) (atoms_of_list D')) in H7. apply H7.
-- rewrite H1' in H3. rewrite <- app_assoc in H3.
specialize (IHn G1 G2 D1 (D3 ++ a :: b :: D') H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c, m1, (☉ m2). repeat split.
+ apply H6.
+ rewrite H1. constructor 4. apply H6'.
+ rewrite (atoms_list_app D (b :: a :: D')).
rewrite H1'. rewrite (atoms_list_app D1 D3).
rewrite <- union_assoc. simpl. rewrite (union_assoc (^V b) (^V a) (atoms_of_list D')).
rewrite (union_comm (^V b) (^V a) ).
rewrite (atoms_list_app D1 (D3 ++ a :: b :: D')) in H7.
rewrite (atoms_list_app D3 (a :: b :: D')) in H7.
simpl in H7. rewrite (union_assoc (^V a) (^V b) (atoms_of_list D')) in H7. apply H7.
--
specialize (IHn G1 G2 D (a :: b :: D') H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c, m1, (☉ m2). repeat split.
+ rewrite H1. apply H6.
+ rewrite H1'. rewrite <- app_nil_l. constructor 4. simpl. apply H6'.
+ admit.
-- rewrite app_cons in H3. rewrite app_cons in H3.
rewrite app_assoc in H3. rewrite app_assoc in H3. rewrite <- (app_assoc D [a] [b]) in H3.
specialize (IHn G1 G2 (D ++ [a] ++ [b]) (D') H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
rewrite app_comm_cons in H6.
apply LKr_partition_mid_l in H6. destruct H6 as [m' H6].
rewrite app_assoc in H6. rewrite (app_cons [a] D c) in H6.
rewrite <- app_assoc in H6.
simpl in H6.
apply (LKr2O G1 (c :: D ++ [b]) c a m') in H6.
apply (LKrE G1 [] (D ++ [b]) (c ∨ a) c (☉ m')) in H6.
simpl in H6.
apply (LKr1O G1 (c ∨ a :: D ++ [b]) c a (☉ (☉ m'))) in H6.
apply (LKrC G1 (D ++ [b]) (c ∨ a) (☉ (☉ (☉ m')))) in H6.
specialize (LKA a) as H6''.
specialize (LKl_app_list [a] G2 [a] leaf H6'') as H8.
destruct H8 as [m3 H8].
apply LKl_cons_app in H8. destruct H8 as [m'' H8].
apply (LKrW (c :: G2) (D') a m2) in H6'.
apply (LKr_app_list ([a] ++ G2) [a] D' m'') in H8.
destruct H8 as [m4 H8]. apply (LK_cons_app ([a] ++ G2) [a] D' m4) in H8.
destruct H8 as [m5 H8]. simpl in H8.
specialize (LKlO G2 (a :: D') c a (☉ m2) m5 H6' H8) as H9.
exists (c ∨ a) , (☉ (☉ (☉ (☉ m')))), (☉ m2 ≍ m5).
repeat split.
+ rewrite H1. apply H6.
+ rewrite H1'. apply H9.
+ simpl. admit.
(* rewrite exchg_atoms_of_list.
replace (D ++ a :: b :: D') with ((D ++ [a] ++ [b]) ++
D').
apply H7. *)
-- replace (D ++ a :: b :: D') with ((D ++ a :: b) ++ D') in H3.
specialize (IHn G1 G2 (D ++ a :: b) (D') H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c, (☉ m1), m2. repeat split.
+ rewrite H1. apply (LKrE G1 (c::D) [] a b m1). simpl. apply H6.
+ rewrite H1'. apply H6'.
+ rewrite exchg_atoms_of_list.
rewrite <- app_assoc in H7. simpl in H7. auto.
+ rewrite <- app_assoc. simpl. reflexivity.
-- rewrite H1' in H3. rewrite app_comm_cons in H3. rewrite app_comm_cons in H3. rewrite app_assoc in H3.
specialize (IHn G1 G2 (D ++ a :: b :: D3) (D2) H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c, (☉ m1), m2. repeat split.
+ subst. apply (LKrE G1 (c::D) D3 a b m1). simpl. apply H6.
+subst. apply H6'.
+ rewrite exchg_atoms_of_list.
replace ((D ++ a :: b :: D3) ++ D2) with (D ++ a :: b :: D') in H7.
auto.
{rewrite <- app_assoc. simpl. rewrite H1'. reflexivity. }
-- rewrite <- app_nil_r in H3.
specialize (IHn G1 G2 (D ++ a :: b :: D') [] H3) as H'.
destruct H' as [c [m1 [m2 [H6 [H6' H7]]]]].
exists c, (☉ m1), m2. repeat split.
+ subst. apply (LKrE G1 (c::D) D' a b m1). apply H6.
+ subst. apply H6'.
+ rewrite exchg_atoms_of_list. rewrite app_nil_r in H7.
auto.
- admit.
-admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- subst. destruct D1, D2; inversion H2; subst.
+ specialize (IHn1 G1 G2 [] (a :: D2) H4) as H6. destruct H6 as [c0 [m1 [m2 [H6 [H6' H7]]]]].
specialize (IHn2 G1 G2 [] (b :: D2) H5) as H8. destruct H8 as [c1 [m1' [m2' [H8 [H8' H9]]]]].
exists (c0 ∧ c1), ( m1 ≍ m1'), ( (☉ m2) ≍ (☉ m2')). repeat split.
* constructor 8. apply H6. apply H8.
* constructor 8.
** constructor 9. apply H6'.
** constructor 10. apply H8'.
* simpl. simpl in H9. simpl in H7.
apply (incl_union_inter_add).
** apply H7.
** apply H9.
+ simpl in *.
specialize (IHn1 G1 G2 (a :: D1) [] H4) as H6. destruct H6 as [c0 [m1 [m2 [H6 [H6' H7]]]]].
specialize (IHn2 G1 G2 (b :: D1) [] H5) as H8. destruct H8 as [c1 [m1' [m2' [H8 [H8' H9]]]]].
exists (c0 ∨ c1),
(☉ ((☉ ☉ m1) ≍ (☉ ☉ m1'))),
(m2 ≍ m2'). repeat split.
* apply (LKrE G1 [] D1 (a ∧ b) (c0 ∨ c1) ((☉ ☉ m1) ≍ (☉ ☉ m1'))).
simpl. constructor 8.
** apply (LKrE G1 [] D1 (c0 ∨ c1) (a) (☉ m1)).
simpl. constructor 11. apply H6.
** apply (LKrE G1 [] D1 (c0 ∨ c1) (b) (☉ m1')).
simpl. constructor 12. apply H8.
* constructor 13.
** apply H6'.
** apply H8'.
* simpl. simpl in H9. simpl in H7.
apply (incl_union_inter_add).
** apply H7.
** apply H9.
+ simpl in *.
specialize (IHn1 G1 G2 (a :: D1) (p0 :: D2 ) H4) as H6. destruct H6 as [c0 [m1 [m2 [H6 [H6' H7]]]]].
specialize (IHn2 G1 G2 (b :: D1) (p0 :: D2 ) H5) as H8. destruct H8 as [c1 [m1' [m2' [H8 [H8' H9]]]]].
exists (c0 ∨ c1),
(☉ ((☉ ☉ m1) ≍ (☉ ☉ m1'))),
(m2 ≍ m2'). repeat split.
* apply (LKrE G1 [] D1 (a ∧ b) (c0 ∨ c1) ((☉ ☉ m1) ≍ (☉ ☉ m1'))).
simpl. constructor 8.
** apply (LKrE G1 [] D1 (c0 ∨ c1) (a) (☉ m1)).
simpl. constructor 11. apply H6.
** apply (LKrE G1 [] D1 (c0 ∨ c1) (b) (☉ m1')).
simpl. constructor 12. apply H8.
* constructor 13.
** apply H6'.
** apply H8'.
* simpl. simpl in H9. simpl in H7.
apply (incl_union_inter_add).
** apply H7.
** apply H9.
- admit.
- admit.
Admitted. *)