Same alphabet requirements in Word theorems

[Jerry James]

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

[David A. Wheeler]

> On Dec 31, 2023, at 7:32 PM, Jerry James <logan...@gmail.com> wrote:
>
> 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.

Welcome back!! I had the same problem in the latter part of 2023, where some personal challenges meant I was mostly unavailable & I'm only starting to be able to engage more.

We're grateful for whatever time you can apply.

> 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.\

We've often relaxed requirements on various theorems as they were found unnecessary (unless there was some special rationale, and I don't see one here). I think the same is true for this case. I'm glad you noticed this circumstance & look forward to your work!

I'll note that Gödel's Incompleteness Theorem is #6 in the Metamath 100 list <https://us.metamath.org/mm_100.html>. If you make it easier to do proofs related to formal languages, and add more theorems about it, your work might make it easier to complete that theorem.

> 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.

It looks great! I see several people already reviewed it, all liked it, and it's already been merged. So I think you have your answer :-).

This is exactly the process we like! Propose things incrementally so it's easier to review the change, tweak it where appopriate, merge, repeat. Thanks so much.

> Wishing everybody a happy new year. Regards,

You too!

--- David A. Wheeler

[Jerry James]

On Monday, January 1, 2024 at 4:16:59 PM UTC-7 David A. Wheeler wrote:

It looks great! I see several people already reviewed it, all liked it, and it's already been merged. So I think you have your answer :-).

This is exactly the process we like! Propose things incrementally so it's easier to review the change, tweak it where appopriate, merge, repeat. Thanks so much.

Well, PR #2 is going to be delayed a bit.  I am tackling ccatlen next.   It is used in more proofs than eqwrd, and I have a brand new time crunch that is going to keep me busy for about a week.  I'm about 3/4 of the way through fixing up consuming proofs, so hopefully I can have something to show early next week.

--

Jerry James

[Alexander van der Vekens]

I accepted already https://github.com/metamath/set.mm/pull/3731, and I think it is a good idea to generalize the theorems for Words requiring the same alphabet at the moment. So please go on ...