Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Alphabet generalisation #28

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
Open

Alphabet generalisation #28

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
37a40a5
generate mm0 file for given list of words
MirceaS Apr 7, 2023
e7ad592
simplified the script slightly
MirceaS Apr 7, 2023
a427b6e
generalised more theorems in 23... and developed mm1 generation part …
MirceaS Apr 11, 2023
ec18cd9
changed a variable name
MirceaS Apr 11, 2023
316404a
generalised more letter theorems
MirceaS Apr 11, 2023
4328c40
generalised derivative of different letters
MirceaS Apr 16, 2023
20795ea
generlaised fp_implies_regex_interior
MirceaS Apr 16, 2023
6cc1017
finished generalising all the theorems in the mm0 code
MirceaS Apr 21, 2023
65f8408
integrated theory generation for ab alphabet & fixed tests
MirceaS Apr 21, 2023
6d0d753
removed comment that is no longer accurate
MirceaS Apr 21, 2023
e5a4fe2
addressed PR comments
MirceaS Apr 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
634 changes: 317 additions & 317 deletions 01-propositional.mm1
View file
Open in desktop
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because of weird conflicts with the theory of words when running the tests I had to rename all a's in this file to aa and all b's to bb.
Feel free to rename them to whatever else if you don't like this.

Large diffs are not rendered by default.

