Alphabet generalisation

[MirceaS]

Generalised the theorems in the Theory of Words so that they don't only work for the original binary "a" and "b" alphabet.
They now work for arbitrary alphabets described by the pattern top_letter.
Also wrote python script generating theory files for simple alphabets made up of named letters.

[MirceaS]

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.

[nishantjr]

This PR does some great work. Here are some of the things I like about it:

• It introduces some nice infrastructure for dealing with functional patterns
• It proves some theorems that will generalize nicely outside of the theory of words, such as to contextual implication over functional contexts.

These are issues I see:

• There are a lot of generated theorems. This means that we are doing proof
  generation in three different languages (LISP, Maude and Python). I think
  that this will quickly become hard to maintain, unless done in a principled
  manner.
• Since our goal here is to build up a library of matching logic theorems, we
  should focus on modularity and re-usability, so that other people can easily
  re-use our library of theorems for there use cases.
• der_l1_l2_phi, der_l1_l2_phi_and and regex_eq_der_diff_l look like
  pretty much the same theorem?

Here is my proposal to get this functionality merged.

1. Theorems relating to constructors/functional patterns:

   • In an mm0 file, define notation for constructors/functional patterns,
   • Generalize theorems relevant theorems here. Assuming functional contexts, examples are:
     • cong_of_equiv_der ==> cong_of_equiv_ctximp
     • regex_eq_der_exists ==> propag_exists_ctximp
     • regex_eq_der_bot ==> propag_bot_ctximp
     • regex_eq_der_choice ==> propag_or_ctximp
     • regex_eq_der_conj ==> propag_and_ctximp
     • regex_eq_der_neg ==> propag_neg_ctximp
   • I think a lot of these are usable in the theory of separation logic as well.

2. I feel that the most readable and accessible way to define languages over arbitrary alphabets is
   as a series of nesting dolls.
   The theory for n letters, is defined as an extension to that with n-1 letters:
   Each alphabet, alphabet N is a sort with larger alphabets supersorts of smaller ones.
   In fact, we can define this theory in metamath without any python generation, the only caveat it that
   we the domain-words axiom cannot be easily defined.
   In any case, it may make sense to move towards the traditional sort infrastructure,
   and introduce sorted negation to deal with this.

   I propose using the attached formalization or similar.
   countable-words.txt

[nishantjr]

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.

[MirceaS]

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?

[nishantjr]

Why not simplify the theorem to $ derivative l1 (l2 . phi)) <-> (l1 == l2) /\ phi $ by adding a second hypothesis for l2? Also, h1 could probably be h1: $l1 -> top_letter, which is a more standard way of saying "l1 is of sort letter". The theorem then becomes:

theorem der_l1_l2_phi_and (l1 l2 phi: Pattern)
  (l1_func: $ is_func l1 $)
  (l2_func: $ is_func l2 $)
  (h1: $ l1 -> top_letter $)
  (h2: $ l2 -> top_letter $):
$derivative l1 (l2 . phi)) <-> (l1 == l2) /\ phi$

which is much easier to understand.

[MirceaS]

that's the signature of der_l1_l2_phi (see discussion above).
Also I changed most of the occurences to use that notation instead

[MirceaS]

• der_l1_l2_phi, der_l1_l2_phi_and and regex_eq_der_diff_l look like
  pretty much the same theorem?

der_l1_l2_phi came first and was the main lemma used for regex_eq_der_diff_l (which needs to exist beacuse it's one of the theorems referenced in the proof generation). When generalising the theorem I noticed that der_l1_l2_phi was not general enough so I instead had to prove and use der_l1_l2_phi_and, which is a bit more convoluted.
While we could now prove der_l1_l2_phi from der_l1_l2_phi_and fairly easily, I chose to keep the original proof of der_l1_l2_phi just in case someone ever wants to actually read it to understand how it works (since the proof of der_l1_l2_phi_and is strictly more complex) and because there's virtually no downside to keeping both proofs.

Also I expect der_l1_l2_phi to be quite useful and straightforward in most cases. der_l1_l2_phi_and exists for degenerate cases like the one I had to deal with.

Also I like the proposal to generalise our theorems to arbitrary contextual implications. I'm not atm convinced that they all can be generalised but it would be nice. However idk if it should necessarely be part of this PR specifically. That's another pretty large piece of work and ti would be useful to ahve this merged in.