Skip to content

Commit e3a167d

Browse files
committed
finished proof
1 parent 5ebf6d3 commit e3a167d

File tree

7 files changed

+459
-166
lines changed

7 files changed

+459
-166
lines changed

01-propositional.mm1

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -773,3 +773,12 @@ theorem iand4 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -
773773

774774
theorem iand5 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $) (h5: $ aa -> f $): $ aa -> bb /\ c /\ d /\ e /\ f $ =
775775
'(iand (iand (iand (iand h1 h2) h3) h4) h5);
776+
777+
theorem iand6 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $) (h5: $ aa -> f $) (h6: $ aa -> g $): $ aa -> bb /\ c /\ d /\ e /\ f /\ g $ =
778+
'(iand (iand (iand (iand (iand h1 h2) h3) h4) h5) h6);
779+
780+
theorem iand7 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $) (h5: $ aa -> f $) (h6: $ aa -> g $) (h7: $ aa -> h $): $ aa -> bb /\ c /\ d /\ e /\ f /\ g /\ h $ =
781+
'(iand (iand (iand (iand (iand (iand h1 h2) h3) h4) h5) h6) h7);
782+
783+
theorem imp_or_extract: $ (aa -> bb) \/ (aa -> c) <-> (aa -> (bb \/ c)) $ =
784+
'(ibii (eori (imim2 orl) (imim2 orr)) imp_or_split);

10-theory-definedness.mm0

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,21 @@ def is_func {.x: EVar} (phi: Pattern): Pattern = $ exists x (eVar x == phi) $;
2929

3030
def is_pred (phi: Pattern): Pattern = $ (phi == bot) \/ (phi == top) $;
3131

32+
--- Domain Quantifiers
33+
----------------------
34+
35+
def exists_in {x: EVar} (phi psi: Pattern x): Pattern = $ exists x ((eVar x C= phi) /\ psi) $;
36+
notation exists_in {x: EVar} (phi psi: Pattern x): Pattern = ($E$:0) x ($:$:0) phi ($.$:0) psi;
37+
38+
def forall_in {x: EVar} (phi psi: Pattern x): Pattern = $ forall x ((eVar x C= phi) -> psi) $;
39+
notation forall_in {x: EVar} (phi psi: Pattern x): Pattern = ($A$:0) x ($:$:0) phi ($.$:0) psi;
40+
41+
42+
def is_sorted_pred (phi psi: Pattern): Pattern = $ (psi == bot) \/ (psi == phi) $;
43+
44+
def is_sorted_func {.x: EVar} (phi psi: Pattern): Pattern = $ E x : phi . eVar x == psi $;
45+
46+
3247
--- Contextual Implications
3348
---------------------------
3449

12-proof-system-p.mm1

Lines changed: 65 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,10 @@ theorem subset_imp_or_subset_r:
365365
theorem subset_and: $ (phi C= (psi1 /\ psi2)) -> (phi C= psi1) /\ (phi C= psi2) $ =
366366
'(iand (framing_subset id anl) (framing_subset id anr));
367367

368+
theorem and_subset: $ (phi1 C= psi) /\ (phi2 C= psi) <-> (phi1 \/ phi2 C= psi) $ =
369+
'(ibii (rsyl (anr propag_and_floor) @ framing_floor @ curry eor) @
370+
iand (framing_floor @ imim1 orl) (framing_floor @ imim1 orr));
371+
368372
theorem taut_equiv_top (h: $ phi $): $ phi <-> top $ =
369373
'(ibii imp_top @ a1i h);
370374
theorem taut_and_equiv (h: $ phi $): $ phi /\ psi <-> psi $ =
@@ -1052,12 +1056,12 @@ theorem ceil_appCtx_dual (phi: Pattern) {box: SVar} (ctx: Pattern box):
10521056
$ |^ phi ^| -> ~ (app[ (~ (|^ phi ^|)) / box ] ctx) $ =
10531057
'(rsyl (anr floor_ceil_ceil) @ rsyl floor_appCtx_dual @ con3 @ framing @ con3 @ anl floor_ceil_ceil);
10541058

