Skip to content

Commit 42babb6

Browse files
committed
wip
1 parent 5ebf6d3 commit 42babb6

File tree

2 files changed

+97
-75
lines changed

2 files changed

+97
-75
lines changed

nominal/core.mm1

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,15 @@ axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
5656
(is_of_sort phi alpha) ->
5757
(is_of_sort psi tau) ->
5858
((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
59+
60+
axiom EV_swap {a b c d: EVar} (alpha tau: Pattern) (phi: Pattern a b c d):
61+
$ is_atom_sort alpha $ >
62+
$ is_nominal_sort tau $ >
63+
$ s_forall alpha a (s_forall alpha b (s_forall alpha c (s_forall alpha d (
64+
(is_of_sort phi alpha) ->
65+
(is_of_sort psi tau) ->
66+
((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)))))) $;
67+
6068
axiom EV_supp {a b: EVar} (tau: Pattern) (phi: Pattern a b):
6169
$ is_atom_sort alpha $ >
6270
$ is_nominal_sort tau $ >

nominal/lambda.mm1

Lines changed: 88 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,11 @@ axiom EV_lc_var {a b: EVar} (c: Pattern a b):
2323
term lc_app_sym: Symbol;
2424
def lc_app (phi rho: Pattern): Pattern = $ (sym lc_app_sym) @@ phi @@ rho $;
2525
axiom function_lc_app: $ ,(is_function '(sym lc_var_app) '[Exp Exp] 'Exp) $;
26+
axiom EV_lc_app {a b: EVar} (phi psi: Pattern a b):
27+
$ s_forall Var a (s_forall Var b (
28+
(is_of_sort phi Exp) ->
29+
(is_of_sort psi Exp) ->
30+
((swap (eVar a) (eVar b) (lc_app phi psi)) == lc_app (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
2631

2732
term lc_lam_sym: Symbol;
2833
def lc_lam (phi: Pattern): Pattern = $ (sym lc_lam_sym) @@ phi $;
@@ -454,6 +459,24 @@ theorem curried_function_swap_atom {a b c: EVar}:
454459
theorem satisfying_exps2_is_exp: $ is_exp satisfying_exps2 $ =
455460
(named '(imp_to_subset @ exists_generalization_disjoint @ rsyl (anim2 anl) @ curry subset_to_imp));
456461

462+
theorem subset_trans_var_lemma {x: EVar} (phi psi: Pattern x):
463+
$ (phi C= psi) -> (x in phi) -> ((eVar x) C= psi) $ =
464+
'(rsyl (com12 subset_trans) @ imim1 eVar_in_subset_forward);
465+
466+
theorem var_in_satisfying_exps2:
467+
$(x in satisfying_exps2) <-> (is_exp (eVar x)) /\ s_forall Var a (s_forall Var b (s_forall Exp plug1 (s_forall Exp plug2 ((fresh_for (eVar a) (eVar plug2)) /\ (eVar a != eVar b) -> subst_induction_pred (eVar a) (eVar b) (eVar x) (eVar plug1) (eVar plug2)))))$ =
468+
(named '(ibii
469+
(iand (subset_trans_var_lemma satisfying_exps2_is_exp) @
470+
rsyl (anl ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
471+
exists_generalization_disjoint @
472+
rsyl anr @
473+
curry @
474+
syl anr ,(func_subst_explicit_helper 'x $forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))$)) @
475+
476+
syl (anr ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
477+
syl ,(exists_intro_subst @ propag_e_subst 'x $((eVar x) C= bot) /\ ((bot == (eVar x)) /\ (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))))$) @
478+
anim2 @ ian eq_refl));
479+
457480
theorem EV_set: $ EV_pattern Var satisfying_exps2 $ =
458481
(named '(univ_gene @ anr imp_r_forall_disjoint @ univ_gene @ exp @ syl (curry subset_to_eq) @ syl
459482
(iand anr @ rsyl (anim
@@ -586,11 +609,9 @@ theorem mem_func_lemma_neg:
586609
(named '(com12 ,(func_subst_explicit_thm 'y2 $~(z in (eVar y2)) -> ~((eVar z) == (eVar y2))$) @ univ_gene @ con3 membership_var_reverse));
587610

588611
theorem subst_induction_var2: $ (lc_var Vars) C= satisfying_exps2 $ =
589-
(named '(imp_to_subset @ membership_elim @ forall_framing membership_imp_reverse @ univ_gene @
590-
syl (anr ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
591-
syl ,(exists_intro_subst @ propag_e_subst 'x $((eVar x) C= bot) /\ ((bot == (eVar x)) /\ (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))))$) @
592-
iand (rsyl eVar_in_subset_forward @ com12 subset_trans @ mp ,(function_sorting_full 1) function_lc_var) @
593-
iand (a1i eq_refl) @
612+
(named '(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
613+
syl (anr var_in_satisfying_exps2) @
614+
iand (subset_trans_var_lemma @ mp ,(function_sorting_full 1) function_lc_var) @
594615
anr ,(forall_extract $_ -> _$) @ univ_gene @
595616
anr ,(forall_extract $_ -> _ -> _$) @ univ_gene @
596617
anr ,(forall_extract $_ -> _ -> _ -> _$) @ univ_gene @
@@ -682,77 +703,70 @@ theorem subst_induction_var2: $ (lc_var Vars) C= satisfying_exps2 $ =
682703
a1i eq_refl));
683704

684705
theorem subst_induction_app2: $ (lc_app satisfying_exps2 satisfying_exps2) C= satisfying_exps2 $ =
685-
'(imp_to_subset _);
686-
687-
theorem subst_induction_app_lemma
688-
(a_var: $ is_sorted_func Var a $)
689-
(b_var: $ is_sorted_func Var b $)
690-
(plug1_exp: $ is_exp plug1 $)
691-
(plug2_exp: $ is_exp plug2 $):
692-
$ (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 $ =
693-
(named '(rsyl (anl an4) @ rsyl (anim2 @
694-
syl (curry eq_trans) @
695-
iand
696-
(rsyl anl @ eq_equiv_to_eq_eq ,(func_subst_explicit_helper 'z $_ @@ (eVar z) @@ _$))
697-
(rsyl anr @ eq_equiv_to_eq_eq ,(func_subst_explicit_helper 'z $_ @@ (eVar z)$))
698-
) @
699-
rsyl (anim1 @ iand id id) @
700-
rsyl (anl anass) @
701-
rsyl (anim2 @ anim1 @ syl (curry @ subst_app b_var plug2_exp) (anim
702-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
703-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
704-
)) @
705-
rsyl (anim2 @ curry eq_trans) @
706-
rsyl (anim1 @ iand id id) @
707-
rsyl (anl anass) @
708-
rsyl (anim2 @ anim1 @ syl ,(imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app a_var plug1_exp) @
709-
rsyl (anim2 @ curry eq_trans) @
710-
rsyl (anim1 @ iand id id) @
711-
rsyl (anl anass) @
712-
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
713-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
714-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
715-
)) @
716-
rsyl (anim2 @ impcom eq_trans) @
717-
rsyl (anim1 @ iand id id) @
718-
rsyl (anl anass) @
719-
rsyl (anim2 @ anim1 @ syl eq_sym @ syl ,(imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app b_var plug2_exp) @
720-
rsyl (anim2 @ impcom eq_trans) @
721-
anr));
722-
723-
theorem subst_induction_app (a b plug1 plug2: Pattern)
724-
(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 $):
725-
$ (lc_app (satisfying_exps a b plug1 plug2) (satisfying_exps a b plug1 plug2)) C= (satisfying_exps a b plug1 plug2) $ =
726-
(named '(imp_to_subset @
727-
rsyl (anl ,(ex_appCtx_subst 'appCtxLRVar)) @
706+
(named '(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
707+
syl (anr var_in_satisfying_exps2) @
708+
iand (subset_trans_var_lemma @ mp ,(function_sorting 2 'function_lc_app) satisfying_exps2_is_exp satisfying_exps2_is_exp) @
709+
anr ,(forall_extract $_ -> _$) @ univ_gene @
710+
anr ,(forall_extract $_ -> _ -> _$) @ univ_gene @
711+
anr ,(forall_extract $_ -> _ -> _ -> _$) @ univ_gene @
712+
anr ,(forall_extract $_ -> _ -> _ -> _ -> _$) @ univ_gene @
713+
rsyl (anl ,(membership_appCtx_subst 'appCtxLRVar)) @
714+
rsyl (exists_framing @ anim2 @ anl ,(membership_appCtx_subst 'appCtxRVar)) @
728715
exists_generalization_disjoint @
729-
rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @
716+
rsyl and_exists_disjoint_reverse @
730717
exists_generalization_disjoint @
731-
rsyl ,(appCtx_floor_commute_b_subst 'appCtxLRVar) @
732-
rsyl (anim1 @ iand id id) @
733-
rsyl (anl anass) @
734-
rsyl (anim2 @
735-
rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxLRVar)) @
736-
rsyl (anim2 ancom) @
737-
rsyl (anr anass) @
738-
rsyl (anim2 @
739-
rsyl ,(appCtx_floor_commute_b_subst 'appCtxRVar) @
740-
rsyl (anim1 @ iand id id) @
741-
rsyl (anl anass) @
742-
anim2 @
743-
rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxRVar)) @
744-
rsyl (anim2 ancom) @
745-
anr anass
746-
) @
747-
rsyl (anl anlass) @
748-
anim2 @
749-
anr anass) @
750718
rsyl (anr anass) @
751-
rsyl (anim2 @ anim1 lemma) @
752-
rsyl (anim2 @ ancom) @
753-
rsyl (anim1 @ curry @ mp ,(inst_foralls 2) function_lc_app) @
754-
curry ,(func_subst_alt_thm_sorted 'x $(eVar x) /\ ((app (app _ (app (app _ (eVar x)) _)) _) == (app (app _ (app (app _ (eVar x)) _)) _))$)
755-
));
719+
rsyl (iand anl @ iand anr anl) @
720+
rsyl (anim2 @ syl appl @ anim2 @ syl mem_func_lemma @ syl (exists_framing anr) @ syl (curry @ mp ,(inst_foralls 2) function_lc_app) @ anim (subset_trans_var_lemma satisfying_exps2_is_exp) (subset_trans_var_lemma satisfying_exps2_is_exp)) @
721+
impcom @
722+
mp ,(func_subst_imp_to_var 'y3 $bot -> bot -> bot -> bot -> bot -> bot -> ((bot @@ bot @@ (bot @@ bot @@ (eVar y3) @@ bot) @@ bot) == (bot @@ bot @@ (bot @@ bot @@ (eVar y3) @@ bot) @@ bot))$) @
723+
exp @ exp @ exp @ exp @ exp @
724+
sylc eq_trans (
725+
syl ,(imp_eq_framing_subst @ appCtx_constructor '[0 1]) @
726+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
727+
iand4 an4lr anllr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp)) @
728+
sylc eq_trans (
729+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
730+
iand4 an3lr anlr (syl (curry @ curry subst_sorting) @ iand3 an4lr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) anllr)
731+
(syl (curry @ curry subst_sorting) @ iand3 an4lr (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp) anllr)) @
732+
syl eq_sym @
733+
sylc eq_trans (
734+
syl ,(imp_eq_framing_subst @ appCtx_constructor '[0 1]) @
735+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
736+
iand4 an3lr anlr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp)) @
737+
sylc eq_trans (
738+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
739+
iand4 an4lr (syl (curry @ curry subst_sorting) @ iand3 an3lr anllr anlr) (syl (curry @ curry subst_sorting) @ iand3 an3lr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) anlr)
740+
(syl (curry @ curry subst_sorting) @ iand3 an3lr (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp) anlr)) @
741+
syl (curry eq_trans) @
742+
syl (anim ,(eq_framing_imp_subst 'appCtxLRVar) ,(eq_framing_imp_subst 'appCtxRVar)) @
743+
iand
744+
(curry @ curry @ curry @ curry @ curry @
745+
rsyl anl @
746+
rsyl (anl var_in_satisfying_exps2) @
747+
rsyl anr @
748+
rsyl var_subst_same_var @ imim2 @
749+
rsyl var_subst_same_var @ imim2 @
750+
rsyl var_subst_same_var @ imim2 @
751+
rsyl var_subst_same_var @ imim2 @
752+
imim2 eq_sym)
753+
(curry @ curry @ curry @ curry @ curry @
754+
rsyl anr @
755+
rsyl (anl var_in_satisfying_exps2) @
756+
rsyl anr @
757+
rsyl var_subst_same_var @ imim2 @
758+
rsyl var_subst_same_var @ imim2 @
759+
rsyl var_subst_same_var @ imim2 @
760+
rsyl var_subst_same_var @ imim2 @
761+
imim2 eq_sym)));
762+
763+
764+
theorem subst_induction_lam2: $ (lc_lam (abstraction Vars satisfying_exps2)) C= satisfying_exps2 $ =
765+
'(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
766+
syl (anr var_in_satisfying_exps2) @
767+
iand (subset_trans_var_lemma @ mp ,(function_sorting 1 'function_lc_lam) @ mp ,(function_sorting 2 '(function_abstraction Var_atom Exp_sort)) subset_refl satisfying_exps2_is_exp) @
768+
_);
769+
756770

757771
theorem subst_induction_lam_lemma (a b c plug1 plug2: Pattern)
758772
(diff_atoms_ab: $ a != b $)
@@ -823,7 +837,7 @@ theorem subst_induction_lemma:
823837
satisfying_exps2_is_exp
824838
EV_set
825839
subst_induction_var2
826-
_
840+
subst_induction_app2
827841
_);
828842

829843
do {

0 commit comments

Comments
 (0)