finished main proof but with some gaps

Author: MirceaS

01-propositional.mm1

@@ -390,6 +390,7 @@ theorem con2: $ (aa -> ~bb) -> (bb -> ~aa) $ = '(a3d (syl5 dne id));
 theorem notnot1: $ aa -> ~~aa $ = '(con2 id);
 theorem con3: $ (aa -> bb) -> (~bb -> ~aa) $ = '(syl con2 (imim2i notnot1));
 theorem con1: $ (~aa -> bb) -> (~bb -> aa) $ = '(a3d (imim2i notnot1));
+theorem con4: $ (~aa -> ~bb) -> (bb -> aa) $ = '(syl (imim1 notnot1) con1);
 theorem cases (h1: $ aa -> bb $) (h2: $ ~aa -> bb $): $ bb $ = '(contra @ syl h1 @ con1 h2);
 theorem casesd (h1: $ aa -> bb -> c $) (h2: $ aa -> ~bb -> c $): $ aa -> c $ =
 '(cases (com12 h1) (com12 h2));

02-ml-normalization.mm1

@@ -33,6 +33,10 @@ theorem eFresh_not {x: EVar} (phi: Pattern x)
   $ _eFresh x (~ phi) $ =
   '(eFresh_imp h eFresh_disjoint);
 
+theorem eFresh_forall_same_var {x: EVar} (phi: Pattern x):
+  $ _eFresh x (forall x phi) $ =
+  '(eFresh_not eFresh_exists_same_var);
+
 theorem sFresh_not {X: SVar} (phi: Pattern X)
   (h: $ _sFresh X phi $):
   $ _sFresh X (~ phi) $ =

12-proof-system-p.mm1

@@ -145,6 +145,13 @@ theorem prop_43_exists_def {x: EVar} (phi: Pattern x):
   $ (exists x (|^ phi ^|)) -> |^ exists x phi ^| $ =
   '(exists_generalization (eFresh_app eFresh_disjoint eFresh_exists_same_var) (framing_def exists_intro_same_var));
 
