wip

Author: MirceaS

12-proof-system-p.mm1

@@ -119,6 +119,12 @@ theorem prop_43_exists {box: SVar} {x: EVar} (ctx: Pattern box) (phi: Pattern bo
   $ (exists x (app[ phi / box ] ctx)) -> app[ exists x phi / box ] ctx $ =
   '(exists_generalization (eFresh_appCtx eFresh_disjoint eFresh_exists_same_var) (framing exists_intro_same_var));
 
+theorem prop_43_exists_fresh {box: SVar} {x: EVar} (ctx phi: Pattern box x)
+  (ctx_fresh: $ _eFresh x ctx $):
+  $ (exists x (app[ phi / box ] ctx)) -> app[ exists x phi / box ] ctx $ =
+  '(exists_generalization (eFresh_appCtx ctx_fresh eFresh_exists_same_var) (framing exists_intro_same_var));
+
+
 theorem exists_appCtx {x: EVar} {box: SVar} (ctx: Pattern box) (phi: Pattern x):
   $ (app[ exists x phi / box ] ctx) <-> exists x (app[ phi / box ] ctx) $ =
   '(ibii propag_exists_disjoint prop_43_exists);
@@ -1038,6 +1044,9 @@ do {
   (def (func_subst x phi1 phi1_pf func_phi2) '(
     exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) ,phi1_pf) ,func_phi2
   ))
+  (def (func_subst_alt x phi1 func_phi2) '(
+    anr imp_exists_disjoint (mp (exists_framing @ syl anr ,(func_subst_explicit_helper x phi1)) ,func_phi2)
+  ))
   (def (func_subst_thm func_phi2 x phi1) '(
     exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x (nth 4 @ get-decl phi1))) ,phi1) ,func_phi2
   ))
@@ -1231,7 +1240,3 @@ theorem in_exists_lemma {x: EVar} (phi: Pattern x): $ (x in exists x (eVar x /\
 theorem in_exists_to_forall_domain {x: EVar} (pred: Pattern x) (phi: Pattern):
   $ (phi C= exists x (eVar x /\ pred)) -> forall x (x in phi -> x in pred)$ =
   '(rsyl (subset_mem_disjoint_lemma eFresh_exists_same_var) @ forall_framing @ imim2 in_exists_lemma);
-
-theorem eq_pred_pointwise {box1 box2: SVar} {x: EVar} (phi: Pattern x box1 box2) (ctx1 ctx2: Pattern x box1 box2):
-  $ (phi C= exists x (eVar x /\ ((app[ eVar x / box1 ] ctx1) == (app[ eVar x / box2 ] ctx2)))) ->
-    ((app[ phi / box1 ] ctx1) == (app[ phi / box2 ] ctx2)) $ = '();

nominal/core.mm1

@@ -27,7 +27,7 @@ term abstraction_sym: Symbol;
 def abstraction (phi rho: Pattern): Pattern = $ (sym abstraction_sym) @@ phi @@ rho $;
 term supp_sym: Symbol;
 def supp (phi: Pattern): Pattern = $ (sym supp_sym) @@ phi $;
-def fresh_for {a: EVar} (phi: Pattern a): Pattern a = $ ~ (a in supp phi) $;
+def fresh_for (phi psi: Pattern): Pattern = $ ~ (phi C= supp psi) $;
 
 def EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
 $ s_forall alpha a (s_forall alpha b ((swap a b phi) == phi)) $;
@@ -88,7 +88,7 @@ axiom F1 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
   $ (is_atom a alpha) ->
     (is_atom b alpha) ->
     (is_of_sort phi tau) ->
-    ((fresh_for a phi) /\ (fresh_for b phi) -> ((swap a b phi) == phi)) $;
+    ((fresh_for (eVar a) phi) /\ (fresh_for (eVar b) phi) -> ((swap a b phi) == phi)) $;
 axiom F2 (alpha: Pattern) {a b: EVar}:
   $ is_atom_sort alpha $ >
   $ (is_atom a alpha) ->
@@ -100,12 +100,12 @@ axiom F3 (alpha1 alpha2: Pattern) {a b: EVar}:
   $ (is_atom a alpha1) ->
     (is_atom b alpha2) ->
     (alpha1 != alpha2) ->
-    (fresh_for a (eVar b)) $;
+    ((eVar a) != (eVar b)) $;
 axiom F4 (alpha tau phi: Pattern) {a: EVar}:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ (is_of_sort phi tau) ->
-    (s_exists alpha a (fresh_for a phi)) $;
+    (s_exists alpha a (fresh_for (eVar a) phi)) $;
 axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >

nominal/lambda.mm1

@@ -182,6 +182,7 @@ axiom subst_same_var {a: EVar} (plug: Pattern a):
 axiom subst_diff_var {a b: EVar} (plug: Pattern a b):
   $ (is_var (eVar a)) ->
     (is_var (eVar b)) ->
+    ((eVar a) != (eVar b)) -> 
     (is_exp plug) ->
     ((subst b (lc_var (eVar a)) plug) == (lc_var (eVar a))) $;
 axiom subst_app {a: EVar} (plug phi1 phi2: Pattern a):
@@ -195,21 +196,40 @@ axiom subst_lam {a b: EVar} (plug phi: Pattern a b):
     (is_var (eVar b)) ->
     (is_exp plug) ->
     (is_exp phi) ->
-    (fresh_for a plug) ->
+    (fresh_for (eVar a) plug) ->
     ((subst b (lc_lam_a a phi) plug) == (lc_lam_a a (subst b phi plug))) $;
 
-
-
-
-theorem subst_induction {a b: EVar} (phi1 plug1 plug2: Pattern):
-  $ (is_var (eVar a)) ->
-    (is_var (eVar b)) ->
-    (is_exp phi1) ->
-    (is_exp plug1) ->
-    (is_exp plug2) ->
-    (fresh_for a phi3) ->
-    ((subst b (subst a phi1 plug1) plug2) == (subst a (subst b phi1 plug2) (subst b plug1 plug2))) $ =
-    '();
+def subst_induction_pred (a b phi plug1 plug2: 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) = $ exists x ((eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) $;
+
+theorem subst_induction_app_lemma {x y: EVar} (a b phi1 plug1 plug2: Pattern)
+  (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 $):
+  $ (subst_induction_pred a b x plug1 plug2 /\ subst_induction_pred a b y plug1 plug2) -> subst_induction_pred a b (lc_app x y) plug1 plug2 $ =
+  '();
+
+theorem subst_induction_app (a b phi1 plug1 plug2: Pattern)
+  (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 $):
+  $ (lc_app (satisfying_exps a b plug1 plug2) (satisfying_exps a b plug1 plug2)) C= (satisfying_exps a b plug1 plug2) $ =
+  '();
+
+
+theorem subst_induction (a b phi1 plug1 plug2: Pattern)
+  (a_var: $ is_sorted_func Var a $)
+  (b_var: $ is_sorted_func Var b $)
+  (phi1_exp: $ is_exp phi1 $)
+  (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)) $ =
+  '(induction_principle);
 
 
 

sorts.mm0

@@ -19,6 +19,8 @@ def s_forall (s: Pattern) {x: EVar} (phi: Pattern x): Pattern = $ forall x ((eVa
 
 def is_sorted_pred (s: Pattern) (phi: Pattern): Pattern = $ (phi == bot) \/ (phi == dom s) $;
 
+def is_sorted_func {.x: EVar} (s: Pattern) (phi: Pattern): Pattern = $ s_exists s x (eVar x == phi) $;
+
 -- Singleton sort
 term pred_sym: Symbol;
 def pred: Pattern = $ sym pred_sym $;