Mathbox

[GinoGiotto]

• Removed intemediate lemma dvelimfw. In ax-13-complete it's used only once and only by another of my lemmas.

• Corrections to the comments of cbval2vw and cbvex2vw.

• Added proof chain that leads to cbvmptvw, which is the most used additional theorem in ax-13-complete (it has 443 direct usages).

[tirix]

Theorem cbvmptv is a good example of a theorem that is used a lot.
I can guess adding one letter to the theorem name will shift a lot of compressed proofs.
Why not just make your version of cbvmptv the official one and set the current to "OLD" ?

[GinoGiotto]

Why not just make your version of cbvmptv the official one and set the current to "OLD" ?

It's fine with me. Actually it would probably be a lot easier to do it this way (and it would generate less amount of changes).

If you want, I can make a list of the most used additional lemmas and do the same for them (I have to check that it works before following this approach).

The only things we have to consider is that some of them might be used by other additional lemmas and that not all replacements are admitted. In ax-13-complete I verified that cbvmptvw is used by my other lemma frsucmpt2w (which is not in my mathbox yet). Also the original cbvmptv is left used by three theorems. So either I will have to add some dv conditions afterwards or I will have to add other lemmas in the same PR. I don't know how much this domino effect will propagate, but if it turns out to be a reasonable amount I wouldn't be against it (and it would still generate less amount of changes than the "classical" approach of adding lemmas and minimize).

Ok, with a quick look it seems doable. frsucmpt2w seems to be the only additional lemma using cbvmptvw. The original cbvmptv is left used by three theorems which are not used by anyone. The original frsucmpt2 has no uses and no additional lemma uses frsucmpt2w (so it's only used by theorems that don't require additional dv conditions). I cannot claim it works with full confidence until I try it, but at first glance it looks promising.

[GinoGiotto]

Update: on branch https://github.com/GinoGiotto/set.mm/tree/cbvmptv I posted this commit showing how the PR would look like (then I would also add the OLD version).

[avekens]

~cbvmptvw requires x and y to bis distinct, whereas ~cbvmptv does not. So only 3 of the 444 usages of ~cbvmptv do not depend on this detail, and therefore the replacement can be done without additial changes? Since the original ~cbvmptv is used and therefore is still required, it should not be declared as OLD (which would mean that it should be removed after a year), but renamed with a proper label.

[GinoGiotto]

So only 3 of the 444 usages of ~cbvmptv do not depend on this detail, and therefore the replacement can be done without additial changes?

The necessary changes to make the verifiers green are only these and rewrap.

Since the original ~cbvmptv is used and therefore is still required, it should not be declared as OLD (which would mean that it should be removed after a year), but renamed with a proper label.

It depends which way you want to see it.
If we add 6 dv conditions or so (like I did in the commit I mentioned) then you don't need the original ~cbvmptv at all. If you don't want to add 6 new dv, but you only want them to be added on ~cbvmptv then yes we have to keep the original version with a different name.

[tirix]

Are those DV which would be added "useless" ones, in the sense that they affect set variables which actually don't appear in the final theorem statement?
If so, they would be quite harmless to add.

[avekens]

After analysing the commit 6a865d0, I see no problems in changing the DV conditions of the theorems currently using ~ cbvmptv:

• ~rdgsucmpt2 uses both x and y in the hypotheses, but the purpose of this theorem is to keep these variables distinct, so they can be declared as distinct, too.
• ~frsucmpt2 same arguments as for ~rdgsucmpt2
• ~tendo0cbv, ~tendo02, ~tendo0cl: Norm's mathbox, so we unfortunately will not get feedback by the author. ~tendo0cbv seems to be unneccesary anyway, the statements and hypotheses of ~tendo02 and ~ tendo0cl only contain f, so g is actually only an auxiliary variable.
• 0ome: only the hypothesis contains one of the variables (x), so y is actually only an auxiliary variable.

Therefore, it will not be a problem to repace the current ~cbvmptv by ~cbvmptvw and mark the current ~cbvmptv as OLD.

[sctfn]

Can we keep it as an ALT instead so we can demonstrate how to do it without DVs?On Jan 17, 2024, at 10:20 AM, avekens ***@***.***> wrote: @avekens approved this pull request. After analysing the commit 6a865d0, I see no problems in changing the DV conditions of the theorems currently using ~ cbvmpt: ~rdgsucmpt2 uses both x and y in the hypotheses, but the purpose of this theorem is to keep these variables distinct, so they can be declared as distinct, too. ~frsucmpt2 same arguments as for ~rdgsucmpt2 ~tendo0cbv, ~tendo02, ~tendo0cl: Norm's mathbox, so we unfortunately will not get feedback by the author. ~tendo0cbv seems to be unneccesary anyway, the statements and hypotheses of ~tendo02 and ~ tendo0cl only contain f, so g is actually only an auxiliary variable. 0ome: only the hypothesis contains one of the variables (x), so y is actually only an auxiliary variable. Therefore, it will not be a probmel to repace the current ~cbvmptv by ~cbvmptvw and mark the current ~cbvmptv as OLD. —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[GinoGiotto]

Can we keep it as an ALT instead so we can demonstrate how to do it without DVs?

That's not an issue for me. Btw in the meantime I noticed that we can use the same trick for cbvmpt, which is currently used directly by 116 theorems, and it works for cbvmptf and cbvopab1 as well. All these together would require the addition of 8 dv conditions instead of 6.

On branch cbvmptv_2 I pushed the following commit 53d419b verifying that it passes all checks (I also removed a few unnecessary dv from cbvmpt).

I didn't read this message yet, so I put OLD proofs. I can change them to ALT if desired.

[tirix]

ALT works for me too!

[tirix]

@GinoGiotto Can I merge this, or would you prefer to first rework it?

[GinoGiotto]

@GinoGiotto Can I merge this, or would you prefer to first rework it?

Merge, I'll rework in the next PR.