Skip to content

Commit e508558

Browse files
MirceaSMirceaS
committed
cleanup
1 parent 1b3782b commit e508558

File tree

2 files changed

+11
-165
lines changed

2 files changed

+11
-165
lines changed

‎nominal/core.mm1‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,13 @@ axiom pred_freshness:
4444
$ is_nominal_sort tau $ >
4545
$ ,(is_multi_function '(sym freshness_sym) '[alpha] 'tau) $;
4646

47-
47+
axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
48+
$ is_atom_sort alpha $ >
49+
$ is_nominal_sort tau $ >
50+
$ is_of_sort phi alpha $ >
51+
$ is_of_sort psi tau $ >
52+
$ s_forall alpha a (s_forall alpha b ((swap a b (abstraction phi psi)) == abstraction (swap a b phi) (swap a b psi))) $;
53+
4854

4955
axiom EV_pred (alpha tau: Pattern):
5056
$ is_atom_sort alpha $ >

‎nominal/lambda.mm1‎

Lines changed: 4 additions & 164 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,8 @@ axiom function_lc_app: $ ,(is_function '(sym lc_var_app) '[Exp Exp] 'Exp) $;
2121
term lc_lam_sym: Symbol;
2222
def lc_lam (phi: Pattern): Pattern = $ (sym lc_lam_sym) @@ phi $;
2323
axiom function_lc_lam: $ ,(is_function '(sym lc_lam_sym) '[(sort_abstraction Var Exp)] 'Exp) $;
24-
axiom EV_lc_lam (phi: Pattern) {a b: EVar}:
24+
axiom EV_lc_lam {a b: EVar} (phi: Pattern a b):
25+
$ is_of_sort phi (sort_abstraction Var Exp) $ >
2526
$ s_forall Var a (s_forall Var b ((swap a b (lc_lam phi)) == lc_lam (swap a b phi))) $;
2627

2728
axiom no_junk {X: SVar}:
@@ -53,7 +54,8 @@ theorem lc_lemma_1 {x: EVar} (exp_pred exp_suff_fresh: Pattern)
5354
theorem lc_lemma_2 {x y: EVar} (exp_pred: Pattern)
5455
(ev_unquant: $ (is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var) -> ((swap x y exp_pred) == exp_pred) $):
5556
$ (((is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var)) /\ ((lc_lam (abstraction (eVar y) exp_pred)) C= exp_pred)) -> ((lc_lam (abstraction (eVar x) exp_pred)) C= exp_pred) $ =
56-
'();
57+
'(rsyl (anim2 ,(subset_imp_subset_framing_subst 'appCtxRVar)) @
58+
_);
5759

5860
theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
5961
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
@@ -68,7 +70,6 @@ theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
6870
rsyl (anr anass) @
6971
lc_lemma_2 @ exp_pred_ev_unquantified exp_pred_ev));
7072

