search

Formal-Systems-Laboratory / matching-logic-mm0

Formalisation of Matching Logic in Metamath 0
BSD 3-Clause "New" or "Revised" License
0 stars 1 forks source link

Alphabet generalisation #28

Open MirceaS opened 1 year ago

MirceaS commented 1 year ago

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 commented 1 year ago
  • 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.