+
+theorem forall_floor {x: EVar} (phi: Pattern x):
+  $ |_ forall x phi _| <-> forall x (|_ phi _|) $ =
+  '(ian
+    (con3 @ rsyl (exists_framing dne) @ rsyl prop_43_exists_def @ framing_def notnot1)
+    (con3 @ rsyl (framing_def dne) @ rsyl propag_exists_def @ exists_framing notnot1));
+
 do {
   (def (ex_appCtx_subst subst) '(norm (norm_equiv ,subst @ norm_exists ,subst) exists_appCtx))
   (def (or_appCtx_subst subst) '(norm (norm_equiv ,subst @ norm_or ,subst ,subst) or_appCtx))
@@ -166,6 +173,10 @@ theorem propag_and_floor: $|_ phi /\ psi _| <-> |_ phi _| /\ |_ psi _|$ =
     (rsyl (anr notor) @ rsyl (con3 propag_or_def) @ con3 @ framing_def @ anl notan)
   );
 
+theorem prop_43_or_def_rev (phi1 phi2: Pattern):
+  $ |^ phi1 \/ phi2 ^| -> (|^ phi1 ^| \/ |^ phi2 ^|) $ =
+  '(syl (orim (framing_def dne) (framing_def dne)) @ rsyl (framing_def @ orim notnot1 notnot1) @ con4 @ rsyl (anl notor) @ rsyl (anr propag_and_floor) @ con3 @ framing_def (anr notan));
+
 theorem appCtxLR {box: SVar} (phi2 phi3: Pattern) (phi1 phi4: Pattern box):
   $ Norm (app[ phi1 / box ] (app (app phi3 phi4) phi2)) (app (app phi3 (app[ phi1 / box ] phi4)) phi2) $ =
   '(norm_trans appCtxL_disjoint @ norm_app_l appCtxR_disjoint);
@@ -243,11 +254,6 @@ theorem cong_of_equiv_mem {x: EVar} (phi1 phi2: Pattern x)
 theorem cong_of_equiv_eq (h1: $phi1 <-> phi2$) (h2: $psi1 <-> psi2$): $(phi1 == psi1) <-> (phi2 == psi2)$ =
   '(cong_of_equiv_not @ cong_of_equiv_def @ cong_of_equiv_not @ cong_of_equiv_equiv h1 h2);
 
-do {
-  (def (cong_eq_lift pf to_eq) '(equiv_to_eq @ ,pf (corollary_57_floor ,to_eq)))
-  (def (cong_eq_lift2 pf to_eq1 to_eq2) '(equiv_to_eq @ ,pf (corollary_57_floor ,to_eq1) (corollary_57_floor ,to_eq2)))
-};
-
 theorem univ_gene {x: EVar} (phi: Pattern x)
   (p: $ phi $):
   $ forall x phi $ = '(exists_generalization_disjoint @ notnot1 p);
@@ -589,6 +595,15 @@ do {
 
 -- Equality reasoning
 
+do {
+  (def (cong_eq_lift pf to_eq) '(equiv_to_eq @ ,pf (corollary_57_floor ,to_eq)))
+  (def (cong_eq_lift2 pf to_eq1 to_eq2) '(equiv_to_eq @ ,pf (corollary_57_floor ,to_eq1) (corollary_57_floor ,to_eq2)))
+};
+
+theorem cong_of_eq_exists {x: EVar} (phi1 phi2: Pattern x)
+  (h: $ phi1 == phi2 $): $ (exists x phi1) == (exists x phi2) $ =
+  (cong_eq_lift 'cong_of_equiv_exists 'h);
+
 theorem in_refl: $ x in eVar x $ =
   '(framing_def (iand id id) definedness);
 
@@ -688,10 +703,15 @@ theorem eq_to_app
   $ (phi1 == phi2) -> ((app psi1 rho1) -> (app psi2 rho2)) $ =
   '(syld (eq_to_app_l h1) (eq_to_app_r h2));
 
-theorem eq_to_exists {x: EVar} (phi1 phi2: Pattern) (psi1 psi2: Pattern x)
-  (h: $ (phi1 == phi2) -> (psi1 -> psi2) $):
-  $ (phi1 == phi2) -> ((exists x psi1) -> (exists x psi2)) $ =
-  '(exp @ rsyl and_exists_disjoint_reverse @ exists_framing @ curry h);
+theorem eq_to_exists_fresh {x: EVar} (phi psi1 psi2: Pattern x)
+  (freshness: $_eFresh x phi$)
+  (h: $ phi -> (psi1 -> psi2) $):
+  $ phi -> ((exists x psi1) -> (exists x psi2)) $ =
+  '(exp @ rsyl (and_exists_fresh_reverse freshness) @ exists_framing @ curry h);
+theorem eq_to_exists {x: EVar} (phi: Pattern) (psi1 psi2: Pattern x)
+  (h: $ phi -> (psi1 -> psi2) $):
+  $ phi -> ((exists x psi1) -> (exists x psi2)) $ =
+  '(eq_to_exists_fresh eFresh_disjoint h);
 
 do {
   (def (bi_lift pf to_equiv) '(iand (,pf @ syl anl ,to_equiv) (,pf @ syl anr ,to_equiv)))
@@ -793,9 +813,13 @@ theorem eq_to_eq_r_bi
   (h: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
   $ (phi1 == phi2) -> ((rho == psi1) <-> (rho == psi2)) $ = '(eq_to_eq_bi eq_to_id_bi h);
 
-theorem eq_to_exists_bi {x: EVar} (phi1 phi2: Pattern) (psi1 psi2: Pattern x)
-  (h: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
-  $ (phi1 == phi2) -> ((exists x psi1) <-> (exists x psi2)) $ = (bi_lift 'eq_to_exists 'h);
+theorem eq_to_exists_bi_fresh {x: EVar} (phi psi1 psi2: Pattern x)
+  (freshness: $ _eFresh x phi $)
+  (h: $ phi -> (psi1 <-> psi2) $):
+  $ phi -> ((exists x psi1) <-> (exists x psi2)) $ = '(iand (eq_to_exists_fresh freshness @ syl anl h) (eq_to_exists_fresh freshness @ syl anr h));
+theorem eq_to_exists_bi {x: EVar} (phi: Pattern) (psi1 psi2: Pattern x)
+  (h: $ phi -> (psi1 <-> psi2) $):
+  $ phi -> ((exists x psi1) <-> (exists x psi2)) $ = '(eq_to_exists_bi_fresh eFresh_disjoint h);
 theorem eq_to_forall_bi {x: EVar} (phi1 phi2: Pattern) (psi1 psi2: Pattern x)
   (h: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
   $ (phi1 == phi2) -> ((forall x psi1) <-> (forall x psi2)) $ =
@@ -986,12 +1010,16 @@ theorem eq_imp_eq_framing {box: SVar} (ctx phi psi: Pattern box):
   '(rsyl (iand eq_imp_subset @ rsyl eq_sym eq_imp_subset) @ rsyl (anim subset_imp_subset_framing subset_imp_subset_framing) @ curry subset_to_eq);
 
 do {
-  (def (subset_imp_subset_framing_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) subset_imp_subset_framing))
+  (def (subset_imp_subset_framing_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) (!! subset_imp_subset_framing box)))
   (def (eq_imp_eq_framing_subst subst) '(norm (norm_imp_r @ norm_eq ,subst ,subst) eq_imp_eq_framing))
 };
 
-
 do {
+  (def (appCtx_constructor path) @ if (null? path) 'appCtxVar @ if {(hd path) = 0}
+    '(norm_trans appCtxL_disjoint @ norm_app ,(appCtx_constructor (tl path)) norm_refl)
+    '(norm_trans appCtxR_disjoint @ norm_app norm_refl ,(appCtx_constructor (tl path)))
+  )
+
   (def (cong_of_equiv_propag x equiv_pf ctx) @ match ctx
     [$eVar ,y$ (if (== x y) equiv_pf 'biid)]
     [$exists ,y ,psi$ (if (== x y) 'biid '(cong_of_equiv_exists ,(cong_of_equiv_propag x equiv_pf psi)))]
@@ -1255,3 +1283,13 @@ do {
     '(rsyl (rsyl ,(inst_foralls {n - 1}) ,(forall_imp_climb {n - 1})) var_subst_same_var)
   ))
 };
+
+theorem imp_eq_to_conj_in_eq:
+  $ (|^ phi1 ^| -> (phi2 == phi3)) -> ((phi2 /\ |^ phi1 ^|) == (phi3 /\ |^ phi1 ^|)) $ =
+  '(rsyl (imim1 dne) @ eori
+    (rsyl (anl not_ceil_floor_bi) @ rsyl (anr floor_idem) @
+    framing_floor @ rsyl (anr not_ceil_floor_bi) @ iand
+      (com12 @ rsyl anr @ com12 absurd)
+      (com12 @ rsyl anr @ com12 absurd)
+    ) @
+    eq_equiv_to_eq_eq @ eq_to_and_l_bi eq_to_intro_bi);

nominal/lambda.mm1

@@ -100,19 +100,19 @@ theorem lc_lemma_1 {x: EVar} (exp_pred exp_suff_fresh: Pattern)
   (exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
   (h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
   $ s_exists Var x ((lc_lam_a x exp_pred) C= exp_pred) $ =
-  (named '(exists_framing (rsyl (anl eVar_in_subset) @ iand
+  '(exists_framing (rsyl (anl eVar_in_subset) @ iand
     (com12 subset_trans exp_suff_fresh_sorting)
     (rsyl (syl
         ,(subset_imp_subset_framing_subst 'appCtxRVar)
         ,(subset_imp_subset_framing_subst 'appCtxLRVar)
       ) @ com12 subset_trans h_abs))
-    @ anl lemma_ceil_exists_membership exp_suff_fresh_nonempty));
+    @ anl lemma_ceil_exists_membership exp_suff_fresh_nonempty);
 
 theorem lc_lemma_2 {x y: EVar} (exp_pred: Pattern)
   (exp_pred_sorting: $ is_exp exp_pred $)
   (exp_pred_ev: $ EV_pattern Var exp_pred $):
   $ (((is_var (eVar x)) /\ (is_var (eVar y))) /\ ((lc_lam_a y exp_pred) C= exp_pred)) -> ((lc_lam_a x exp_pred) C= exp_pred) $ =
-  (named '(
+  '(
     rsyl (anim2 ,(subset_imp_subset_framing_subst 'appCtxRVar)) @
     rsyl (iand anl @ 
             rsyl (anim1 @
@@ -122,7 +122,7 @@ theorem lc_lemma_2 {x y: EVar} (exp_pred: Pattern)
             curry subset_trans) @
     rsyl (anim1 @ rsyl ancom @ exp_pred_ev_unquantified exp_pred_ev) @
     curry @
-    syl anl ,(func_subst_explicit_helper 'hole $(_ @@ (_ @@ (eVar hole))) C= (eVar hole)$)));
+    syl anl ,(func_subst_explicit_helper 'hole $(_ @@ (_ @@ (eVar hole))) C= (eVar hole)$));
 
 theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
   (exp_pred_sorting: $ is_exp exp_pred $)
@@ -171,9 +171,14 @@ theorem induction_principle (exp_pred exp_suff_fresh: Pattern)
   ) exp_pred_sorting));
 
 
+
+---- Substitution
+
+-- base term and definition
 term subst_sym: Symbol;
 def subst (a phi1 phi2: Pattern): Pattern = $ (sym subst_sym) @@ a @@ phi1 @@ phi2 $;
 
+-- subst axioms
 axiom function_subst: $ ,(is_function '(sym subst_sym) '[Var Exp Exp] 'Exp) $;
 axiom subst_same_var {a: EVar} (plug: Pattern a):
   $ (is_var (eVar a)) ->
@@ -192,31 +197,26 @@ axiom subst_app (a phi1 phi2 plug: Pattern):
     (is_exp phi2) ->
     ((subst a (lc_app phi1 phi2) plug) == (lc_app (subst a phi1 plug) (subst a phi2 plug))) $;
 axiom subst_lam {a b: EVar} (plug phi: Pattern a b):
-  $ (is_var (eVar a)) ->
+  $ ((eVar a) != (eVar b)) ->
+    (is_var (eVar a)) ->
     (is_var (eVar b)) ->
     (is_exp plug) ->
     (is_exp phi) ->
     (fresh_for (eVar a) plug) ->
     ((subst (eVar b) (lc_lam_a a phi) plug) == (lc_lam_a a (subst (eVar b) phi plug))) $;
 
--- phi[a / plug1][b / plug2] == phi[b / plug2][a / plug1[b / plug2]]
-
--- (app x y)[a / plug1][b / plug2] == (app x y)[b / plug2][a / plug1[b / plug2]]
--- (app (x[a / plug1]) (y[a / plug1]))[b / plug2] == (app (x[b / plug2]) (y[b / plug2]))[a / plug1[b / plug2]]
--- app (x[a / plug1][b / plug2]) (y[a / plug1][b / plug2]) == app (x[b / plug2][a / plug1[b / plug2]]) (y[b / plug2][a / plug1[b / plug2]])
 
+-- induction proof
 def subst_induction_pred (a b phi plug1 plug2: Pattern): Pattern = $ (subst b (subst a phi plug1) plug2) == (subst a (subst b phi plug2) (subst b plug1 plug2)) $;
 def satisfying_exps {.x: EVar} (a b plug1 plug2: Pattern): Pattern = $ s_exists Exp x ((eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) $;
 
-theorem subst_induction_app_lemma {x y: EVar} (a b plug1 plug2: Pattern)
-  (diff_atoms: $ a != b $)
+theorem subst_induction_app_lemma
   (a_var: $ is_sorted_func Var a $)
   (b_var: $ is_sorted_func Var b $)
   (plug1_exp: $ is_exp plug1 $)
-  (plug2_exp: $ is_exp plug2 $)
-  (a_fresh: $ fresh_for a phi3 $):
+  (plug2_exp: $ is_exp plug2 $):
   $ (is_exp (eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) /\ (is_exp (eVar y) /\ subst_induction_pred a b (eVar y) plug1 plug2) -> subst_induction_pred a b (lc_app (eVar x) (eVar y)) plug1 plug2 $ =
-  '(rsyl (anl an4) @ rsyl (anim2 @
+  (named '(rsyl (anl an4) @ rsyl (anim2 @
     syl (curry eq_trans) @
     iand
       (rsyl anl @ eq_equiv_to_eq_eq ,(func_subst_explicit_helper 'z $_ @@ (eVar z) @@ _$))
@@ -228,7 +228,23 @@ theorem subst_induction_app_lemma {x y: EVar} (a b plug1 plug2: Pattern)
     (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
     (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
     )) @
-  _);
+  rsyl (anim2 @ curry eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl ,(eq_imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app a_var plug1_exp) @
+  rsyl (anim2 @ curry eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl eq_sym @ syl (curry @ subst_app a_var (mp (mp (mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug1_exp) plug2_exp)) (anim
+    (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
+    (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
+    )) @
+  rsyl (anim2 @ impcom eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl eq_sym @ syl ,(eq_imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app b_var plug2_exp) @
+  rsyl (anim2 @ impcom eq_trans) @
+  anr));
 
 theorem subst_induction_app (a b plug1 plug2: Pattern)
   (lemma: $ (is_exp (eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) /\ (is_exp (eVar y) /\ subst_induction_pred a b (eVar y) plug1 plug2) -> subst_induction_pred a b (lc_app (eVar x) (eVar y)) plug1 plug2 $):
@@ -263,17 +279,37 @@ theorem subst_induction_app (a b plug1 plug2: Pattern)
     rsyl (anim1 @ curry @ mp ,(inst_foralls 2) function_lc_app) @
     curry ,(func_subst_alt_thm_sorted 'x $(eVar x) /\ ((app (app _ (app (app _ (eVar x)) _)) _) == (app (app _ (app (app _ (eVar x)) _)) _))$)));
 
+theorem subst_induction_lemma (a b phi plug1 plug2: Pattern)
+  (diff_atoms: $ a != b $)
+  (a_var: $ is_sorted_func Var a $)
+  (b_var: $ is_sorted_func Var b $)
+  (phi_exp: $ is_exp phi $)
+  (plug1_exp: $ is_exp plug1 $)
+  (plug2_exp: $ is_exp plug2 $)
+  (a_fresh: $ fresh_for a plug2 $):
+  $ Exps == (satisfying_exps a b plug1 plug2) $ =
+  '(induction_principle _ _ _ _ _ (subst_induction_app @ subst_induction_app_lemma a_var b_var plug1_exp plug2_exp) _);
 
-theorem subst_induction (a b phi1 plug1 plug2: Pattern)
+theorem subst_induction (a b phi plug1 plug2: Pattern)
   (diff_atoms: $ a != b $)
   (a_var: $ is_sorted_func Var a $)
   (b_var: $ is_sorted_func Var b $)
-  (phi1_exp: $ is_exp phi1 $)
+  (phi_exp: $ is_exp phi $)
   (plug1_exp: $ is_exp plug1 $)
   (plug2_exp: $ is_exp plug2 $)
-  (a_fresh: $ fresh_for a phi3 $):
-  $ (subst b (subst a phi1 plug1) plug2) == (subst a (subst b phi1 plug2) (subst b plug1 plug2)) $ =
-  '();
+  (a_fresh: $ fresh_for a plug2 $):
+  $ (subst b (subst a phi plug1) plug2) == (subst a (subst b phi plug2) (subst b plug1 plug2)) $ =
+  (named '(mp (
+    rsyl (com12 subset_trans @ eq_imp_subset @ subst_induction_lemma diff_atoms a_var b_var phi_exp plug1_exp plug2_exp a_fresh) @
+    rsyl (subset_mem_disjoint_lemma eFresh_disjoint) @
+    rsyl (forall_framing (rsyl
+      (imim2 @ rsyl membership_exists_forward @ exists_generalization_disjoint @ rsyl (anl ,(propag_mem 'x $(_ C= _) /\ ((eVar _) /\ (_ == _))$)) @ rsyl anr (curry @ syl anr ,(func_subst_explicit_helper 'x $(app (app _ (app (app _ (eVar x)) _)) _) == (app (app _ (app (app _ (eVar x)) _)) _)$)))
+      (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) (anl ceil_floor_floor)))) @
+    rsyl (anr forall_floor) @
+    syl (rsyl
+      (eq_trans @ equiv_to_eq ,(appCtx_pointwise_subst @ appCtx_constructor '[0 1 0 1])) @
+      com12 eq_trans @ eq_sym @ equiv_to_eq ,(appCtx_pointwise_subst @ appCtx_constructor '[0 1 0 1])) @
+    framing_floor @ eq_to_exists_bi_fresh eFresh_forall_same_var @ syl corollary_57_floor @ rsyl var_subst_same_var imp_eq_to_conj_in_eq) phi_exp));