Skip to content

Commit 1f0a304

Browse files
MirceaSMirceaS
committed
finished bulk of ev proof
1 parent baa8142 commit 1f0a304

File tree

5 files changed

+278
-49
lines changed

5 files changed

+278
-49
lines changed

‎01-propositional.mm1‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -434,6 +434,12 @@ theorem an5l: $ aa /\ bb /\ c /\ d /\ e /\ f -> aa $ = '(anwl an4l);
434434
theorem an5lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g -> bb $ = '(anwl an4lr);
435435
theorem an6l: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g -> aa $ = '(anwl an5l);
436436
theorem an6lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h -> bb $ = '(anwl an5lr);
437+
theorem an7l: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h -> aa $ = '(anwl an6l);
438+
theorem an7lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h /\ i -> bb $ = '(anwl an6lr);
439+
theorem an8l: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h /\ i -> aa $ = '(anwl an7l);
440+
theorem an8lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h /\ i /\ j -> bb $ = '(anwl an7lr);
441+
theorem an9l: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h /\ i /\ j -> aa $ = '(anwl an8l);
442+
theorem an9lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h /\ i /\ j /\ k -> bb $ = '(anwl an8lr);
437443
theorem curry (h: $ aa -> bb -> c $): $ aa /\ bb -> c $ = '(sylc h anl anr);
438444
theorem exp (h: $ aa /\ bb -> c $): $ aa -> bb -> c $ = '(syl6 h ian);
439445
theorem impcom (h: $ aa -> bb -> c $): $ bb /\ aa -> c $ = '(curry (com12 h));

‎11-definedness-normalization.mm1‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,5 +65,5 @@ theorem propag_bot {box: SVar} (ctx: Pattern box):
6565
'(syl (! singleton_same_var _ x _ _ (eVar x)) @ iand (framing absurdum) (framing absurdum));
6666

6767
theorem propag_or_def (phi1 phi2: Pattern):
68-
$ |^ phi1 \/ phi2 ^| -> |^ phi1 ^| \/ |^ phi2 ^| $ =
69-
'(norm (norm_imp defNorm (norm_or defNorm defNorm)) (! propag_or x));
68+
$ |^ phi1 \/ phi2 ^| <-> |^ phi1 ^| \/ |^ phi2 ^| $ =
69+
'(ibii (norm (norm_imp defNorm (norm_or defNorm defNorm)) (! propag_or x)) @ eori (framing_def orl) (framing_def orr));

‎12-proof-system-p.mm1‎

Lines changed: 136 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,10 @@ theorem eFresh_ceil {x: EVar} (phi: Pattern x)
1414
(h: $ _eFresh x phi $):
1515
$ _eFresh x (|^ phi ^|) $ =
1616
'(eFresh_app eFresh_disjoint h);
17+
theorem eFresh_floor {x: EVar} (phi: Pattern x)
18+
(h: $ _eFresh x phi $):
19+
$ _eFresh x (|_ phi _|) $ =
20+
'(eFresh_not @ eFresh_app eFresh_disjoint @ eFresh_not h);
1721
theorem eFresh_mem {x y: EVar} (phi: Pattern x y)
1822
(h: $ _eFresh x phi $):
1923
$ _eFresh x (y in phi) $ =
@@ -177,7 +181,7 @@ theorem exists_intro_l_bi_disjoint {x: EVar} (phi: Pattern x) (psi: Pattern)
177181
theorem propag_and_floor: $|_ phi /\ psi _| <-> |_ phi _| /\ |_ psi _|$ =
178182
'(ibii
179183
(iand (framing_floor anl) (framing_floor anr))
180-
(rsyl (anr notor) @ rsyl (con3 propag_or_def) @ con3 @ framing_def @ anl notan)
184+
(rsyl (anr notor) @ rsyl (con3 @ anl propag_or_def) @ con3 @ framing_def @ anl notan)
181185
);
182186

