Skip to content

Commit e5cd005

Browse files
MirceaSMirceaS
committed
fully proved induction principle
1 parent 6e073b7 commit e5cd005

File tree

5 files changed

+199
-45
lines changed

5 files changed

+199
-45
lines changed

‎02-ml-normalization.mm1‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,11 @@ theorem norm_and_r (phi psi psi2: Pattern)
9797
$ Norm (phi /\ psi) (phi /\ psi2) $ =
9898
'(norm_and norm_refl h);
9999

100+
theorem norm_forall {x: EVar} (phi psi: Pattern x)
101+
(h: $ Norm phi psi $):
102+
$ Norm (forall x phi) (forall x psi) $ =
103+
'(norm_not @ norm_exists @ norm_not h);
104+
100105
theorem eFresh_and {x: EVar} (phi1 phi2: Pattern x)
101106
(h1: $ _eFresh x phi1 $)
102107
(h2: $ _eFresh x phi2 $):
@@ -173,6 +178,11 @@ theorem exists_framing {x: EVar} (phi1 phi2: Pattern x)
173178
$ (exists x phi1) -> exists x phi2 $ =
174179
'(exists_generalization eFresh_exists_same_var @ syl exists_intro_same_var h);
175180

181+
theorem forall_framing {x: EVar} (phi1 phi2: Pattern x)
182+
(h: $ phi1 -> phi2 $):
183+
$ (forall x phi1) -> forall x phi2 $ =
184+
'(con3 @ exists_framing @ con3 h);
185+
176186
theorem or_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
177187
$ (phi1 \/ exists x phi2) <-> exists x (phi1 \/ phi2) $ =
178188
'(ibii

‎12-proof-system-p.mm1‎

Lines changed: 80 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,8 @@ theorem equiv_to_eq (h: $ phi <-> psi $): $ phi == psi $ = '(lemma_46_floor h);
258258
theorem eq_imp_subset: $ (phi == psi) -> (phi C= psi) $ = '(framing_floor anl);
259259
theorem subset_to_eq: $ (phi C= psi) -> (psi C= phi) -> (phi == psi) $ = '(exp @ anr propag_and_floor);
260260

261+
theorem subset_refl: $ phi C= phi $ = '(imp_to_subset id);
262+
261263
theorem eq_refl: $ phi == phi $ = '(equiv_to_eq biid);
262264
theorem functional_same_var: $ exists x (eVar x == eVar x) $ = '(exists_intro_same_var eq_refl);
263265
theorem functional_var: $ is_func (eVar x) $ =
@@ -273,6 +275,13 @@ theorem subset_imp_subset_or_r:
273275
$(phi C= psi) -> (phi C= (rho \/ psi))$ =
274276
'(framing_floor @ imim2i orr);
275277

278+
theorem subset_imp_or_subset_l:
279+
$(phi C= psi) -> ((psi \/ phi) C= psi)$ =
280+
'(framing_floor @ eor id);
281+
theorem subset_imp_or_subset_r:
282+
$(phi C= psi) -> ((phi \/ psi) C= psi)$ =
283+
'(framing_floor @ com12 eor id);
284+
276285
theorem subset_and: $ (phi C= (psi1 /\ psi2)) -> (phi C= psi1) /\ (phi C= psi2) $ =
277286
'(iand (framing_subset id anl) (framing_subset id anr));
278287

