Greetings, Due to some real life events, I had to step away from metamath last year. First, I want to apologize for ghosting the community on the last couple of pull requests I made in 2022. I hope you can forgive me for that.
I would like to get involved again. When I stepped away, I was working on some material related to formal languages. Some modifications to the existing Word theorems would make that easier. In particular, some theorems that mention two words in their antecedents require that both words be over the same alphabet, but the proofs work even if they are not. That is, these theorems only require that certain objects be words, and the alphabets in question do not affect the proof. This matters when trying to prove theorems about, for example, a language composed of words with prefixes from language 1 and suffixes from language 2, where the two languages are not necessarily over the same alphabet. Unions can be used; e.g., if I have W e. Word S and X e. Word T, then the existing theorems can be used by specifying that both words are elements of ( S u. T ). That works, but it irks me that I have to do extra work because the theorems unnecessarily constrain the alphabets. Would the community object if I start removing the same-alphabet constraints where they are not necessary? I have opened a pull request for the first such theorem, eqwrd: https://github.com/metamath/set.mm/pull/3731. The change to eqwrd requires changes to the proofs of several other theorems. Mostly, the effect is to add a byte or two and a step or two, due to the additional class variable. To counteract that, I inspected each proof for opportunities to shave off a few bytes here and there. These are the changes in size (in both bytes and steps) in the pull request. Theorem Bytes Steps -------------- ----- ----- eqwrd +0 +0 eqs1 -56 -57 swrdspsleq -1 -190 pfxeq -46 -440 pfxsuffeqwrdeq -54 -178 repswpfx -4 -136 2cshw -12 -290 pfx2 -535 -893 wwlktovf1 -70 -243 eqwrds3 -3 -1 wlkeq -76 -250 wwlkseq +2 +3 ---------------------------- Total: -855 -2675 The dramatic change in the size of pfx2 is because the new eqwrd enables replacing a proof that <" ( W ` 0 ) ( W ` 1 ) "> e. Word V with s2cli. Looking ahead, I foresee being able to remove antecedents from a few theorems after breaking a few more same-alphabet requirements. I hope such changes are a worthwhile use of reviewers' time. If not, please tell me. Wishing everybody a happy new year. Regards, -- Jerry James -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9c6b5d28-5be2-4bce-a6a5-76555dcd51a9n%40googlegroups.com.
