shorter proofs for some theorems in set.mm

[Igor Ieskov]

Hi all,

I found shorter proofs for some theorems in set.mm. They are listed in the attached file shorter-proofs.zip. There are 108 theorems, 47 in the main part of set.mm, the rest in mathboxes. Some of them are marked as OLD or "proof modification is discouraged", but I included such theorems into that file anyway. Since I am not sure how useful this result is and because of big number of theorems, I verified only the first 5 theorems by metamath.exe. I hope new shorter proofs for remaining theorems are also valid, but there is a chance that some of them are not.

Best regards,

Igor

[David A. Wheeler]

> On Feb 16, 2023, at 3:12 AM, Igor Ieskov <igori...@gmail.com> wrote:
>
> Hi all,
>
> I found shorter proofs for some theorems in set.mm. They are listed in the attached file shorter-proofs.zip. There are 108 theorems, 47 in the main part of set.mm, the rest in mathboxes. Some of them are marked as OLD or "proof modification is discouraged", but I included such theorems into that file anyway. Since I am not sure how useful this result is and because of big number of theorems, I verified only the first 5 theorems by metamath.exe. I hope new shorter proofs for remaining theorems are also valid, but there is a chance that some of them are not.

That's awesome!

Would you mind taking some steps so we can more easily review & add them?

We normally accept changes using git & GitHub. That process will automatically
check the validity of the proofs in a variety of ways. I suggest breaking your changes
into multiple changes, so that we can easily accept some while considering others.
If you don't know how, we can try to help!!

We generally don't change "proof modification is discouraged" so you'll need to justify
those changes (or drop them). I don't think we officially reject them for "OLD", but I
wouldn't focus your time on them.

--- David A. Wheeler

[Alexander van der Vekens]

We generally don't change "proof modification is discouraged" so you'll need to justify
those changes (or drop them). I don't think we officially reject them for "OLD", but I
wouldn't focus your time on them.

OLD theorems will be removed after one year, so shorten their proofs is useless.

[Igor Ieskov]

>  Would you mind taking some steps so we can more easily review & add them?

Sure. I've just created a pull request. I will gradually update proofs from the main part. I will not touch proofs from mathboxes.

Below I am providing a list of owners of mathboxes for which I found shorter proofs in order others not to download the file I attached (not sure if posting full names is a good idea):

AS

AV

GS
JB

NM

RP

TA

WL

-

Igor

[David A. Wheeler]

> On Feb 16, 2023, at 4:14 PM, Igor Ieskov <igori...@gmail.com> wrote:
>
> > Would you mind taking some steps so we can more easily review & add them?
>
> Sure. I've just created a pull request. I will gradually update proofs from the main part. I will not touch proofs from mathboxes.

I suggest creating multiple pull requests. That way we can easily accept some & not others.

> Below I am providing a list of owners of mathboxes for which I found shorter proofs in order others not to download the file I attached (not sure if posting full names is a good idea):
> AS
> AV
> GS
> JB
> NM
> RP
> TA
> WL

That's fine, we know who they are. To be fair,
their public names are a terribly-kept secret, since they're posted in
<https://us.metamath.org/metamath/set.mm>.
If someone doesn't want to give their real name they can just give their
pseudonym (e.g., Mel L. O'Cat, Drahflow) or abbreviation (KP, ML),
though real names are great because I expect this database to outlive all of us.

--- David A. Wheeler

[Benoit]

I saw in the zip file a shortening for 19.41v which was strange since the label parts of the compress proofs  were identical. Upon inspection, it appears that the proof in set.mm was not compressed: I did

  MM> sh pr 19.41v/c

and obtain you proof.

Every submission should follow https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md which was not the case for that proof.  I thought this was enforced but discovered it is not: in https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml#L123 you have only

  - run: cp set.mm set-wrapped.mm
  - run: scripts/rewrap set-wrapped.mm

  - run: echo 'Checking for set.mm rewrapping:' && diff -U 0 set.mm set-wrapped.mm

and https://github.com/metamath/set.mm/blob/develop/scripts/rewrap only does, as its name indicates, part of the job described in https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md.

I'll open an issue.  Ideally, we would do 'save proof */compressed' each time, but this takes time, so we can do 'save proof */compressed/fast' after one has done one initial sorrow 'save proof */compressed' and in principle it should be sufficient.

Benoît

[Benoit]

Well, it appears that https://github.com/metamath/set.mm/blob/develop/scripts/rewrap actually implements the job described in https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md. In particular, it uses "save proof */compressed/fast".

But in the help of metamath.c, I see that this does reformatting but not recompressing, so this expains that https://us.metamath.org/mpeuni/19.41v.html remained strangely compressed.

It's probably not worth it to remove the suffix "/fast" since the command is then rather slow.  I just made a PR which only does "MM> save proof */compressed" and it should be enough to run it once in a while. The file iset.mm was left unchanged and see the minimal diffs in the PR for set.mm. (https://github.com/metamath/set.mm/pull/3046)

Benoît

[Igor Ieskov]

Thierry asked (in my pull request):
> I suppose that it has been obtained automatically? It's not explained in the mail on the group, but I'd be interested to know the process. Especially, is that something we can run periodically like minimize, or even within the checks?

Yes, I obtained shorter proofs automatically and by accident. I was testing my program (see the reference below) by converting proofs back and forth between different forms (compressed and table) expecting that I have to get  an identical proof after all transformations if my program is correct. But it appeared that some proofs became longer and some shorter (while majority remained identical as expected, and two failed with an exception). I didn't have time to make sure what is the reason. That's why I have not mentioned this approach in my first email. But I am almost sure that the reason is as follows. My program always tries to reuse the first sub-proof for a statement. So, if a statement has two sub-proofs one longer and another shorter, the one which my program reads first will be reused instead of all other existing sub-proofs for that same statement.

It is possible to create a JavaScript program and run it periodically, after changing the program to always reuse the shortest sub-proof :) On my laptop it ran about 3 minutes for set.mm. Unfortunately I don't have time right now for this change, since I am spending all my free time for developing of my proof assistant (metamath-lamp). But I will return to it once I am done with the proof assistant.

The code I used to get shorter proofs - https://github.com/expln/metamath-lamp/blob/6a6cb4e23ce377406192bed25ffc83e1a4c46dcd/src/metamath/test/MM_save_proofs_to_files.res#L107 

-

Igor

[Thierry Arnoux]

Very clear, thank you Igor!
No need to make a tool right now, I just felt it was important to understand was was going on.