@@ -1123,10 +1132,80 @@ theorem ceil_idempotency_for_pred (phi: Pattern): $ ((phi == bot) \/ (phi == top
11231132
(mp ,(func_subst_imp_to_var 'x $eVar x == |^ eVar x ^| $) @ lemma_46_floor @ bicom @ taut_equiv_top @ framing_def imp_top definedness))
11241133
(mp ,(func_subst_imp_to_var 'x $(eVar x == bot) \/ (eVar x == top)$) ceil_is_pred)));
11251134

1135+
theorem framing_imp {box: SVar} (ctx: Pattern box) (phi psi: Pattern):
1136+
$ (phi C= psi) -> ((app[ phi / box ] ctx) C= (app[ psi / box ] ctx)) $ =
1137+
'(rsyl subset_imp_or_subset_r @
1138+
rsyl (com12 subset_to_eq @ subset_imp_subset_or_r subset_refl) @
1139+
rsyl (eq_to_subset_bi eq_to_id_bi (eq_to_appCtx_bi eq_to_intro_bi)) @
1140+
rsyl anl @
1141+
mpcom @
1142+
imp_to_subset @
1143+
framing orl);
1144+
1145+
do {
1146+
(def (framing_imp_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) framing_imp))
1147+
};
1148+
1149+
theorem under_domain_forall {x: EVar} (phi_a phi_b phi_c phi_d: Pattern x)
1150+
(h: $ phi_b -> phi_c $):
1151+
$ ((forall x (phi_a -> phi_c)) -> phi_d) -> (forall x (phi_a -> phi_b)) -> phi_d $ =
1152+
'(imim1 @ forall_framing @ imim2 h);
1153+
1154+
theorem domain_func_sorting {x: EVar} (phi psi: Pattern):
1155+
$ (exists x ((eVar x C= psi) /\ (eVar x == phi))) -> (phi C= psi) $ =
1156+
'(exists_generalization_disjoint @
1157+
rsyl (anim2 @ rsyl eq_sym eq_imp_subset) @
1158+
impcom subset_trans);
1159+
1160+
theorem forall_exists_lemma {box: SVar} {x: EVar} (ctx: Pattern box) (phi: Pattern):
1161+
$ ( forall x ((app[ (eVar x) / box ] ctx) C= phi)) ->
1162+
((exists x (app[ (eVar x) / box ] ctx)) C= phi ) $ =
1163+
'(con3 @
1164+
rsyl (framing_def @ con3 @ imim2 dne) @
1165+
rsyl (framing_def and_exists_disjoint_r_reverse) @
1166+
rsyl propag_exists_def @
1167+
exists_framing @
1168+
syl notnot1 @
1169+
framing_def @
1170+
con3 @
1171+
imim2 notnot1);
1172+
1173+
theorem forall_exists_lemma_domain {box: SVar} {x: EVar} (ctx: Pattern box) (phi psi: Pattern):
1174+
$ ( forall x (((eVar x) C= psi) -> ((app[ (eVar x) / box ] ctx) C= phi))) ->
1175+
((exists x (((eVar x) C= psi) /\ (app[ (eVar x) / box ] ctx))) C= phi ) $ =
1176+
'(con3 @
1177+
rsyl (framing_def @ con3 @ imim2 dne) @
1178+
rsyl (framing_def and_exists_disjoint_r_reverse) @
1179+
rsyl propag_exists_def @
1180+
exists_framing @
1181+
rsyl (framing_def @ anl anass) @
1182+
rsyl (iand (framing_def anl) (framing_def anr)) @
1183+
syl (con3 @ imim2 notnot1) @
1184+
anim (anl ceil_floor_floor) @
1185+
syl notnot1 @
1186+
framing_def @
1187+
con3 @
1188+
imim2 notnot1);
1189+
1190+
11261191
theorem pointwise_decomposition {box: SVar} {x: EVar} (ctx: Pattern box) (phi psi: Pattern)
11271192
(hyp: $ (x in phi) -> (app[ eVar x / box ] ctx C= psi) $):
11281193
$ app[ phi / box ] ctx C= psi $ =
11291194
'(imp_to_subset @ rsyl (anl appCtx_pointwise) @
11301195
exists_generalization_disjoint @
11311196
impcom @
1132-
rsyl hyp subset_to_imp);
1197+
rsyl hyp subset_to_imp);
1198+
1199+
theorem pointwise_decomposition_imp {box: SVar} {x: EVar} (ctx: Pattern box) (phi psi: Pattern):
1200+
$ (forall x (((eVar x) C= phi) -> (app[ eVar x / box ] ctx C= psi))) ->
1201+
(app[ phi / box ] ctx C= psi) $ =
1202+
'(rsyl forall_exists_lemma_domain @
1203+
anl (mp ,(func_subst_explicit_helper 'y $ (eVar y) C= _ $) (
1204+
equiv_to_eq @
1205+
bitr
1206+
(cong_of_equiv_exists @ bitr (aneq1i eVar_in_subset_rev) ancomb)
1207+
(bicom appCtx_pointwise))));
1208+
1209+
do {
1210+
(def (pointwise_decomposition_imp_subst subst) '(norm (norm_imp (norm_forall @ norm_imp_r @ norm_subset ,subst norm_refl) @ norm_subset ,subst norm_refl) pointwise_decomposition_imp))
1211+
};

‎nominal/core.mm1‎

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,9 @@ axiom pred_freshness:
4747
axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
4848
$ is_atom_sort alpha $ >
4949
$ is_nominal_sort tau $ >
50-
$ is_of_sort phi alpha ->
51-
is_of_sort psi tau ->
52-
s_forall alpha a (s_forall alpha b ((swap a b (abstraction phi psi)) == abstraction (swap a b phi) (swap a b psi))) $;
50+
$ (is_of_sort phi alpha) ->
51+
(is_of_sort psi tau) ->
52+
(s_forall alpha a (s_forall alpha b ((swap a b (abstraction phi psi)) == abstraction (swap a b phi) (swap a b psi)))) $;
5353

5454

5555
axiom EV_pred (alpha tau: Pattern):
@@ -59,62 +59,62 @@ axiom EV_pred (alpha tau: Pattern):
5959
axiom S1 (alpha tau: Pattern) {a: EVar} (phi: Pattern a):
6060
$ is_atom_sort alpha $ >
6161
$ is_nominal_sort tau $ >
62-
$ is_atom a alpha ->
63-
is_of_sort phi tau ->
64-
(moot_swap a phi) == phi $;
62+
$ (is_atom a alpha) ->
63+
(is_of_sort phi tau) ->
64+
((moot_swap a phi) == phi) $;
6565
axiom S2 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
6666
$ is_atom_sort alpha $ >
6767
$ is_nominal_sort tau $ >
68-
$ is_atom a alpha ->
69-
is_atom b alpha ->
70-
is_of_sort phi tau ->
68+
$ (is_atom a alpha) ->
69+
(is_atom b alpha) ->
70+
(is_of_sort phi tau) ->
7171
(swap a b (swap a b phi)) == phi $;
7272
axiom S3 (alpha: Pattern) {a b: EVar}:
7373
$ is_atom_sort alpha $ >
74-
$ is_atom a alpha ->
75-
is_atom b alpha ->
76-
(swap a b (eVar a)) == eVar b $;
74+
$ (is_atom a alpha) ->
75+
(is_atom b alpha) ->
76+
((swap a b (eVar a)) == eVar b) $;
7777
axiom S4 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
7878
$ is_atom_sort alpha $ >
7979
$ is_nominal_sort tau $ >
80-
$ is_atom a alpha ->
81-
is_atom b alpha ->
82-
is_of_sort phi tau ->
83-
(swap a b phi) == (swap b a phi) $;
80+
$ (is_atom a alpha) ->
81+
(is_atom b alpha) ->
82+
(is_of_sort phi tau) ->
83+
((swap a b phi) == (swap b a phi)) $;
8484
axiom F1 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
8585
$ is_atom_sort alpha $ >
8686
$ is_nominal_sort tau $ >
87-
$ is_atom a alpha ->
88-
is_atom b alpha ->
89-
is_of_sort phi tau ->
90-
(phi C= freshness a) /\ (phi C= freshness b) -> ((swap a b phi) == phi) $;
87+
$ (is_atom a alpha) ->
88+
(is_atom b alpha) ->
89+
(is_of_sort phi tau) ->
90+
((phi C= freshness a) /\ (phi C= freshness b) -> ((swap a b phi) == phi)) $;
9191
axiom F2 (alpha: Pattern) {a b: EVar}:
9292
$ is_atom_sort alpha $ >
93-
$ is_atom a alpha ->
94-
is_atom b alpha ->
95-
(b in freshness a) <-> (eVar a != eVar b) $;
93+
$ (is_atom a alpha) ->
94+
(is_atom b alpha) ->
95+
((b in freshness a) <-> (eVar a != eVar b)) $;
9696
axiom F3 (alpha1 alpha2: Pattern) {a b: EVar}:
9797
$ is_atom_sort alpha1 $ >
9898
$ is_atom_sort alpha2 $ >
99-
$ is_atom a alpha1 ->
100-
is_atom b alpha2 ->
101-
alpha1 != alpha2 ->
102-
b in freshness a $;
99+
$ (is_atom a alpha1) ->
100+
(is_atom b alpha2) ->
101+
(alpha1 != alpha2) ->
102+
(b in freshness a) $;
103103
axiom F4 (alpha tau phi: Pattern) {a: EVar}:
104104
$ is_atom_sort alpha $ >
105105
$ is_nominal_sort tau $ >
106-
$ is_of_sort phi tau ->
107-
s_exists alpha a (phi C= freshness a) $;
106+
$ (is_of_sort phi tau) ->
107+
(s_exists alpha a (phi C= freshness a)) $;
108108
axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
109109
$ is_atom_sort alpha $ >
110110
$ is_nominal_sort tau $ >
111-
$ is_atom a alpha ->
112-
is_atom b alpha ->
113-
is_of_sort phi tau ->
114-
is_of_sort rho tau ->
115-
((abstraction (eVar a) phi) == (abstraction (eVar b) rho)) <->
111+
$ (is_atom a alpha) ->
112+
(is_atom b alpha) ->
113+
(is_of_sort phi tau) ->
114+
(is_of_sort rho tau) ->
115+
(((abstraction (eVar a) phi) == (abstraction (eVar b) rho)) <->
116116
((eVar a == eVar b) /\ (phi == rho)) \/
117-
((rho C= freshness a) /\ ((swap a b phi) == rho)) $;
117+
((rho C= freshness a) /\ ((swap a b phi) == rho))) $;
118118
axiom A2 (alpha tau: Pattern) {x a y: EVar}:
119119
$ is_atom_sort alpha $ >
120120
$ is_nominal_sort tau $ >

‎nominal/lambda.mm1‎

Lines changed: 74 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ term lc_lam_sym: Symbol;
2222
def lc_lam (phi: Pattern): Pattern = $ (sym lc_lam_sym) @@ phi $;
2323
axiom function_lc_lam: $ ,(is_function '(sym lc_lam_sym) '[(sort_abstraction Var Exp)] 'Exp) $;
2424
axiom EV_lc_lam {a b: EVar} (phi: Pattern a b):
25-
$ is_of_sort phi (sort_abstraction Var Exp) $ >
26-
$ s_forall Var a (s_forall Var b ((swap a b (lc_lam phi)) == lc_lam (swap a b phi))) $;
25+
$ (is_of_sort phi (sort_abstraction Var Exp)) ->
26+
(s_forall Var a (s_forall Var b ((swap a b (lc_lam phi)) == lc_lam (swap a b phi)))) $;
2727

2828
axiom no_junk {X: SVar}:
2929
$ Exps == mu X ( (lc_var Vars)
@@ -32,6 +32,60 @@ axiom no_junk {X: SVar}:
3232

3333
--- no_confusion
3434

35+
theorem abstraction_sorting_lemma:
36+
$ is_of_sort (abstraction Vars Exps) (sort_abstraction Var Exp) $ =
37+
(named '(
38+
under_domain_forall
39+
,(pointwise_decomposition_imp_subst 'appCtxRVar)
40+
,(pointwise_decomposition_imp_subst 'appCtxLRVar) @
41+
under_domain_forall (
42+
under_domain_forall domain_func_sorting id
43+
) id @
44+
function_abstraction Var_atom Exp_sort));
45+
46+
theorem abstraction_sorting (phi rho: Pattern):
47+
$ is_of_sort phi Var -> is_of_sort rho Exp -> is_of_sort (abstraction phi rho) (sort_abstraction Var Exp) $ =
48+
(named '(
49+
rsyl ,(framing_imp_subst 'appCtxLRVar) @
50+
rsyl subset_trans @
51+
imim ,(framing_imp_subst 'appCtxRVar) @
52+
com12 subset_trans abstraction_sorting_lemma));
53+
54+
theorem EV_lc_lam_abstraction {a b: EVar} (phi: Pattern a b):
55+
$ is_of_sort phi Exp ->
56+
((is_of_sort (eVar a) Var) /\ (is_of_sort (eVar b) Var)) ->
57+
((swap a b (lc_lam (abstraction (eVar a) phi))) == lc_lam (abstraction (eVar b) (swap a b phi))) $ =
58+
(named '(exp @
59+
sylc eq_trans (
60+
rsyl (anr anass) @
61+
curry @
62+
rsyl (iand (impcom abstraction_sorting) anr) @
63+
curry @
64+
--- unquantification of EV_lc_lam
65+
rsyl EV_lc_lam @
66+
rsyl var_subst_same_var @
67+
imim2i var_subst_same_var
68+
) ( sylc eq_trans (
69+
syl ,(eq_imp_eq_framing_subst 'appCtxRVar) @
70+
rsyl (anr anass) @
71+
curry @
72+
rsyl (iand anr id) @
73+
rsyl (anr anass) @
74+
curry @
75+
curry @
76+
--- unquantification of EV_abstraction
77+
rsyl (EV_abstraction Var_atom Exp_sort) @
78+
imim2 @
79+
rsyl var_subst_same_var @
80+
imim2 var_subst_same_var
81+
) (
82+
rsyl anr @
83+
syl ,(eq_imp_eq_framing_subst 'appCtxRLRVar) @
84+
curry @
85+
S3 Var_atom
86+
))
87+
));
88+
3589

3690
theorem exp_pred_ev_unquantified {x y: EVar} (exp_pred: Pattern)
3791
(exp_pred_ev: $ EV_pattern Var exp_pred $):
@@ -52,12 +106,23 @@ theorem lc_lemma_1 {x: EVar} (exp_pred exp_suff_fresh: Pattern)
52106
@ anl lemma_ceil_exists_membership exp_suff_fresh_nonempty));
53107

54108
theorem lc_lemma_2 {x y: EVar} (exp_pred: Pattern)
55-
(ev_unquant: $ (is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var) -> ((swap x y exp_pred) == exp_pred) $):
109+
(exp_pred_sorting: $ is_of_sort exp_pred Exp $)
110+
(exp_pred_ev: $ EV_pattern Var exp_pred $):
56111
$ (((is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var)) /\ ((lc_lam (abstraction (eVar y) exp_pred)) C= exp_pred)) -> ((lc_lam (abstraction (eVar x) exp_pred)) C= exp_pred) $ =
57-
'(rsyl (anim2 ,(subset_imp_subset_framing_subst 'appCtxRVar)) @
58-
_);
112+
(named '(
113+
rsyl (anim2 ,(subset_imp_subset_framing_subst 'appCtxRVar)) @
114+
rsyl (iand anl @
115+
rsyl (anim1 @
116+
rsyl ancom @
117+
rsyl (EV_lc_lam_abstraction exp_pred_sorting) @
118+
syl eq_imp_subset eq_sym) @
119+
curry subset_trans) @
120+
rsyl (anim1 @ rsyl ancom @ exp_pred_ev_unquantified exp_pred_ev) @
121+
curry @
122+
syl anl ,(func_subst_explicit_helper 'hole $(_ @@ (_ @@ (eVar hole))) C= (eVar hole)$)));
59123

60124
theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
125+
(exp_pred_sorting: $ is_of_sort exp_pred Exp $)
61126
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
62127
(exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
63128
(exp_pred_ev: $ EV_pattern Var exp_pred $)
@@ -68,9 +133,10 @@ theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
68133
rsyl and_exists_disjoint_reverse @
69134
exists_generalization_disjoint @
70135
rsyl (anr anass) @
71-
lc_lemma_2 @ exp_pred_ev_unquantified exp_pred_ev));
136+
lc_lemma_2 exp_pred_sorting exp_pred_ev));
72137

73138
theorem freshness_irrelevance (exp_pred exp_suff_fresh: Pattern)
139+
(exp_pred_sorting: $ is_of_sort exp_pred Exp $)
74140
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
75141
(exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
76142
(exp_pred_ev: $ EV_pattern Var exp_pred $)
@@ -80,7 +146,7 @@ theorem freshness_irrelevance (exp_pred exp_suff_fresh: Pattern)
80146
pointwise_decomposition @
81147
norm (norm_sym @ norm_imp_r @ norm_subset appCtxRLRVar norm_refl) @
82148
rsyl (anl eVar_in_subset) @
83-
lc_lemma_3 exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs));
149+
lc_lemma_3 exp_pred_sorting exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs));
84150

85151
theorem prototype_induction_principle (exp_pred exp_suff_fresh: Pattern)
86152
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
@@ -98,5 +164,5 @@ theorem prototype_induction_principle (exp_pred exp_suff_fresh: Pattern)
98164
eori (eori
99165
(corollary_57_floor h_var)
100166
(corollary_57_floor h_app))
101-
@ corollary_57_floor @ freshness_irrelevance exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs
167+
@ corollary_57_floor @ freshness_irrelevance exp_pred_sorting exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs
102168
) exp_pred_sorting));

‎nominal/lemmas.mm1‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

0 commit comments

Comments
 (0)