4 changes: 0 additions & 4 deletions 02-ml-normalization.mm1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,8 +269,6 @@ do {

[$epsilon$ 'eSubstitution_disjoint]
[$top_letter$ 'eSubstitution_disjoint]
[$a$ 'eSubstitution_disjoint]
[$b$ 'eSubstitution_disjoint]
[$top_word ,Y$ 'eSubstitution_disjoint]
[$concat ,psi1 ,psi2$ '(_eSubst_concat ,(propag_e_subst_adv x psi1 wo_x) ,(propag_e_subst_adv x psi2 wo_x))]
[$nnimp ,phi1 ,phi2$ '(_eSubst_nnimp ,(propag_e_subst_adv x phi1 wo_x) ,(propag_e_subst_adv x phi2 wo_x))]
Expand Down Expand Up @@ -301,8 +299,6 @@ do {

[$epsilon$ 'sSubstitution_disjoint]
[$top_letter$ 'sSubstitution_disjoint]
[$a$ 'sSubstitution_disjoint]
[$b$ 'sSubstitution_disjoint]
[$concat ,psi1 ,psi2$ '(sSubst_concat ,(propag_s_subst_adv X psi1 wo_X) ,(propag_s_subst_adv X psi2 wo_X))]
[$top_word ,Y$ (if (== X Y) 'sSubstitution_in_same_mu 'sSubstitution_disjoint)]
[$kleene ,Y ,psi$ (if (== X Y)
Expand Down
5 changes: 5 additions & 0 deletions 10-theory-definedness.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ infixl _in: $in$ prec 35;

axiom definedness {x: EVar}: $ |^ eVar x ^| $;

--- Functional Patterns
-----------------------

def is_func {.x: EVar} (phi: Pattern): Pattern = $ exists x (eVar x == phi) $;
MirceaS marked this conversation as resolved.
Show resolved Hide resolved

--- Contextual Implications
---------------------------

Expand Down
43 changes: 27 additions & 16 deletions 12-proof-system-p.mm1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,12 @@ theorem propag_exists_def {x: EVar} (phi: Pattern x):
$ |^ exists x phi ^| -> exists x (|^ phi ^|) $ =
'(norm (norm_imp defNorm @ norm_exists defNorm) (! propag_exists_disjoint box));

theorem swap_exists {x y: EVar} (phi: Pattern x y): $ exists x (exists y phi) -> exists y (exists x phi) $ =
MirceaS marked this conversation as resolved.
Show resolved Hide resolved
'(exists_generalization (eFresh_exists eFresh_exists_same_var) @ exists_framing exists_intro_same_var);

theorem swap_exists_bi {x y: EVar} (phi: Pattern x y): $ exists x (exists y phi) <-> exists y (exists x phi) $ =
'(ibii swap_exists swap_exists);

theorem prop_43_bot (rho: Pattern): $ bot -> rho $ = 'absurdum;
theorem prop_43_or {box: SVar} (ctx: Pattern box) (phi1 phi2: Pattern):
$ (app[ phi1 / box ] ctx \/ app[ phi2 / box ] ctx) -> app[ phi1 \/ phi2 / box ] ctx $ =
Expand Down Expand Up @@ -253,8 +259,8 @@ theorem subset_to_eq: $ (phi C= psi) -> (psi C= phi) -> (phi == psi) $ = '(exp @

theorem eq_refl: $ phi == phi $ = '(equiv_to_eq biid);
theorem functional_same_var: $ exists x (eVar x == eVar x) $ = '(exists_intro_same_var eq_refl);
theorem functional_var: $ exists x (eVar x == eVar y) $ =
'(exists_intro @ norm (norm_sym @ _eSubst_eq eSubstitution_in_same_eVar eSubstitution_disjoint) eq_refl);
theorem functional_var: $ is_func (eVar x) $ =
(named '(exists_intro @ norm (norm_sym @ _eSubst_eq eSubstitution_in_same_eVar eSubstitution_disjoint) eq_refl));

theorem eq_sym: $ (phi1 == phi2) -> (phi2 == phi1) $ =
'(con3 @ framing_def @ con3 bicom);
Expand Down Expand Up @@ -764,6 +770,10 @@ theorem eq_to_forall_bi {x: EVar} (phi1 phi2: Pattern) (psi1 psi2: Pattern x)
$ (phi1 == phi2) -> ((forall x psi1) <-> (forall x psi2)) $ =
'(eq_to_not_bi @ eq_to_exists_bi @ eq_to_not_bi h);

theorem eq_to_func_bi
(h: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
MirceaS marked this conversation as resolved.
Show resolved Hide resolved
$ (phi1 == phi2) -> ((is_func psi1) <-> (is_func psi2)) $ = (named '(eq_to_exists_bi @ eq_to_eq_r_bi h));

theorem eq_to_mem_bi {x: EVar} (phi1 phi2 psi1 psi2: Pattern x)
(h: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
$ (phi1 == phi2) -> ((x in psi1) <-> (x in psi2)) $ =
Expand Down Expand Up @@ -968,6 +978,7 @@ do {
[$_subset ,phi1 ,phi2$ '(eq_to_subset_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
[$equiv ,phi1 ,phi2$ '(eq_to_equiv_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
[$_eq ,phi1 ,phi2$ '(eq_to_eq_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
[$is_func ,psi$ '(eq_to_func_bi ,(func_subst_explicit_helper x psi))]

[$nnimp ,phi1 ,phi2$ '(eq_to_nnimp_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper X phi2))]
[$concat ,phi1 ,phi2$ '(eq_to_concat_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))]
Expand Down Expand Up @@ -1003,31 +1014,31 @@ do {
exists_generalization ,fre (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) ,phi1_pf) ,func_phi2
))

(def (propag_mem x ctx) @ match ctx
(def (propag_mem_w_fun x ctx fun_patterns) @ if (not (== (lookup fun_patterns ctx) #undef)) (func_subst_thm (lookup fun_patterns ctx) 'y 'membership_var_bi) @ match ctx
-- special case for top and bottom?
[$eVar ,y$ (if (== x y) '(taut_equiv_top membership_same_var) 'membership_var_bi)]
[$exists ,y ,psi$ (if (== x y) 'biid '(bitr membership_exists_bi @ cong_of_equiv_exists ,(propag_mem x psi)))]
[$forall ,y ,psi$ (if (== x y) 'biid '(bitr membership_forall_bi @ cong_of_equiv_forall ,(propag_mem x psi)))]
[$exists ,y ,psi$ (if (== x y) 'biid '(bitr membership_exists_bi @ cong_of_equiv_exists ,(propag_mem_w_fun x psi fun_patterns)))]
[$forall ,y ,psi$ (if (== x y) 'biid '(bitr membership_forall_bi @ cong_of_equiv_forall ,(propag_mem_w_fun x psi fun_patterns)))]
[$_in ,y ,psi$ (if (== x y) 'lemma_in_in_same_var 'lemma_in_in)]
[$not ,psi$ '(bitr membership_not_bi @ cong_of_equiv_not ,(propag_mem x psi))]
[$imp ,phi1 ,phi2$ '(bitr membership_imp_bi @ cong_of_equiv_imp ,(propag_mem x phi1) ,(propag_mem x phi2))]
[$or ,phi1 ,phi2$ '(bitr membership_or_bi @ cong_of_equiv_or ,(propag_mem x phi1) ,(propag_mem x phi2))]
[$and ,phi1 ,phi2$ '(bitr membership_and_bi @ cong_of_equiv_and ,(propag_mem x phi1) ,(propag_mem x phi2))]
[$equiv ,phi1 ,phi2$ '(bitr membership_equiv_bi @ cong_of_equiv_equiv ,(propag_mem x phi1) ,(propag_mem x phi2))]
[$app ,phi1 ,phi2$ '(bitr membership_app @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem #undef phi2))]
[$not ,psi$ '(bitr membership_not_bi @ cong_of_equiv_not ,(propag_mem_w_fun x psi fun_patterns))]
[$imp ,phi1 ,phi2$ '(bitr membership_imp_bi @ cong_of_equiv_imp ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))]
[$or ,phi1 ,phi2$ '(bitr membership_or_bi @ cong_of_equiv_or ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))]
[$and ,phi1 ,phi2$ '(bitr membership_and_bi @ cong_of_equiv_and ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))]
[$equiv ,phi1 ,phi2$ '(bitr membership_equiv_bi @ cong_of_equiv_equiv ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))]
[$app ,phi1 ,phi2$ '(bitr membership_app @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem_w_fun #undef phi2 fun_patterns))]
[$_ceil ,psi$ 'mem_def]
[$_floor ,psi$ 'mem_floor]
[$_subset ,phi1 ,phi2$ 'mem_floor]
[$_eq ,phi1 ,phi2$ 'mem_floor]

-- [$nnimp ,phi1 ,phi2$ '(membership_nnimp ,(propag_mem x phi1) ,(propag_mem X phi2))]
[$a$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_a)]
[$b$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_b)]
[$epsilon$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_epsilon)]
[$concat ,phi1 ,phi2$ '(bitr membership_app2 @ cong_of_equiv_exists @ cong_of_equiv_and ,(propag_mem #undef phi1) @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem #undef phi2))]
-- [$nnimp ,phi1 ,phi2$ '(membership_nnimp ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun X phi2 fun_patterns))]
[$epsilon$ (func_subst_thm 'functional_epsilon 'y 'membership_var_bi)]
[$concat ,phi1 ,phi2$ '(bitr membership_app2 @ cong_of_equiv_exists @ cong_of_equiv_and ,(propag_mem_w_fun #undef phi1 fun_patterns) @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem_w_fun #undef phi2 fun_patterns))]

[_ 'biid]
)

(def (propag_mem x ctx) @ propag_mem_w_fun x ctx (atom-map!))
};

theorem func_subst_explicit_test_1 {x y: EVar} (phi: Pattern)
Expand Down
17 changes: 4 additions & 13 deletions 20-theory-words.mm0
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,5 @@
import "10-theory-definedness.mm0";

term a_symbol : Symbol ;
def a : Pattern = $sym a_symbol$ ;
term b_symbol : Symbol ;
def b : Pattern = $sym b_symbol$ ;

Comment on lines -3 to -7
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd like to keep a copy of the theory we used for the paper submission separate from the generated theorems for reference.
I think that that may be easier to understand than the generated files.
We can also have a 15-constructors.mm1 file with various lemmas regarding functional patterns etc. that are shared between them.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can have that in a separate branch, like submission.
Also I feel the generated files are super easy to understand, maybe I should commit them to the repo given that the maude code doesn't support arbitrary alphabets. Also what lemmas do you mean?

def emptyset : Pattern = $bot$ ;

term epsilon_symbol : Symbol ;
Expand All @@ -18,9 +13,8 @@ def kleene_l {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ sVar X .
def kleene_r {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ alpha . sVar X)$;
def kleene {X: SVar} (alpha: Pattern X) : Pattern = $(kleene_r X alpha)$;

--- We assume that the alphabet has only two letters.
--- This, however, captures the full expressivity.
def top_letter : Pattern = $a \/ b$;
term top_letter_symbol: Symbol;
def top_letter: Pattern = $sym top_letter_symbol$;

def top_word_l {X: SVar} : Pattern = $(kleene_l X top_letter )$ ;
def top_word_r {X: SVar} : Pattern = $(kleene_r X top_letter )$ ;
Expand All @@ -30,12 +24,9 @@ def top_word {X: SVar} : Pattern = $(kleene X top_letter )$ ;

axiom domain_words {X: SVar} : $ top_word X $;

axiom functional_epsilon {x : EVar} : $exists x (eVar x == epsilon)$;
axiom functional_a {x : EVar} : $exists x (eVar x == a)$;
axiom functional_b {x : EVar} : $exists x (eVar x == b)$;
axiom functional_concat {w v x: EVar} : $exists x (eVar x == (eVar w . eVar v))$;
axiom functional_epsilon : $ is_func epsilon $;
axiom functional_concat {w v: EVar} : $ is_func (eVar w . eVar v)$;

axiom no_confusion_ab_e : $a != b$;
axiom no_confusion_ae_e : $~(epsilon C= top_letter)$;
axiom no_confusion_ec_e {u v: EVar} : $(epsilon == eVar u . eVar v) -> (epsilon == eVar u) /\ (epsilon == eVar v)$;
axiom no_confusion_cc_e {u v x y: EVar} : $(x in top_letter) -> (y in top_letter)
Expand Down
7 changes: 3 additions & 4 deletions 21-words-helpers.mm1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,8 +134,7 @@ theorem cong_of_equiv_kleene {X: SVar} (phi1 phi2: Pattern X)

--- Helpers for top_letter
theorem positive_in_top_letter {X: SVar}:
$ _Positive X top_letter $ =
'(positive_in_or positive_disjoint positive_disjoint);
$ _Positive X top_letter $ = '(positive_disjoint);
theorem sSubst_top_letter {X: SVar} (psi: Pattern X):
$ Norm (s[ psi / X ] (top_letter)) (top_letter) $ = 'sSubstitution_disjoint;
theorem eSubst_top_letter {X: EVar} (psi: Pattern X):
Expand All @@ -145,7 +144,7 @@ theorem eSubst_top_letter {X: EVar} (psi: Pattern X):
--- TODO: Define in terms of kleene_l
theorem positive_in_top_word_l_body {X: SVar}: $_Positive X (epsilon \/ sVar X . top_letter)$ =
'(positive_in_or positive_disjoint @
positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_in_top_letter);
positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_disjoint);
MirceaS marked this conversation as resolved.
Show resolved Hide resolved
theorem kt_top_word_l {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $psi . top_letter -> psi$): $top_word_l X -> psi$ =
'(KT positive_in_top_word_l_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ sVar X . top_letter$) @ eori base rec);
theorem unfold_r_top_word_l {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ top_word_l X . top_letter$) : $phi -> top_word_l X$ =
Expand All @@ -155,7 +154,7 @@ theorem unfold_r_top_word_l {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ t
--- TODO: Define in terms of kleene_r
theorem positive_in_top_word_r_body {X: SVar}: $_Positive X (epsilon \/ top_letter . sVar X)$ =
'(positive_in_or positive_disjoint @
positive_in_app (positive_in_app positive_disjoint positive_in_top_letter) positive_in_same_sVar);
positive_in_app (positive_in_app positive_disjoint positive_disjoint) positive_in_same_sVar);
theorem kt_top_word_r {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $top_letter . psi -> psi$): $top_word_r X -> psi$ =
'(KT positive_in_top_word_r_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ top_letter . sVar X$) @ eori base rec);
theorem lemma_83_top_word_r_forward
Expand Down
Loading