1055-
theorem ceil_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
1059+
theorem floor_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
10561060
$ (app[ |_ phi _| -> psi / box ] ctx) -> |_ phi _| -> app[ psi / box ] ctx $ =
10571061
'(exp @ rsyl (anim propag_or floor_appCtx_dual) @ rsyl (anl andir) @ eori (syl absurdum @ rsyl (anim1 @ framing notnot1) @ notnot1 notnot1) anl);
10581062

10591063
do {
1060-
(def (ceil_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) ceil_imp_in_appCtx))
1064+
(def (floor_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) floor_imp_in_appCtx))
10611065
};
10621066

10631067
theorem alpha_exists {x y: EVar} (phi: Pattern x y)
@@ -1291,6 +1295,21 @@ theorem ceil_is_pred: $ (|^ phi ^| == bot) \/ (|^ phi ^| == top) $ =
12911295
@ rsyl anr @ mpcom taut)
12921296
emr);
12931297

1298+
theorem floor_is_pred: $ (|_ phi _| == bot) \/ (|_ phi _| == top) $ =
1299+
'(orim
1300+
(anl
1301+
@ bitr (bicom @ cong_of_equiv_not @ ceil_floor_floor)
1302+
@ bitr not_ceil_floor_bi
1303+
@ cong_of_equiv_floor
1304+
@ ibii (iand id @ a1i absurdum)
1305+
anl)
1306+
(anl
1307+
@ bitr (bicom floor_idem)
1308+
@ cong_of_equiv_floor
1309+
@ ibii (iand (a1i imp_top) @ com12 @ a1i id)
1310+
@ rsyl anr @ mpcom taut)
1311+
emr);
1312+
12941313
theorem ceil_idempotency_for_pred (phi: Pattern): $ ((phi == bot) \/ (phi == top)) <-> (phi == |^ phi ^|) $ =
12951314
(named '(ibii
12961315
(eori
@@ -1543,3 +1562,47 @@ do {
15431562
[_ 'biid]
15441563
)
15451564
};
1565+
1566+
theorem is_pred_floor: $ (is_pred phi) <-> (phi == |_ phi _|) $ =
1567+
'(ibii
1568+
(rsyl (anl floor_of_floor_or) @ framing_floor @ eori (rsyl (rsyl corollary_57_floor anl) @ iand (imim2 absurdum) @ a1i corollary_57_floor) @ iand (rsyl ,(func_subst_explicit_helper 'x $ (eVar x) -> |_ eVar x _| $) @ rsyl anr @ mpcom @ a1i @ lemma_46_floor taut) @ a1i corollary_57_floor)
1569+
(rsyl ,(func_subst_explicit_helper 'x $((eVar x) == bot) \/ ((eVar x) == top)$) @ rsyl anr @ mpcom floor_is_pred));
1570+
1571+
theorem KT_imp {X: SVar} (ctx ante phi: Pattern X)
1572+
(pos: $ _Positive X ctx $)
1573+
(propag: $ (s[ ante -> phi / X ] ctx) -> ante -> s[ phi / X ] ctx $)
1574+
(h: $ ante -> (s[ phi / X ] ctx) -> phi $):
1575+
$ ante -> (mu X ctx) -> phi $ =
1576+
'(com12 @ KT pos @ rsyl propag (prop_2 h));
1577+
1578+
theorem KT_subset {X: SVar} (ctx phi: Pattern X)
1579+
(pos: $ _Positive X ctx $)
1580+
(propag: $ (s[ ((s[ phi / X ] ctx) C= phi) -> phi / X ] ctx) -> ((s[ phi / X ] ctx) C= phi) -> s[ phi / X ] ctx $):
1581+
$ ((s[ phi / X ] ctx) C= phi) -> ((mu X ctx) C= phi) $ =
1582+
'(rsyl (anr floor_idem) @ framing_floor @ KT_imp pos propag corollary_57_floor);
1583+
1584+
do {
1585+
(def (KT_subset_subst subst pos propag) '(norm (norm_imp_l @ norm_subset ,subst norm_refl) @ KT_subset ,pos @ norm (norm_sym @ norm_imp (norm_trans (norm_svSubst_pt norm_refl @ norm_imp_l @ norm_subset ,subst norm_refl) ,subst) @ norm_imp (norm_subset ,subst norm_refl) ,subst) ,propag))
1586+
};
1587+
1588+
1589+
theorem floor_extract_app
1590+
(h1: $ phi1 -> |_ psi _| -> rho1 $)
1591+
(h2: $ phi2 -> |_ psi _| -> rho2 $):
1592+
$ (app phi1 phi2) -> |_ psi _| -> app rho1 rho2 $ =
1593+
(named '(rsyl ,(framing_subst 'h1 'appCtxLVar) @ rsyl ,(floor_imp_in_appCtx_subst 'appCtxLVar) @ rsyl (imim2 (rsyl ,(framing_subst 'h2 'appCtxRVar) ,(floor_imp_in_appCtx_subst 'appCtxRVar))) imidm));
1594+
1595+
theorem floor_extract_or
1596+
(h1: $ phi1 -> |_ psi _| -> rho1 $)
1597+
(h2: $ phi2 -> |_ psi _| -> rho2 $):
1598+
$ phi1 \/ phi2 -> |_ psi _| -> rho1 \/ rho2 $ =
1599+
'(rsyl (orim h1 h2) @ anl imp_or_extract);
1600+
1601+
do {
1602+
(def (floor_extract x ctx) @ match ctx
1603+
[$eVar ,y$ (if (== x y) 'id 'prop_1)]
1604+
[$app ,phi1 ,phi2$ '(floor_extract_app ,(floor_extract x phi1) ,(floor_extract x phi2))]
1605+
[$or ,phi1 ,phi2$ '(floor_extract_or ,(floor_extract x phi1) ,(floor_extract x phi2))]
1606+
[_ 'prop_1]
1607+
)
1608+
};

nominal/core.mm1

Lines changed: 41 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ axiom function_sort_abstraction: $ ,(is_function '(sym sort_abstraction_sym) '[a
1818

1919
def is_atom_sort (alpha: Pattern): Pattern = $ (is_func alpha) /\ (alpha C= dom atoms) $;
2020
def is_nominal_sort (tau: Pattern): Pattern = $ (is_func tau) /\ (tau C= dom nominal_sorts) $;
21-
def is_atom (a alpha: Pattern): Pattern = $ is_sorted_func alpha a $;
21+
def is_atom (a alpha: Pattern): Pattern = $ is_sorted_func (dom alpha) a $;
2222

2323
axiom nominal_sorts_are_sorts: $ (is_nominal_sort phi) -> (is_sort phi) $;
2424

@@ -29,6 +29,13 @@ def abstraction (phi rho: Pattern): Pattern = $ (sym abstraction_sym) @@ phi @@
2929
term supp_sym: Symbol;
3030
def supp (phi: Pattern): Pattern = $ (sym supp_sym) @@ phi $;
3131
def fresh_for (phi psi: Pattern): Pattern = $ ~ (phi C= supp psi) $;
32+
term comma_sym: Symbol;
33+
def comma (phi psi: Pattern): Pattern = $ (sym comma_sym) @@ phi @@ psi $;
34+
infixl comma: $,,$ prec 35;
35+
term comma_sort_sym: Symbol;
36+
def comma_sort: Pattern = $ sym comma_sort_sym $;
37+
38+
axiom comma_sort_nominal: $ is_nominal_sort comma_sort $;
3239

3340
def EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
3441
$ s_forall alpha a (s_forall alpha b ((swap (eVar a) (eVar b) phi) == phi)) $;
@@ -48,6 +55,10 @@ axiom multifunction_supp:
4855
$ is_atom_sort alpha $ >
4956
$ is_nominal_sort tau $ >
5057
$ ,(is_multi_function '(sym supp_sym) '[tau] 'alpha) $;
58+
axiom function_comma:
59+
$ is_nominal_sort tau1 $ >
60+
$ is_nominal_sort tau2 $ >
61+
$ ,(is_function '(sym comma_sym) '[tau1 tau2] 'comma_sort) $;
5162

5263
axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
5364
$ is_atom_sort alpha $ >
@@ -56,14 +67,40 @@ axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
5667
(is_of_sort phi alpha) ->
5768
(is_of_sort psi tau) ->
5869
((swap (eVar a) (eVar b) (abstraction phi psi)) == abstraction (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
59-
-- add EV axiom for swap
60-
axiom EV_supp {a b: EVar} (tau: Pattern) (phi: Pattern a b):
70+
71+
axiom EV_swap {a b c d: EVar} (alpha tau: Pattern) (phi: Pattern a b c d):
72+
$ is_atom_sort alpha $ >
73+
$ is_nominal_sort tau $ >
74+
$ s_forall alpha a (s_forall alpha b (s_forall alpha c (s_forall alpha d (
75+
(is_of_sort phi alpha) ->
76+
(is_of_sort psi tau) ->
77+
((swap (eVar a) (eVar b) (swap (eVar c) (eVar d) phi)) == swap (swap (eVar a) (eVar b) (eVar c)) (swap (eVar a) (eVar b) (eVar d)) (swap (eVar a) (eVar b) phi)))))) $;
78+
79+
axiom EV_supp {a b: EVar} (alpha tau: Pattern) (phi: Pattern a b):
6180
$ is_atom_sort alpha $ >
6281
$ is_nominal_sort tau $ >
6382
$ s_forall alpha a (s_forall alpha b (
6483
(is_of_sort phi tau) ->
6584
((swap (eVar a) (eVar b) (supp phi)) == supp (swap (eVar a) (eVar b) phi)))) $;
6685

86+
axiom EV_comma {a b: EVar} (alpha tau: Pattern) (phi1 phi2: Pattern a b):
87+
$ is_atom_sort alpha $ >
88+
$ is_nominal_sort tau $ >
89+
$ s_forall alpha a (s_forall alpha b (
90+
(is_of_sort phi1 tau) ->
91+
(is_of_sort phi2 tau) ->
92+
((swap (eVar a) (eVar b) (phi1 ,, phi2)) == ((swap (eVar a) (eVar b) phi1) ,, (swap (eVar a) (eVar b) phi2))))) $;
93+
94+
axiom fresh_comma {a: EVar} (alpha tau1 tau2: Pattern) (phi1 phi2: Pattern a):
95+
$ is_atom_sort alpha $ >
96+
$ is_nominal_sort tau1 $ >
97+
$ is_nominal_sort tau2 $ >
98+
$ s_forall alpha a (
99+
(is_of_sort phi1 tau1) ->
100+
(is_of_sort phi2 tau2) ->
101+
(fresh_for (eVar a) (phi1 ,, phi2)) ->
102+
(fresh_for (eVar a) phi1) /\ (fresh_for (eVar a) phi2)) $;
103+
67104
axiom EV_pred (alpha tau: Pattern):
68105
$ is_atom_sort alpha $ >
69106
$ is_nominal_sort tau $ >
@@ -110,7 +147,7 @@ axiom F3 {a b: EVar} (alpha1 alpha2: Pattern a b):
110147
axiom F4 {a: EVar} (alpha tau phi: Pattern):
111148
$ is_atom_sort alpha $ >
112149
$ is_nominal_sort tau $ >
113-
$ (is_sorted_func tau phi) ->
150+
$ (is_sorted_func (dom tau) phi) ->
114151
(s_exists alpha a (fresh_for (eVar a) phi)) $;
115152
axiom A1 {a b: EVar} (alpha tau phi rho: Pattern a b):
116153
$ is_atom_sort alpha $ >

0 commit comments

Comments
 (0)