-
Notifications
You must be signed in to change notification settings - Fork 1
/
21-words-helpers.mm1
210 lines (189 loc) · 11.5 KB
/
21-words-helpers.mm1
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
import "11-definedness-normalization.mm1";
import "20-theory-words.mm0";
import "13-fixedpoints.mm1";
--- Helpers for concat
theorem eFresh_concat {x: EVar} (phi psi: Pattern x)
(fresh1: $ _eFresh x phi $)
(fresh2: $ _eFresh x psi $):
$ _eFresh x (phi . psi) $ =
'(eFresh_app (eFresh_app eFresh_disjoint fresh1) fresh2);
theorem positive_in_concat {X: SVar} (phi1 phi2: Pattern X)
(h1: $ _Positive X phi1 $) (h2: $ _Positive X phi2 $): $ _Positive X (phi1 . phi2) $
= '(positive_in_app (positive_in_app positive_disjoint h1) h2);
theorem sSubst_concat {X: SVar} (psi rho1 rho2 phi1 phi2: Pattern X)
(h1: $ Norm (s[ psi / X ] phi1) rho1 $)
(h2: $ Norm (s[ psi / X ] phi2) rho2 $):
$ Norm (s[ psi / X ] (phi1 . phi2)) (rho1 . rho2) $ =
'(_sSubst_app (_sSubst_app sSubstitution_disjoint h1) h2);
theorem sSubst_concat_l {X: SVar} (phi psi rho: Pattern X) (gamma: Pattern)
(h: $ Norm (s[ phi / X ] psi) rho $):
$ Norm (s[ phi / X ] (psi . gamma)) (rho . gamma) $ =
'(sSubst_concat h sSubstitution_disjoint);
theorem sSubst_concat_r {X: SVar} (phi psi rho: Pattern X) (gamma: Pattern)
(h: $ Norm (s[ phi / X ] psi) rho $):
$ Norm (s[ phi / X ] (gamma . psi)) (gamma . rho) $ =
'(sSubst_concat sSubstitution_disjoint h);
theorem framing_concat_l (h: $phi -> psi$): $phi . rho -> psi . rho$ =
'(app_framing_l @ app_framing_r h);
theorem framing_concat_r (h: $phi -> psi$): $rho . phi -> rho . psi$ =
'(app_framing_r h);
theorem _eSubst_concat {x: EVar} (phi psi1 psi2 rho1 rho2: Pattern x)
(h1: $ Norm (e[ phi / x ] psi1) rho1 $)
(h2: $ Norm (e[ phi / x ] psi2) rho2 $):
$ Norm (e[ phi / x ] (psi1 . psi2)) (rho1 . rho2) $ =
'(_eSubst_app (_eSubst_app eSubstitution_disjoint h1) h2);
theorem _eSubst_concat_l {x: EVar} (phi psi rho: Pattern x) (gamma: Pattern)
(h: $ Norm (e[ phi / x ] psi) rho $):
$ Norm (e[ phi / x ] (psi . gamma)) (rho . gamma) $ =
'(_eSubst_concat h eSubstitution_disjoint);
theorem _eSubst_concat_r {x: EVar} (phi psi rho: Pattern x) (gamma: Pattern)
(h: $ Norm (e[ phi / x ] psi) rho $):
$ Norm (e[ phi / x ] (gamma . psi)) (gamma . rho) $ =
'(_eSubst_concat eSubstitution_disjoint h);
theorem _sSubst_concat {X: SVar} (phi psi1 psi2 rho1 rho2: Pattern X)
(h1: $ Norm (s[ phi / X ] psi1) rho1 $)
(h2: $ Norm (s[ phi / X ] psi2) rho2 $):
$ Norm (s[ phi / X ] (psi1 . psi2)) (rho1 . rho2) $ =
'(_sSubst_app (_sSubst_app sSubstitution_disjoint h1) h2);
theorem _sSubst_concat_l {X: SVar} (phi psi rho: Pattern X) (gamma: Pattern)
(h: $ Norm (s[ phi / X ] psi) rho $):
$ Norm (s[ phi / X ] (psi . gamma)) (rho . gamma) $ =
'(_sSubst_concat h sSubstitution_disjoint);
theorem _sSubst_concat_r {X: SVar} (phi psi rho: Pattern X) (gamma: Pattern)
(h: $ Norm (s[ phi / X ] psi) rho $):
$ Norm (s[ phi / X ] (gamma . psi)) (gamma . rho) $ =
'(_sSubst_concat sSubstitution_disjoint h);
theorem norm_concat
(h1: $Norm phi1 phi2$)
(h2: $Norm psi1 psi2$)
: $ Norm (phi1 . psi1) (phi2 . psi2)$
= '(norm_app (norm_app norm_refl h1) h2);
theorem norm_concat_l
(h: $Norm phi1 phi2$)
: $ Norm (phi1 . psi) (phi2 . psi)$
= '(norm_app (norm_app norm_refl h) norm_refl);
theorem norm_concat_r
(h: $Norm psi1 psi2$)
: $ Norm (phi . psi1) (phi . psi2)$
= '(norm_app norm_refl h);
theorem appctx_concat_l {box: SVar} (phi: Pattern box) (psi: Pattern):
$ Norm (app[ phi / box ] (sVar box . psi)) (phi . psi) $ =
'(norm_trans appCtxL_disjoint @ norm_app (norm_trans appCtxR_disjoint @ norm_app norm_refl appCtxVar) norm_refl);
theorem appctx_concat_r {box: SVar} (psi: Pattern box) (phi: Pattern):
$ Norm (app[ psi / box ] (phi . sVar box)) (phi . psi) $ =
'(norm_trans appCtxR_disjoint @ norm_app norm_refl appCtxVar);
theorem appctx_concat_l_l {box: SVar} (phi: Pattern box) (rho psi: Pattern):
$ Norm (app[ phi / box ] ((sVar box . psi) . rho)) ((phi . psi) . rho) $ =
'(norm_trans appCtxLR @ norm_concat_l appctx_concat_l);
theorem appctx_concat_l_r {box: SVar} (phi: Pattern box) (rho psi: Pattern):
$ Norm (app[ phi / box ] ((psi . sVar box) . rho)) ((psi . phi) . rho) $ =
'(norm_trans appCtxLR @ norm_concat_l appctx_concat_r);
theorem appctx_concat_r_l {box: SVar} (phi: Pattern box) (rho psi: Pattern):
$ Norm (app[ phi / box ] (rho . (sVar box . psi))) (rho . (phi . psi)) $ =
'(norm_trans appCtxR_disjoint @ norm_concat_r appctx_concat_l);
theorem appctx_concat_r_r {box: SVar} (phi: Pattern box) (rho psi: Pattern):
$ Norm (app[ phi / box ] (rho . (psi . sVar box))) (rho . (psi . phi)) $ =
'(norm_trans appCtxR_disjoint @ norm_concat_r appctx_concat_r);
theorem propag_or_concat : $(phi1 \/ phi2) . psi -> (phi1 . psi) \/ (phi2 . psi)$
= (named '(norm (norm_imp appctx_concat_l (norm_or appctx_concat_l appctx_concat_l)) propag_or));
theorem cong_of_equiv_concat_l (h: $phi1 <-> phi2$): $(phi1 . psi) <-> (phi2 . psi)$ =
'(ibii (framing_concat_l @ anl h) (framing_concat_l @ anr h));
theorem cong_of_equiv_concat_r (h: $phi1 <-> phi2$): $(psi . phi1) <-> (psi . phi2)$ =
'(ibii (framing_concat_r @ anl h) (framing_concat_r @ anr h));
theorem cong_of_equiv_concat (h1: $phi1 <-> phi2$) (h2: $psi1 <-> psi2$): $(phi1 . psi1) <-> (phi2 . psi2)$ =
'(bitr (cong_of_equiv_concat_l h1) (cong_of_equiv_concat_r h2));
theorem eq_to_concat_bi
(h1: $ (phi1 == phi2) -> (psi1 <-> psi2) $)
(h2: $ (phi1 == phi2) -> (rho1 <-> rho2) $):
$ (phi1 == phi2) -> ((psi1 . rho1) <-> (psi2 . rho2)) $ =
'(eq_to_app_bi (eq_to_app_r_bi h1) h2);
theorem eq_to_der_bi
(h1: $ (phi1 == phi2) -> (psi1 <-> psi2) $)
(h2: $ (phi1 == phi2) -> (rho1 <-> rho2) $):
$ (phi1 == phi2) -> ((derivative psi1 rho1) <-> (derivative psi2 rho2)) $ =
(named '(eq_to_exists_bi @ eq_to_and_r_bi @ eq_to_subset_bi (norm (norm_sym @ norm_imp_r @ norm_equiv appctx_concat_r appctx_concat_r) @ eq_to_concat_bi h1 eq_to_id_bi) h2));
--- Helpers for Kleene
theorem positive_in_kleene_l_body {X: SVar} (phi: Pattern X)
(h: $ _Positive X phi $):
$ _Positive X (epsilon \/ (sVar X . phi)) $ =
'(positive_in_or positive_disjoint @ positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) h);
theorem positive_in_kleene_r_body {X: SVar} (phi: Pattern X)
(h: $ _Positive X phi $):
$ _Positive X (epsilon \/ phi . sVar X) $ =
'(positive_in_or positive_disjoint @ positive_in_app (positive_in_app positive_disjoint h) positive_in_same_sVar);
theorem cong_of_equiv_kleene {X: SVar} (phi1 phi2: Pattern X)
(h1: $ _Positive X phi1 $)
(h2: $ _Positive X phi2 $)
(h: $ phi1 <-> phi2 $):
$ (kleene X phi1) <-> (kleene X phi2) $ =
'(cong_of_equiv_mu
(positive_in_kleene_r_body h1)
(positive_in_kleene_r_body h2)
(cong_of_equiv_or_r @ cong_of_equiv_concat_l h));
--- Helpers for top_letter
theorem positive_in_top_letter {X: SVar}:
$ _Positive X top_letter $ =
'(positive_in_or positive_disjoint positive_disjoint);
theorem sSubst_top_letter {X: SVar} (psi: Pattern X):
$ Norm (s[ psi / X ] (top_letter)) (top_letter) $ = 'sSubstitution_disjoint;
theorem eSubst_top_letter {X: EVar} (psi: Pattern X):
$ Norm (e[ psi / X ] (top_letter)) (top_letter) $ = 'eSubstitution_disjoint;
--- Helpers for top_word_l
--- TODO: Define in terms of kleene_l
theorem positive_in_top_word_l_body {X: SVar}: $_Positive X (epsilon \/ sVar X . top_letter)$ =
'(positive_in_or positive_disjoint @
positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_in_top_letter);
theorem kt_top_word_l {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $psi . top_letter -> psi$): $top_word_l X -> psi$ =
'(KT positive_in_top_word_l_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ sVar X . top_letter$) @ eori base rec);
theorem unfold_r_top_word_l {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ top_word_l X . top_letter$) : $phi -> top_word_l X$ =
'(rsyl h @ norm (norm_imp_l ,(propag_s_subst 'X $epsilon \/ sVar X . top_letter$)) @ pre_fixpoint positive_in_top_word_l_body);
--- Helpers for top_word_r
--- TODO: Define in terms of kleene_r
theorem positive_in_top_word_r_body {X: SVar}: $_Positive X (epsilon \/ top_letter . sVar X)$ =
'(positive_in_or positive_disjoint @
positive_in_app (positive_in_app positive_disjoint positive_in_top_letter) positive_in_same_sVar);
theorem kt_top_word_r {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $top_letter . psi -> psi$): $top_word_r X -> psi$ =
'(KT positive_in_top_word_r_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ top_letter . sVar X$) @ eori base rec);
theorem lemma_83_top_word_r_forward
: $( epsilon \/ top_letter . top_word_r X ) -> top_word_r X $
= '(norm_lemma (norm_sym @ _sSubst_or sSubstitution_disjoint @ sSubst_concat sSubstitution_disjoint sSubstitution_in_same_sVar ) @ pre_fixpoint positive_in_top_word_r_body ) ;
theorem lemma_83_top_word_r_reverse
: $ top_word_r X -> ( epsilon \/ top_letter . top_word_r X ) $
= '(kt_top_word_r (orld id) (orrd @ framing_concat_r lemma_83_top_word_r_forward));
theorem lemma_83_top_word_r
: $( epsilon \/ top_letter . top_word_r X ) <-> top_word_r X $
= '(ibii lemma_83_top_word_r_forward lemma_83_top_word_r_reverse);
theorem unfold_r_top_word_r {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ top_letter . top_word_r X$) : $phi -> top_word_r X$ = '(rsyl h @ lemma_83_top_word_r_forward);
theorem unfold_l_top_word_r {X : SVar} (phi: Pattern X) (h: $(epsilon \/ top_letter . top_word_r X) -> phi$) : $top_word_r X -> phi$ = '(syl h lemma_83_top_word_r_reverse);
theorem unfold_kleene_lemma {X : SVar} (phi: Pattern X)
(X_fresh: $ _sFresh X phi $):
$ epsilon \/ (phi . kleene X phi) -> kleene X phi $ =
'(norm (norm_imp_l @ norm_trans ,(propag_s_subst 'Y $epsilon \/ (phi . sVar Y)$) @ norm_or_r @ norm_concat_l @ sSubstitution_fresh X_fresh) @ pre_fixpoint (positive_in_kleene_r_body @ positive_fresh X_fresh));
theorem unfold_kleene_l_lemma {X : SVar} (phi: Pattern X)
(X_fresh: $ _sFresh X phi $):
$ epsilon \/ ((kleene_l X phi) . phi) -> kleene_l X phi $ =
'(norm (norm_imp_l @ norm_trans ,(propag_s_subst 'Y $epsilon \/ (sVar Y . phi)$) @ norm_or_r @ norm_concat_r @ sSubstitution_fresh X_fresh) @ pre_fixpoint (positive_in_kleene_l_body @ positive_fresh X_fresh));
theorem unfold_kleene {X : SVar} (phi: Pattern X)
(X_fresh: $ _sFresh X phi $):
$ kleene X phi <-> epsilon \/ (phi . kleene X phi) $ =
(named '(ibii (KT (positive_in_kleene_r_body @ positive_fresh X_fresh) @ norm (norm_sym @ norm_imp_l @ norm_trans ,(propag_s_subst 'Y $epsilon \/ (phi . sVar Y)$) @ norm_or_r @ norm_concat_l @ sSubstitution_fresh X_fresh) @
orim2 ,(framing_subst '(unfold_kleene_lemma X_fresh) 'appctx_concat_r)) @ unfold_kleene_lemma X_fresh));
theorem unfold_kleene_l {X : SVar} (phi: Pattern X)
(X_fresh: $ _sFresh X phi $):
$ kleene_l X phi <-> epsilon \/ ((kleene_l X phi) . phi) $ =
(named '(ibii (KT (positive_in_kleene_l_body @ positive_fresh X_fresh) @ norm (norm_sym @ norm_imp_l @ norm_trans ,(propag_s_subst 'Y $epsilon \/ (sVar Y . phi)$) @ norm_or_r @ norm_concat_r @ sSubstitution_fresh X_fresh) @
orim2 ,(framing_subst '(unfold_kleene_l_lemma X_fresh) 'appctx_concat_l)) @ unfold_kleene_l_lemma X_fresh));
theorem _sSubst_nnimp {X: SVar} (phi phi1 phi2 psi1 psi2: Pattern X)
(h1: $ Norm (s[ phi / X ] phi1) psi1 $)
(h2: $ Norm (s[ phi / X ] phi2) psi2 $):
$ Norm (s[ phi / X ] (phi1 ->> phi2)) (psi1 ->> psi2) $ =
'(_sSubst_imp (_sSubst_not @ _sSubst_not h1) h2);
theorem eq_to_nnimp_bi
(h1: $ (phi1 == phi2) -> (psi1 <-> psi2) $)
(h2: $ (phi1 == phi2) -> (rho1 <-> rho2) $):
$ (phi1 == phi2) -> ((psi1 ->> rho1) <-> (psi2 ->> rho2)) $ =
'(eq_to_imp_bi (eq_to_not_bi @ eq_to_not_bi h1) h2);
do {
(def (func_subst_eps x phi1) (func_subst_thm 'functional_epsilon x phi1))
(def (func_subst_concat x phi1) (func_subst_thm 'functional_concat x phi1))
};