183187
theorem prop_43_or_def_rev (phi1 phi2: Pattern):
@@ -230,6 +234,9 @@ theorem cong_of_equiv_app (h1: $phi1 <-> phi2$) (h2: $psi1 <-> psi2$): $(app phi
230234
theorem cong_of_equiv_exists {x: EVar} (phi1 phi2: Pattern x)
231235
(h: $ phi1 <-> phi2 $): $ (exists x phi1) <-> (exists x phi2) $ =
232236
'(iani (exists_framing @ anl h) (exists_framing @ anr h));
237+
theorem cong_of_equiv_forall {x: EVar} (phi1 phi2: Pattern x)
238+
(h: $ phi1 <-> phi2 $): $ (forall x phi1) <-> (forall x phi2) $ =
239+
'(cong_of_equiv_not @ cong_of_equiv_exists @ cong_of_equiv_not h);
233240
theorem cong_of_equiv_sSubst_ctx {X: SVar} (phi phi1 phi2: Pattern X)
234241
(h: $ phi1 <-> phi2 $): $ (s[ phi / X ] phi1) <-> (s[ phi / X ] phi2) $ = '(ibii
235242
(sSubst_ctx_framing @ anl h)
@@ -279,6 +286,13 @@ theorem imp_forall {x: EVar} (phi1: Pattern) (phi2: Pattern x):
279286
$ (phi1 -> forall x phi2) <-> forall x (phi1 -> phi2) $ =
280287
'(imp_forall_fresh eFresh_disjoint);
281288

289+
theorem or_forall {x: EVar} (phi1: Pattern) (phi2: Pattern x):
290+
$ (phi1 \/ forall x phi2) <-> forall x (phi1 \/ phi2) $ = 'imp_forall;
291+
292+
theorem and_forall {x: EVar} (phi1: Pattern) (phi2: Pattern x):
293+
$ (phi1 /\ forall x phi2) <-> forall x (phi1 /\ phi2) $ =
294+
'(con3b @ bitr (cong_of_equiv_imp_r @ bicom notnot) @ bitr imp_exists_disjoint @ cong_of_equiv_exists notnot);
295+
282296

283297
theorem lemma_46 (phi: Pattern) {box: SVar} (ctx: Pattern box)
284298
(p : $ phi $):
@@ -356,7 +370,7 @@ theorem membership_var_forward {x y: EVar}: $ (x in (eVar y)) -> (eVar x == eVar
356370
@ norm (norm_imp defNorm norm_refl)
357371
(! framing box _ _ _ @ anr lemma_51));
358372
theorem membership_var_reverse {x y: EVar}: $ (eVar x == eVar y) -> (x in (eVar y)) $
359-
= '(propag_or_def @ framing_def or_imp_xor_and @ norm defNorm @ prop_43_or @ norm (norm_sym @ norm_or defNorm (! defNorm box)) @ orl definedness);
373+
= '(anl propag_or_def @ framing_def or_imp_xor_and @ norm defNorm @ prop_43_or @ norm (norm_sym @ norm_or defNorm (! defNorm box)) @ orl definedness);
360374
theorem membership_var_bi {x y: EVar}:
361375
$ (x in (eVar y)) <-> (eVar x == eVar y) $
362376
= '(iani membership_var_forward membership_var_reverse);
@@ -370,7 +384,7 @@ theorem membership_not_forward {x: EVar} (phi: Pattern x):
370384
$(x in ~phi) -> ~(x in phi) $ = '(con2 @ dne singletonDef);
371385
theorem membership_not_reverse {x: EVar} (phi: Pattern x):
372386
$~(x in phi) -> (x in ~phi) $ =
373-
'(propag_or_def @ framing_def (exp @ iand anl @ curry @ com12 dne) definedness);
387+
'(anl propag_or_def @ framing_def (exp @ iand anl @ curry @ com12 dne) definedness);
374388
theorem membership_not_bi {x: EVar} (phi: Pattern x):
375389
$ (x in ~phi) <-> ~(x in phi) $ =
376390
'(iani membership_not_forward membership_not_reverse);
@@ -482,7 +496,7 @@ theorem lemma_56 {box: SVar} (phi ctx: Pattern box)
482496
'(rsyl (rsyl (framing @ anl lemma_exists_and) @ propag_exists eFresh_disjoint)
483497
(exists_generalization eFresh_disjoint @ rsyl
484498
(dne @ singleton_norm norm_refl (! defNorm box2))
485-
(propag_or_def @ framing_def (anl com12b @ rsyl dne @ imim2i dne) (! definedness x))
499+
(anl propag_or_def @ framing_def (anl com12b @ rsyl dne @ imim2i dne) (! definedness x))
486500
));
487501

