finished proof

Author: MirceaS

01-propositional.mm1

@@ -773,3 +773,12 @@ theorem iand4 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -
 
 theorem iand5 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $) (h5: $ aa -> f $): $ aa -> bb /\ c /\ d /\ e /\ f $ =
   '(iand (iand (iand (iand h1 h2) h3) h4) h5);
+
+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 $ =
+  '(iand (iand (iand (iand (iand h1 h2) h3) h4) h5) h6);
+
+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 $ =
+  '(iand (iand (iand (iand (iand (iand h1 h2) h3) h4) h5) h6) h7);
+
+theorem imp_or_extract: $ (aa -> bb) \/ (aa -> c) <-> (aa -> (bb \/ c)) $ =
+  '(ibii (eori (imim2 orl) (imim2 orr)) imp_or_split);

10-theory-definedness.mm0

@@ -29,6 +29,21 @@ def is_func {.x: EVar} (phi: Pattern): Pattern = $ exists x (eVar x == phi) $;
 
 def is_pred (phi: Pattern): Pattern = $ (phi == bot) \/ (phi == top) $;
 
+--- Domain Quantifiers
+----------------------
+
+def exists_in {x: EVar} (phi psi: Pattern x): Pattern = $ exists x ((eVar x C= phi) /\ psi) $;
+notation exists_in {x: EVar} (phi psi: Pattern x): Pattern = ($E$:0) x ($:$:0) phi ($.$:0) psi;
+
+def forall_in {x: EVar} (phi psi: Pattern x): Pattern = $ forall x ((eVar x C= phi) -> psi) $;
+notation forall_in {x: EVar} (phi psi: Pattern x): Pattern = ($A$:0) x ($:$:0) phi ($.$:0) psi;
+
+
+def is_sorted_pred (phi psi: Pattern): Pattern = $ (psi == bot) \/ (psi == phi) $;
+
+def is_sorted_func {.x: EVar} (phi psi: Pattern): Pattern = $ E x : phi . eVar x == psi $;
+
+
 --- Contextual Implications
 ---------------------------
 

12-proof-system-p.mm1

@@ -365,6 +365,10 @@ theorem subset_imp_or_subset_r:
 theorem subset_and: $ (phi C= (psi1 /\ psi2)) -> (phi C= psi1) /\ (phi C= psi2) $ =
   '(iand (framing_subset id anl) (framing_subset id anr));
 
+theorem and_subset: $ (phi1 C= psi) /\ (phi2 C= psi) <-> (phi1 \/ phi2 C= psi) $ =
+  '(ibii (rsyl (anr propag_and_floor) @ framing_floor @ curry eor) @
+  iand (framing_floor @ imim1 orl) (framing_floor @ imim1 orr));
+
 theorem taut_equiv_top (h: $ phi $): $ phi <-> top $ =
   '(ibii imp_top @ a1i h);
 theorem taut_and_equiv (h: $ phi $): $ phi /\ psi <-> psi $ =
@@ -1052,12 +1056,12 @@ theorem ceil_appCtx_dual (phi: Pattern) {box: SVar} (ctx: Pattern box):
   $ |^ phi ^| -> ~ (app[ (~ (|^ phi ^|)) / box ] ctx) $ =
   '(rsyl (anr floor_ceil_ceil) @ rsyl floor_appCtx_dual @ con3 @ framing @ con3 @ anl floor_ceil_ceil);
 
-theorem ceil_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
+theorem floor_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
   $ (app[ |_ phi _| -> psi / box ] ctx) -> |_ phi _| -> app[ psi / box ] ctx $ =
   '(exp @ rsyl (anim propag_or floor_appCtx_dual) @ rsyl (anl andir) @ eori (syl absurdum @ rsyl (anim1 @ framing notnot1) @ notnot1 notnot1) anl);
 
 do {
-  (def (ceil_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) ceil_imp_in_appCtx))
+  (def (floor_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) floor_imp_in_appCtx))
 };
 
 theorem alpha_exists {x y: EVar} (phi: Pattern x y)
@@ -1291,6 +1295,21 @@ theorem ceil_is_pred: $ (|^ phi ^| == bot) \/ (|^ phi ^| == top) $ =
     @ rsyl anr @ mpcom taut)
     emr);
 