71-
7273
theorem freshness_irrelevance (exp_pred exp_suff_fresh: Pattern)
7374
(exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
7475
(exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
@@ -93,164 +94,3 @@ theorem prototype_induction_principle (exp_pred exp_suff_fresh: Pattern)
9394
(h_app: $ (lc_app exp_pred exp_pred) C= exp_pred $)
9495
(h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
9596
$ Exps == exp_pred $ = '();
96-
97-
98-
99-
do {
100-
(def disjoints (atom-map! '[Var #t] '[Exp #t] '[pred #t] '[freshness_arg #t]))
101-
};
102-
103-
theorem positive_in_no_junk {X: SVar}:
104-
$ _Positive X (lc_var (dom Var) \/ lc_app (sVar X) (sVar X) \/ lc_lam (abstraction (dom Var) (sVar X))) $ =
105-
'(positive_in_or (positive_in_or positive_disjoint @ positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_in_same_sVar) @ positive_in_app positive_disjoint @ positive_in_app positive_disjoint positive_in_same_sVar);
106-
107-
theorem predicate_lemma (pred freshness_arg: Pattern) {x y: EVar}
108-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg))$):
109-
$ (pred @@ eVar y @@ freshness_arg) == |^ pred @@ eVar y @@ freshness_arg ^| $ =
110-
'(anl ceil_idempotency_for_pred @ norm ,(propag_e_subst_adv 'z $((app (app pred (eVar z)) freshness_arg) == bot) \/ ((app (app pred (eVar z)) freshness_arg) == top)$ disjoints) @ var_subst predicate);
111-
theorem predicate_lemma_same_var (pred freshness_arg: Pattern) {x: EVar}
112-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg))$):
113-
$ (pred @@ eVar x @@ freshness_arg) == |^ pred @@ eVar x @@ freshness_arg ^| $ =
114-
'(anl ceil_idempotency_for_pred @ var_subst_same_var predicate);
115-
116-
117-
theorem induction_lemma_var (pred freshness_arg: Pattern)
118-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg)) $)
119-
(h_var: $ s_forall Var a (pred @@ (lc_var (eVar a)) @@ freshness_arg) $):
120-
$ (lc_var (dom Var)) -> s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg)) $ =
121-
(named '(membership_elim_implicit @
122-
anr ,(propag_mem 'b $(sym lc_var_sym @@ (dom Var)) -> exists z ((eVar z C= dom Exp) /\ (eVar z /\ _))$) @
123-
syl (exists_framing @ anl anlass) @
124-
syl (exists_framing @ anim1 eq_sym) @
125-
syl (anr @ mp ,(func_to_and_ctx_bi 'z $(eVar z C= dom Exp) /\ x in (pred @@ eVar z @@ freshness_arg)$) functional_var) @
126-
exists_generalization_disjoint @
127-
rsyl (anim1 eVar_in_subset_forward) @
128-
rsyl (anim1 @ iand id @ var_subst_same_var h_var) @
129-
rsyl (anl anrass) @
130-
syl (anim2 @ anl @ bitr (bitr (eq_to_intro_bi @ predicate_lemma predicate) (bicom mem_def)) (cong_of_equiv_mem @ eq_to_intro_rev_bi @ predicate_lemma predicate)) @
131-
iand (anwl @ rsyl ancom (rsyl (anim eVar_in_subset_forward ,(lemma_14_subset_subst 'id 'appCtxRVar)) @ rsyl (curry subset_trans) @ com12 subset_trans @
132-
lemma_46_floor @ syl (eq_to_intro_rev no_junk) @ syl (pre_fixpoint positive_in_no_junk) @ norm (norm_sym @ norm_imp_r @ _sSubst_or (_sSubst_or sSubstitution_disjoint norm_refl) norm_refl) @ orld orl
133-
)) @
134-
curry @ curry @
135-
rsyl (var_subst_same_var function_lc_var) @
136-
rsyl (exists_framing anr) @
137-
exists_generalization_disjoint @
138-
rsyl eq_sym @
139-
mp ,(func_subst_imp_to_var 'y $x in eVar y -> (pred @@ eVar y @@ freshness_arg) -> (pred @@ eVar x @@ freshness_arg)$) @
140-
rsyl membership_var_forward @
141-
rsyl ,(func_subst_explicit_helper 'y $pred @@ eVar y @@ freshness_arg$)
142-
anr
143-
));
144-
145-
theorem induction_lemma_app_lemma: $ lc_app (dom Exp) (dom Exp) C= dom Exp $ =
146-
(named '(lemma_46_floor @ syl (eq_to_intro_rev no_junk) @ syl (pre_fixpoint positive_in_no_junk) @ norm (norm_sym @ norm_imp_r ,(propag_s_subst_adv 'X $ ((sym lc_var_sym @@ (sym domain_sym @@ Var))) \/ (sym lc_app_sym @@ (sVar X) @@ (sVar X)) \/ (sym lc_lam_sym @@ (sym abstraction_sym @@ (sym domain_sym @@ Var) @@ (sVar X))) $ disjoints)) @
147-
syl (orld orr) @ rsyl ,(framing_subst '(eq_to_intro no_junk) 'appCtxLRVar) ,(framing_subst '(eq_to_intro no_junk) 'appCtxRVar)));
148-
149-
theorem induction_lemma_app (pred freshness_arg: Pattern)
150-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg)) $)
151-
(h_app: $ s_forall Exp t1 (s_forall Exp t2 ((pred @@ eVar t1 @@ freshness_arg) /\ (pred @@ eVar t2 @@ freshness_arg) -> (pred @@ (lc_app (eVar t1) (eVar t2)) @@ freshness_arg))) $):
152-
$ (lc_app (s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg)))
153-
(s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg)))
154-
) -> s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg)) $ =
155-
(named '(rsyl ,(framing_subst '(anl alpha_exists_disjoint) 'appCtxLRVar)
156-
@ rsyl ,(framing_subst '(anl alpha_exists_disjoint) 'appCtxRVar)
157-
@ norm (norm_sym @ norm_imp_l @ norm_app (norm_app_r @ norm_exists ,(propag_e_subst_adv 'z $ (eVar z C= app (sym domain_sym) Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$ disjoints)) @ norm_exists ,(propag_e_subst_adv 'z $ (eVar z C= app (sym domain_sym) Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$ disjoints))
158-
@ rsyl (anl ,(ex_appCtx_subst 'appCtxLRVar))
159-
@ exists_generalization_disjoint
160-
@ rsyl (anl ,(ex_appCtx_subst 'appCtxRVar))
161-
@ exists_generalization_disjoint
162-
@ rsyl ,(appCtx_floor_commute_b_subst 'appCtxLRVar)
163-
@ rsyl (anim2 ,(appCtx_floor_commute_b_subst 'appCtxRVar))
164-
@ rsyl (anr anass)
165-
@ rsyl (anim1 @ anr anidm)
166-
@ rsyl (anl anass)
167-
@ rsyl (anim2
168-
@ rsyl (anim2
169-
@ rsyl ,(framing_subst 'ancom 'appCtxLRVar)
170-
@ rsyl ,(framing_subst '(anim1 @ eq_to_intro @ predicate_lemma predicate) 'appCtxLRVar)
171-
@ rsyl ,(appCtx_ceil_commute_b_subst 'appCtxLRVar)
172-
@ rsyl (anim1 @ eq_to_intro_rev @ predicate_lemma predicate)
173-
@ rsyl (anim2
174-
@ rsyl ,(framing_subst 'ancom 'appCtxRVar)
175-
@ rsyl ,(framing_subst '(anim1 @ eq_to_intro @ predicate_lemma predicate) 'appCtxRVar)
176-
@ rsyl ,(appCtx_ceil_commute_b_subst 'appCtxRVar)
177-
@ anim1 @ eq_to_intro_rev @ predicate_lemma predicate)
178-
@ anr anass
179-
)
180-
@ rsyl (anr anass)
181-
@ rsyl (anim1 @ curry @ curry @ syl var_subst_same_var @ var_subst_same_var h_app)
182-
ancom
183-
)
184-
@ rsyl (anim1 @ anr anidm)
185-
@ rsyl (anl anass)
186-
@ rsyl (anim2 @ anim1 @ rsyl (anim ,(subset_imp_subset_framing_subst 'appCtxLRVar) ,(subset_imp_subset_framing_subst 'appCtxRVar)) @ curry subset_trans)
187-
@ rsyl (anim2 @ anim1 @ com12 subset_trans induction_lemma_app_lemma)
188-
@ rsyl (anim1 @ curry @ syl var_subst_same_var @ var_subst_same_var function_lc_app)
189-
@ curry
190-
@ syl (anr imp_exists_disjoint)
191-
@ exists_framing
192-
@ rsyl anr
193-
@ syl anr ,(func_subst_explicit_helper 'z $(eVar z C= dom Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$)));
194-
195-
theorem induction_lemma_abs (pred freshness_arg: Pattern)
196-
(freshness_arg_Exp: $ is_of_sort freshness_arg Exp $)
197-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg)) $)
198-
(h_abs: $ s_forall Var a (s_forall Exp t ((fresh_in_all a freshness_arg) -> (pred @@ eVar t @@ freshness_arg) -> (pred @@ (lc_lam (abstraction (eVar a) (eVar t))) @@ freshness_arg))) $):
199-
$ (lc_lam (abstraction (dom Var) (s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg))))
200-
) -> s_exists Exp x (eVar x /\ (pred @@ eVar x @@ freshness_arg)) $ =
201-
'(rsyl ,(framing_subst (framing_subst '(anl alpha_exists_disjoint) 'appCtxRVar) 'appCtxRVar)
202-
@ norm (norm_sym @ norm_imp_l @ norm_app_r (norm_app_r @ norm_exists ,(propag_e_subst_adv 'z $ (eVar z C= app (sym domain_sym) Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$ disjoints)))
203-
@ rsyl ,(framing_subst '(anl ,(ex_appCtx_subst 'appCtxRVar)) 'appCtxRVar)
204-
@ rsyl (anl ,(ex_appCtx_subst 'appCtxRVar))
205-
@ exists_generalization_disjoint
206-
@ rsyl ,(framing_subst ,(appCtx_floor_commute_b_subst 'appCtxRVar) 'appCtxRVar)
207-
@ rsyl ,(appCtx_floor_commute_b_subst 'appCtxRVar)
208-
@ rsyl (anim2 ,(framing_subst (framing_subst '(anim2 @ eq_to_intro @ predicate_lemma predicate) 'appCtxRVar) 'appCtxRVar))
209-
@ rsyl (anim2 ,(framing_subst (appCtx_ceil_commute_subst 'appCtxRVar) 'appCtxRVar))
210-
@ rsyl (anim2 ,(appCtx_ceil_commute_subst 'appCtxRVar))
211-
@ rsyl (anim2 ancom)
212-
@ rsyl (anr anass)
213-
@ rsyl (anim1 @ anim2 @ eq_to_intro_rev @ predicate_lemma predicate)
214-
@ rsyl (anim2 @ anl ,(appCtx_pointwise_subst '(norm_trans appCtxR_disjoint @ norm_app_r appCtxLRVar)))
215-
@ rsyl and_exists_disjoint_reverse
216-
@ exists_generalization_disjoint
217-
@ rsyl (anim2 @ anim2 eVar_in_subset_forward)
218-
@ rsyl (anim2 ancom)
219-
@ rsyl (anl anlass)
220-
@ rsyl (anr anass)
221-
@ rsyl (anim1 @ anr anass)
222-
@ rsyl (anim1 @ iand anl id)
223-
@ rsyl (anl anass)
224-
@ rsyl (anim2 @ anim1 @ curry @ curry @ exp @ com23 @ curry @ syl var_subst_same_var @ var_subst_same_var h_abs)
225-
-- @ rsyl (anim2 @ anim1 @ mpcom @ _)
226-
-- @ rsyl (anim2 @ anim1 @ curry @ syl (rsyl (exists_framing imancom) (anr imp_exists_disjoint)) @ anr imp_exists_disjoint @ exists_framing imancom @ exists_framing (iand id @ curry (com23 @ syl var_subst_same_var @ var_subst_same_var h_abs)) (F4 Var_atom Exp_sort freshness_arg_Exp))
227-
-- @ rsyl (anim2 @ anim1 @ exists_framing @ anim1 anl)
228-
-- @ syl (curry @ syl anr ,(func_subst_explicit_helper 'z $(eVar z C= dom Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$))
229-
230-
_);
231-
232-
theorem induction_principle (pred freshness_arg: Pattern)
233-
(freshness_arg_Exp: $ is_of_sort freshness_arg Exp $)
234-
(predicate: $ forall x (is_pred (pred @@ eVar x @@ freshness_arg)) $)
235-
(h_var: $ s_forall Var a (pred @@ lc_var (eVar a) @@ freshness_arg) $)
236-
(h_app: $ s_forall Exp t1 (s_forall Exp t2 ((pred @@ eVar t1 @@ freshness_arg) /\ (pred @@ eVar t2 @@ freshness_arg) -> (pred @@ (lc_app (eVar t1) (eVar t2)) @@ freshness_arg))) $)
237-
(h_abs: $ s_forall Var a (s_forall Exp t ((fresh_in_all a freshness_arg) -> (pred @@ eVar t @@ freshness_arg) -> (pred @@ (lc_lam (abstraction (eVar a) (eVar t))) @@ freshness_arg))) $):
238-
$ s_forall Exp t (pred @@ eVar t @@ freshness_arg) $ = (named
239-
'(univ_gene @
240-
rsyl eVar_in_subset_reverse @
241-
rsyl (anl ,(propag_mem 't $(dom Exp) -> exists tt ((eVar tt C= dom Exp) /\ (eVar tt /\ _))$) (membership_intro_implicit @
242-
rsyl (eq_to_intro no_junk) @ KT positive_in_no_junk (norm (norm_sym @ norm_imp_l
243-
,(propag_s_subst_adv 'X $((sym lc_var_sym) @@ ((sym (dom_sym)) @@ Var)) \/ ((sym lc_app_sym) @@ (sVar X) @@ (sVar X)) \/ ((sym lc_lam_sym) @@ ((sym abstraction_sym) @@ ((sym (dom_sym)) @@ Var) @@ (sVar X)))$ disjoints)
244-
) @
245-
eori (eori (induction_lemma_var predicate h_var) (induction_lemma_app predicate h_app)) (induction_lemma_abs freshness_arg_Exp predicate h_abs))
246-
)) @
247-
rsyl (anl @ cong_of_equiv_exists @ cong_of_equiv_and_r @ cong_of_equiv_and_r @ bitr
248-
(cong_of_equiv_mem (eq_to_intro_bi @ predicate_lemma_same_var predicate))
249-
mem_def) @
250-
exists_generalization_disjoint @
251-
syl (eq_to_intro_rev @ predicate_lemma predicate) @
252-
curry @
253-
a1i @
254-
curry @
255-
syl anr ,(func_subst_explicit_helper 'x $|^ pred @@ eVar x @@ freshness_arg ^|$)
256-
));

0 commit comments

Comments
 (0)