488502
theorem corollary_57_ceil (phi: Pattern): $ phi -> |^ phi ^| $ =
@@ -504,7 +518,7 @@ theorem lemma_60_forward {x: EVar} {box: SVar} (ctx phi1 phi2: Pattern box x):
504518
'(iand (framing anl) @
505519
rsyl (framing anr) @ rsyl (norm (
506520
norm_imp (norm_trans appCtxNested_disjoint @ norm_ctxApp_pt norm_refl (! defNorm box1)) @ norm_not (! defNorm box2)
507-
) @ dne singleton) @ propag_or_def @ framing_def lemma_60_helper_1 definedness);
521+
) @ dne singleton) @ anl propag_or_def @ framing_def lemma_60_helper_1 definedness);
508522

509523
theorem lemma_60_reverse {x: EVar} {box: SVar} (ctx phi2: Pattern box x) (phi1: Pattern x):
510524
$ ((app[ phi1 / box ] ctx) /\ (x in phi2)) -> app[ phi1 /\ (x in phi2) / box ] ctx $ =
@@ -878,11 +892,11 @@ theorem lemma_in_in_forward_same_var {x: EVar} (phi: Pattern x):
878892
'(syl ceil_mem_imp_mem @ framing_def anr);
879893
theorem lemma_in_in_reverse {x y: EVar} (phi: Pattern x y):
880894
$ (y in phi) -> x in (y in phi) $ =
881-
'(rsyl mem_imp_floor_mem @ propag_or_def @
895+
'(rsyl mem_imp_floor_mem @ anl propag_or_def @
882896
framing_def lemma_in_in_reverse_helper @ prop_43_or_def @ orr definedness);
883897
theorem lemma_in_in_reverse_same_var {x: EVar} (phi: Pattern x):
884898
$ (x in phi) -> x in (x in phi) $ =
885-
'(rsyl mem_imp_floor_mem @ propag_or_def @
899+
'(rsyl mem_imp_floor_mem @ anl propag_or_def @
886900
framing_def lemma_in_in_reverse_helper @ prop_43_or_def @ orr definedness);
887901

888902
theorem lemma_in_in {x y: EVar} (phi: Pattern x y):
@@ -937,7 +951,7 @@ theorem membership_forall {x y: EVar} (phi: Pattern x y):
937951

938952

939953
theorem floor_imp_mem {x: EVar} (phi: Pattern x): $ |_ phi _| -> x in phi $ =
940-
'(propag_or_def @ framing_def (imim1i dne) @ framing_def ian definedness);
954+
'(anl propag_or_def @ framing_def (imim1i dne) @ framing_def ian definedness);
941955