+theorem floor_is_pred: $ (|_ phi _| == bot) \/ (|_ phi _| == top) $ =
+  '(orim
+    (anl
+    @ bitr (bicom @ cong_of_equiv_not @ ceil_floor_floor)
+    @ bitr not_ceil_floor_bi
+    @ cong_of_equiv_floor
+    @ ibii (iand id @ a1i absurdum)
+    anl)
+    (anl
+    @ bitr (bicom floor_idem)
+    @ cong_of_equiv_floor
+    @ ibii (iand (a1i imp_top) @ com12 @ a1i id)
+    @ rsyl anr @ mpcom taut)
+    emr);
+
 theorem ceil_idempotency_for_pred (phi: Pattern): $ ((phi == bot) \/ (phi == top)) <-> (phi == |^ phi ^|) $ =
   (named '(ibii
     (eori
@@ -1543,3 +1562,47 @@ do {
     [_ 'biid]
   )
 };
+
+theorem is_pred_floor: $ (is_pred phi) <-> (phi == |_ phi _|) $ =
+  '(ibii
+    (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)
+    (rsyl ,(func_subst_explicit_helper 'x $((eVar x) == bot) \/ ((eVar x) == top)$) @ rsyl anr @ mpcom floor_is_pred));
+
+theorem KT_imp {X: SVar} (ctx ante phi: Pattern X)
+  (pos: $ _Positive X ctx $)
+  (propag: $ (s[ ante -> phi / X ] ctx) -> ante -> s[ phi / X ] ctx $)
+  (h: $ ante -> (s[ phi / X ] ctx) -> phi $):
+  $ ante -> (mu X ctx) -> phi $ =
+  '(com12 @ KT pos @ rsyl propag (prop_2 h));
+
+theorem KT_subset {X: SVar} (ctx phi: Pattern X)
+  (pos: $ _Positive X ctx $)
+  (propag: $ (s[ ((s[ phi / X ] ctx) C= phi) -> phi / X ] ctx) -> ((s[ phi / X ] ctx) C= phi) -> s[ phi / X ] ctx $):
+  $ ((s[ phi / X ] ctx) C= phi) -> ((mu X ctx) C= phi) $ =
+  '(rsyl (anr floor_idem) @ framing_floor @ KT_imp pos propag corollary_57_floor);
+
+do {
+  (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))
+};
+
+
+theorem floor_extract_app
+  (h1: $ phi1 -> |_ psi _| -> rho1 $)
+  (h2: $ phi2 -> |_ psi _| -> rho2 $):
+  $ (app phi1 phi2) -> |_ psi _| -> app rho1 rho2 $ =
+  (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));
+
+theorem floor_extract_or
+  (h1: $ phi1 -> |_ psi _| -> rho1 $)
+  (h2: $ phi2 -> |_ psi _| -> rho2 $):
+  $ phi1 \/ phi2 -> |_ psi _| -> rho1 \/ rho2 $ =
+  '(rsyl (orim h1 h2) @ anl imp_or_extract);
+
+do {
+  (def (floor_extract x ctx) @ match ctx
+    [$eVar ,y$ (if (== x y) 'id 'prop_1)]
+    [$app ,phi1 ,phi2$  '(floor_extract_app ,(floor_extract x phi1) ,(floor_extract x phi2))]
+    [$or  ,phi1 ,phi2$  '(floor_extract_or  ,(floor_extract x phi1) ,(floor_extract x phi2))]
+    [_                  'prop_1]
+  )
+};

nominal/core.mm1

@@ -13,12 +13,11 @@ axiom atoms_nominal_sorts: $ dom atoms C= dom nominal_sorts $;
 
 term sort_abstraction_sym: Symbol;
 def sort_abstraction (abs body: Pattern): Pattern = $ (sym sort_abstraction_sym) @@ abs @@ body $;
--- TODO: Check if output sort should be `sorts` or it's okay for it to be `nominal_sorts` (e,g, can we have something like `[a1] [a2] t`? The choice of `nominal_sorts` assumes yes)
 axiom function_sort_abstraction: $ ,(is_function '(sym sort_abstraction_sym) '[atoms nominal_sorts] 'nominal_sorts) $;
 
 def is_atom_sort (alpha: Pattern): Pattern = $ (is_func alpha) /\ (alpha C= dom atoms) $;
 def is_nominal_sort (tau: Pattern): Pattern = $ (is_func tau) /\ (tau C= dom nominal_sorts) $;
-def is_atom (a alpha: Pattern): Pattern = $ is_sorted_func alpha a $;
+def is_atom (a alpha: Pattern): Pattern = $ is_sorted_func (dom alpha) a $;
 
 axiom nominal_sorts_are_sorts: $ (is_nominal_sort phi) -> (is_sort phi) $;
 
@@ -29,6 +28,13 @@ def abstraction (phi rho: Pattern): Pattern = $ (sym abstraction_sym) @@ phi @@
 term supp_sym: Symbol;
 def supp (phi: Pattern): Pattern = $ (sym supp_sym) @@ phi $;
 def fresh_for (phi psi: Pattern): Pattern = $ ~ (phi C= supp psi) $;
+term comma_sym: Symbol;
+def comma (phi psi: Pattern): Pattern = $ (sym comma_sym) @@ phi @@ psi $;
+infixl comma: $,,$ prec 35;
+term comma_sort_sym: Symbol;
+def comma_sort: Pattern = $ sym comma_sort_sym $;
+
+axiom comma_sort_nominal: $ is_nominal_sort comma_sort $;
 
 def EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
 $ s_forall alpha a (s_forall alpha b ((swap (eVar a) (eVar b) phi) == phi)) $;
@@ -48,6 +54,10 @@ axiom multifunction_supp:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ ,(is_multi_function '(sym supp_sym) '[tau] 'alpha) $;
+axiom function_comma:
+  $ is_nominal_sort tau1 $ >
+  $ is_nominal_sort tau2 $ >
+  $ ,(is_function '(sym comma_sym) '[tau1 tau2] 'comma_sort) $;
 
 axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
   $ is_atom_sort alpha $ >
@@ -56,14 +66,40 @@ axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
     (is_of_sort phi alpha) ->
     (is_of_sort psi tau) ->
     ((swap (eVar a) (eVar b) (abstraction phi psi)) == abstraction (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
--- add EV axiom for swap
-axiom EV_supp {a b: EVar}  (tau: Pattern) (phi: Pattern a b):
+
+axiom EV_swap {a b c d: EVar} (alpha tau: Pattern) (phi: Pattern a b c d):
+  $ is_atom_sort alpha $ >
+  $ is_nominal_sort tau $ >
+  $ s_forall alpha a (s_forall alpha b (s_forall alpha c (s_forall alpha d (
+    (is_of_sort phi alpha) ->
+    (is_of_sort psi tau) ->
+    ((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)))))) $;
+
+axiom EV_supp {a b: EVar} (alpha tau: Pattern) (phi: Pattern a b):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ s_forall alpha a (s_forall alpha b (
     (is_of_sort phi tau) ->
     ((swap (eVar a) (eVar b) (supp phi)) == supp (swap (eVar a) (eVar b) phi)))) $;
 
+axiom EV_comma {a b: EVar}  (alpha tau: Pattern) (phi1 phi2: Pattern a b):
+  $ is_atom_sort alpha $ >
+  $ is_nominal_sort tau $ >
+  $ s_forall alpha a (s_forall alpha b (
+    (is_of_sort phi1 tau) ->
+    (is_of_sort phi2 tau) ->
+    ((swap (eVar a) (eVar b) (phi1 ,, phi2)) == ((swap (eVar a) (eVar b) phi1) ,, (swap (eVar a) (eVar b) phi2))))) $;
+
+axiom fresh_comma {a: EVar} (alpha tau1 tau2: Pattern) (phi1 phi2: Pattern a):
+  $ is_atom_sort alpha $ >
+  $ is_nominal_sort tau1 $ >
+  $ is_nominal_sort tau2 $ >
+  $ s_forall alpha a (
+    (is_of_sort phi1 tau1) ->
+    (is_of_sort phi2 tau2) ->
+    (fresh_for (eVar a) (phi1 ,, phi2)) ->
+    (fresh_for (eVar a) phi1) /\ (fresh_for (eVar a) phi2)) $;
+
 axiom EV_pred (alpha tau: Pattern):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
@@ -110,7 +146,7 @@ axiom F3 {a b: EVar} (alpha1 alpha2: Pattern a b):
 axiom F4 {a: EVar} (alpha tau phi: Pattern):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
-  $ (is_sorted_func tau phi) ->
+  $ (is_sorted_func (dom tau) phi) ->
     (s_exists alpha a (fresh_for (eVar a) phi)) $;
 axiom A1 {a b: EVar} (alpha tau phi rho: Pattern a b):
   $ is_atom_sort alpha $ >