942956
theorem mem_floor_forward {x: EVar} (phi: Pattern x):
943957
$ (x in |_ phi _|) -> |_ phi _| $ =
@@ -993,6 +1007,23 @@ do {
9931007
(def (appCtx_floor_commute_b_subst subst) '(norm (norm_imp ,subst @ norm_and_r ,subst) appCtx_floor_commute_b))
9941008
};
9951009

1010+
1011+
theorem floor_appCtx_dual (phi: Pattern) {box: SVar} (ctx: Pattern box):
1012+
$ |_ phi _| -> ~ (app[ (~ (|_ phi _|)) / box ] ctx) $ =
1013+
'(exp @ rsyl (anim2 @ syl ceil_appCtx @ framing dne) @ notnot1 id);
1014+
1015+
theorem ceil_appCtx_dual (phi: Pattern) {box: SVar} (ctx: Pattern box):
1016+
$ |^ phi ^| -> ~ (app[ (~ (|^ phi ^|)) / box ] ctx) $ =
1017+
'(rsyl (anr floor_ceil_ceil) @ rsyl floor_appCtx_dual @ con3 @ framing @ con3 @ anl floor_ceil_ceil);
1018+
1019+
theorem ceil_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
1020+
$ (app[ |_ phi _| -> psi / box ] ctx) -> |_ phi _| -> app[ psi / box ] ctx $ =
1021+
'(exp @ rsyl (anim propag_or floor_appCtx_dual) @ rsyl (anl andir) @ eori (syl absurdum @ rsyl (anim1 @ framing notnot1) @ notnot1 notnot1) anl);
1022+
1023+
do {
1024+
(def (ceil_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) ceil_imp_in_appCtx))
1025+
};
1026+
9961027
theorem alpha_exists {x y: EVar} (phi: Pattern x y)
9971028
(y_fresh: $ _eFresh y phi $):
9981029
$ (exists x phi) <-> exists y (e[ eVar y / x ] phi) $ =
@@ -1050,6 +1081,7 @@ do {
10501081
[_ 'biid]
10511082
)
10521083

1084+
-- x = phi -> C[x] <-> C[phi]
10531085
(def (func_subst_explicit_helper x ctx) @ match ctx
10541086
[$eVar ,y$ (if (== x y) 'eq_to_intro_bi 'eq_to_id_bi)]
10551087
[$exists ,y ,psi$ (if (== x y) 'eq_to_id_bi '(eq_to_exists_bi ,(func_subst_explicit_helper x psi)))]
@@ -1066,6 +1098,8 @@ do {
10661098
[$equiv ,phi1 ,phi2$ '(eq_to_equiv_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
10671099
[$_eq ,phi1 ,phi2$ '(eq_to_eq_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
10681100
[$is_func ,psi$ '(eq_to_func_bi ,(func_subst_explicit_helper x psi))]
1101+
[$bot$ 'eq_to_id_bi]
1102+
[$top$ 'eq_to_id_bi]
10691103

10701104
[$nnimp ,phi1 ,phi2$ '(eq_to_nnimp_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper X phi2))]
10711105
[$concat ,phi1 ,phi2$ '(eq_to_concat_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
@@ -1074,18 +1108,41 @@ do {
10741108
[_ 'eq_to_id_bi]
10751109
)
10761110

1111+
-- C[phi] -> x = phi -> C[x]
10771112
(def (func_subst_imp_to_var x ctx) '(com12 @ syl anr ,(func_subst_explicit_helper x ctx)))
10781113

1114+
-- forall x . phi1[x]
1115+
-- exists y . y = phi2
1116+
----------------------
1117+
-- phi1[phi2]
10791118
(def (func_subst_explicit x y phi1 forall_x_phi1 func_phi2) '(
10801119
exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) (norm ,(propag_e_subst x phi1) (! var_subst ,x ,y ,phi1 ,forall_x_phi1))) ,func_phi2
10811120
))
10821121

1122+
-- (exists y . y = phi2) -> (forall x . phi1[x]) -> phi1[phi2]
1123+
(def (func_subst_explicit_thm x phi1) '(
1124+
exists_generalization_disjoint (com12 (syl (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) (norm (norm_imp_r ,(propag_e_subst x phi1)) (! var_subst ,x))))
1125+
))
1126+
1127+
-- (s_exists y:S . y = phi2) -> (s_forall x:S . phi1[x]) -> phi1[phi2]
1128+
(def (func_subst_explicit_thm_sorted x phi1) '(
1129+
rsyl (iand domain_func_sorting @ exists_framing anr) @ rsyl (anim2 @ rsyl ,(func_subst_explicit_thm x phi1) @ anl com12b) appl
1130+
))
1131+
1132+
-- C[x]
1133+
-- exists x . x = phi2
1134+
----------------------
1135+
-- C[phi]
10831136
(def (func_subst x phi1 phi1_pf func_phi2) '(
10841137
exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) ,phi1_pf) ,func_phi2
10851138
))
1139+
1140+
-- C[phi2] -> exists x . C[x]
10861141
(def (func_subst_alt x phi1 func_phi2) '(
10871142
anr imp_exists_disjoint (mp (exists_framing @ syl anr ,(func_subst_explicit_helper x phi1)) ,func_phi2)
10881143
))
1144+
1145+
-- (s_exists x . x = phi) -> C[phi] -> s_exists x . C[x]
10891146
(def (func_subst_alt_thm_sorted x phi1) '(
10901147
syl (rsyl (exists_framing imancom) (anr imp_exists_disjoint)) @ exists_framing @ anim2 @ syl anr ,(func_subst_explicit_helper x phi1)
10911148
))
@@ -1302,6 +1359,8 @@ theorem subset_mem_lemma {x: EVar} (phi psi: Pattern):
13021359
do {
13031360
(def (forall_imp_climb n) (iterate n (fn (pf) '(syl (anl imp_forall) @ imim2 ,pf)) 'id))
13041361

1362+
(def (forall_imp_push n) (iterate n (fn (pf) '(rsyl (anr imp_forall) @ imim2 ,pf)) 'id))
1363+
13051364
(def (inst_foralls n) (if {n = 0} 'id
13061365
'(rsyl (rsyl ,(inst_foralls {n - 1}) ,(forall_imp_climb {n - 1})) var_subst_same_var)
13071366
))
@@ -1325,3 +1384,72 @@ theorem swap_sorted_forall {x y: EVar} (phi: Pattern x y) (phi_x: Pattern x) (ph
13251384
forall_framing @
13261385
rsyl (forall_framing @ anl com12b) @
13271386
anr imp_forall);
1387+
1388+
theorem ceil_imp_lemma:
1389+
$ (|^ phi ^| -> |_ psi _|) -> |_ |^ phi ^| -> psi _| $ =
1390+
'(rsyl (imim (anl floor_ceil_ceil) (anr ceil_floor_floor)) @ rsyl prop_43_or_def @ rsyl (anr floor_ceil_ceil) @ framing_floor @ rsyl prop_43_or_def_rev @ imim (anr floor_ceil_ceil) (rsyl (anl ceil_floor_floor) corollary_57_floor));
1391+
1392+
theorem floor_imp_lemma:
1393+
$ (|_ phi _| -> |_ psi _|) -> |_ |_ phi _| -> psi _| $ =
1394+
'(rsyl (imim1 @ anl ceil_floor_floor) @ rsyl ceil_imp_lemma @ framing_floor @ imim1 @ anr ceil_floor_floor);
1395+
1396+
theorem ceil_of_ceil_conj:
1397+
$ |^ phi ^| /\ |^ rho ^| <-> |^ |^ phi ^| /\ |^ rho ^| ^| $ =
1398+
'(bitr (cong_of_equiv_and (bicom floor_ceil_ceil) (bicom floor_ceil_ceil)) @ bitr (bicom propag_and_floor) @ bitr (bicom ceil_floor_floor) @ cong_of_equiv_def @ bitr propag_and_floor @ cong_of_equiv_and floor_ceil_ceil floor_ceil_ceil);
1399+
1400+
1401+
theorem floor_of_floor_and:
1402+
$ |_ phi _| /\ |_ rho _| <-> |_ |_ phi _| /\ |_ rho _| _| $ =
1403+
'(bitr (cong_of_equiv_and (bicom floor_idem) (bicom floor_idem)) @ bicom propag_and_floor);
1404+
1405+
theorem floor_of_floor_not:
1406+
$ ~ |_ phi _| <-> |_ ~ |_ phi _| _| $ =
1407+
'(bitr (bicom notnot) @ bitr (bicom floor_ceil_ceil) @ cong_of_equiv_floor notnot);
1408+
1409+
theorem floor_of_floor_or:
1410+
$ |_ phi _| \/ |_ rho _| <-> |_ |_ phi _| \/ |_ rho _| _| $ =
1411+
'(bitr (cong_of_equiv_or (bicom ceil_floor_floor) (bicom ceil_floor_floor)) @ bitr (bicom propag_or_def) @ bitr (bicom floor_ceil_ceil) @ cong_of_equiv_floor @ bitr propag_or_def @ cong_of_equiv_or ceil_floor_floor ceil_floor_floor);
1412+
1413+
theorem floor_of_floor_imp:
1414+
$ (|_ phi _| -> |_ psi _|) <-> |_ |_ phi _| -> |_ psi _| _| $ =
1415+
'(ibii (rsyl (imim2 @ anr floor_idem) floor_imp_lemma) corollary_57_floor);
1416+
1417+
theorem floor_of_floor_forall {x: EVar} (phi: Pattern x):
1418+
$ (forall x (|_ phi _|)) <-> |_ forall x (|_ phi _|) _| $ =
1419+
'(ibii (con3 @ rsyl (framing_def dne) @ rsyl propag_exists_def @ exists_framing @ rsyl (framing_def dne) @ rsyl (anl def_idem) notnot1) corollary_57_floor);
1420+
1421+
theorem floor_of_floor_exists {x: EVar} (phi: Pattern x):
1422+
$ (exists x (|_ phi _|)) <-> |_ exists x (|_ phi _|) _| $ =
1423+
'(ibii (exists_generalization (eFresh_floor eFresh_exists_same_var) @ rsyl (anr floor_idem) @ framing_floor exists_intro_same_var) corollary_57_floor);
1424+
1425+
theorem floor_of_floor_s_exists {x: EVar} (phi: Pattern x):
1426+
$ (exists x (((eVar x) C= sort) /\ |_ phi _|)) <-> |_ exists x (|_ ((eVar x) C= sort) /\ |_ phi _| _|) _| $ =
1427+
'(bitr (cong_of_equiv_exists floor_of_floor_and) floor_of_floor_exists);
1428+
1429+
theorem floor_of_floor_s_forall {x: EVar} (phi: Pattern x):
1430+
$ (forall x (((eVar x) C= sort) -> |_ phi _|)) <-> |_ forall x (|_ ((eVar x) C= sort) -> |_ phi _| _|) _| $ =
1431+
'(bitr (cong_of_equiv_forall floor_of_floor_imp) floor_of_floor_forall);
1432+
1433+
1434+
1435+
do {
1436+
(def (floor_wrap_equiv pred) @ match pred
1437+
[$exists ,x ,phi$ '(bitr (cong_of_equiv_exists ,(floor_wrap_equiv phi)) floor_of_floor_exists)]
1438+
[$forall ,x ,phi$ '(bitr (cong_of_equiv_forall ,(floor_wrap_equiv phi)) floor_of_floor_forall)]
1439+
[$imp ,phi1 ,phi2$ '(bitr (cong_of_equiv_imp ,(floor_wrap_equiv phi1) ,(floor_wrap_equiv phi2)) floor_of_floor_imp)]
1440+
[$not ,phi$ '(bitr (cong_of_equiv_not ,(floor_wrap_equiv phi)) floor_of_floor_not)]
1441+
[$or ,phi1 ,phi2$ '(bitr (cong_of_equiv_or ,(floor_wrap_equiv phi1) ,(floor_wrap_equiv phi2)) floor_of_floor_or)]
1442+
[$and ,phi1 ,phi2$ '(bitr (cong_of_equiv_and ,(floor_wrap_equiv phi1) ,(floor_wrap_equiv phi2)) floor_of_floor_and)]
1443+
[$_ceil ,phi$ '(bicom floor_ceil_ceil)]
1444+
[$_in ,x ,phi$ '(bicom floor_ceil_ceil)]
1445+
[$_floor ,phi$ '(bicom floor_idem)]
1446+
[$_subset ,phi1 ,phi2$ '(bicom floor_idem)]
1447+
[$_eq ,phi1 ,phi2$ '(bicom floor_idem)]
1448+
[$is_func ,phi$ '(floor_of_floor_exists)]
1449+
1450+
[$s_exists ,s ,x ,phi$ '(bitr (cong_of_equiv_exists @ cong_of_equiv_and_r ,(floor_wrap_equiv phi)) floor_of_floor_s_exists)]
1451+
[$s_forall ,s ,x ,phi$ '(bitr (cong_of_equiv_forall @ cong_of_equiv_imp_r ,(floor_wrap_equiv phi)) floor_of_floor_s_forall)]
1452+
)
1453+
1454+
(def (extract_pred_from_appCtx_r pred subst) '(norm (norm_imp ,subst @ norm_and_l ,subst) @ rsyl (anl @ cong_of_equiv_appCtx @ cong_of_equiv_and_r ,(floor_wrap_equiv pred)) @ rsyl appCtx_floor_commute @ anr @ cong_of_equiv_and_r ,(floor_wrap_equiv pred)))
1455+
};

‎nominal/core.mm1‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,9 @@ axiom function_swap:
3535
$ is_atom_sort alpha $ >
3636
$ is_nominal_sort tau $ >
3737
$ ,(is_function '(sym swap_sym) '[alpha alpha tau] 'tau) $;
38+
axiom function_swap_atom:
39+
$ is_atom_sort alpha $ >
40+
$ ,(is_function '(sym swap_sym) '[alpha alpha alpha] 'alpha) $;
3841
axiom function_abstraction:
3942
$ is_atom_sort alpha $ >
4043
$ is_nominal_sort tau $ >
@@ -64,13 +67,13 @@ axiom S1 (alpha tau a phi: Pattern):
6467
$ (is_atom a alpha) ->
6568
(is_of_sort phi tau) ->
6669
((swap a a phi) == phi) $;
67-
axiom S2 (alpha tau a b phi: Pattern):
70+
axiom S2 {a b: EVar} (alpha tau phi: Pattern a b):
6871
$ is_atom_sort alpha $ >
6972
$ is_nominal_sort tau $ >
70-
$ (is_atom a alpha) ->
71-
(is_atom b alpha) ->
73+
$ s_forall alpha a (
74+
s_forall alpha b (
7275
(is_of_sort phi tau) ->
73-
(swap a b (swap a b phi)) == phi $;
76+
((swap (eVar a) (eVar b) (swap (eVar a) (eVar b) phi)) == phi))) $;
7477
axiom S3 {a b: EVar} (alpha: Pattern a b):
7578
$ is_atom_sort alpha $ >
7679
$ s_forall alpha a (

0 commit comments

Comments
 (0)