Proposal for on-going proof minimization

[Norman Megill]

In the past, every year or two we would run "minimize_with" on the entire set.mm. But as set.mm has grown, doing this has become a somewhat large project. The last time was in Feb., which involved people volunteering their CPUs over several weeks as well as my time managing it.

Benoît suggested that we require proofs to be minimized before submission. This would make a global minimization a lower priority effort that we could do less frequently. (Benoît's suggestion was motivated by noticing a proof that was shortened manually in the same way that "minimize_with" would have done automatically, accompanied by a "Proof shortened by" credit and a *OLD version.)

However, I tried making it a requirement a decade or so ago without much success. Sometimes contributors would agree but sometimes forget to do it, and one person objected that it was too much effort. So while we would like contributors to minimize their proofs before submission, it's not something practical to expect or enforce.

I propose we add a temporary tag to recent set.mm proofs that lets us know whether or not "minimize_with" has been run. Volunteers can, at their leisure, minimize the proofs that haven't been.

Ideally we would have a tag or marker in the comment like "(Minimization pending.)", or maybe just "(*)" to minimize clutter, indicating that a proof hasn't been minimized. The volunteer would delete this marker after minimization. To start with, I would put the marker in every theorem added since Mar. 5, 2020 (when the last full minimization was run). Then we would expect all contributors to put this marker in future contributions, whenever they haven't minimized their submitted proofs.

A problem with this is that it is hard to enforce putting in a  "minimization pending" marker  in new theorems - people will simply forget to do it - and "verify markup" has no way of detecting whether or not a proof was really minimized.

So maybe we need two markers standing for "minimization pending" and "minimization done".  All "minimization done" markers would be deleted after a period of time like a year (we don't want them in set.mm permanently since they add no value). "verify markup" could then produce a warning for recent theorems (< 1 year old) that have neither marker.  This seems a little inelegant, but I couldn't think of another way that "verify markup" could recognize.

(Whatever we decide, I could add some automation in metamath.exe to update the marker when a proof is minimized.)

I'd like to hear opinions or suggestions.

Norm

[savask]

I agree that minimization markers "add no value", so in my opinion they should be kept out of set.mm altogether. Maybe we can create a file "minimized_theorems" (something like "discouraged") which will be a list of, well, minimized theorems :-) Contributors won't have to set any tags or modify that file, but if someone decides to minimize a theorem, they will check that file and in case if the theorem wasn't processed earlier they will minimize it and add the name to the file. That way we will avoid additional bureaucratic burden of contributing to set.mm.

The "minimize" command of metamath.exe can be made to skip minimization of theorems mentioned in the "minimized_theorems" file, so minimization volunteers will be able to minimize whole ranges of theorems in bulk, without doing double work.

And speaking of making users minimize their theorems, I think most people need only a small reminder. Right now, after you complete a proof in metamath.exe, the program will remind you to do "SAVE NEW_PROOF" and "VERIFY PROOF". Perhaps a suggestion to minimize the proof can be added there as well? Same goes for mmj2, after a proof is finished and mmj2 compiles it to the compressed proof format, one can add an automatic comment suggesting the user to run "minimize" in metamath.exe.

[Alexander van der Vekens]

I fully agree with Norm's demand that all theorems in set.mm (at least in the main body of set.mm!) should be minimized, but I am of the same opinion as @savask that tagging minimized/not minimized theorems as proposed by Norm is not practicable and would make set.mm more clumsy.

At least I would not be happy if I have to care for these tags in my Mathbox (or allowing others to perform minimizations in my Mathbox, although I always would welcome hints that there is a way to minimize a proof in my Mathbox). I think we should restrict our attention/efforts to main set.mm.

For my part, I always minimize new/modified theorems (unless I do not forget it unintentionally!) before I push them to the Git repository. Hints as suggested by @savask would be a (small) step to achieve more quality (with respect to minimization) and should be provided if this is possible with little effort. Regarding a list to be maintained I am a little bit sceptical if this was practical.

What about checking for not minimized proofs while checking a Pull Request? Of course a program/script has to be written for it. Such a programm/script could look for all new/modified theorems (in main set.mm, not being tagged with "(Proof modification is discouraged.)") and run "minimize_with" for them. If the result is always "No shorter proof was found", then the check is passed, otherwise the pull request should be rejected. By this, each contributor is responsible for providing minimized proofs only.

Alexander

[Alexander van der Vekens]

I am currently workin within my Mathbox, and I found a minimization of one of my poofs (using minimize_with) using a theorem of Benoît's Mathbox (@Benoît: it's bj-eleq2w - can I move it (together with bj-eleq1w?) to main set.mm? Where is the right place for them?).

This example shows that there is a flaw in the approaches we discussed so far: what about minimization if a new theorem is added to main set.mm which would allow for a minimization of following theorems which were minimized before? The global run of "minimize_with" on the entire set.mm would detect and process such cases, but neither the marking proposed by Norm nor the list proposed by @savask nor my proposal would handle such cases. Maybe the program/script of my proposal could be extended to check for proofs which could be minimized by the new/modified theorems (and gives a hint to the contributor which proofs to minimize before the pull request can be accepted)?  

[David A. Wheeler]

> On Dec 11, 2020, at 10:13 PM, Norman Megill <n...@alum.mit.edu> wrote:
>
> Benoît suggested that we require proofs to be minimized before submission.

I think we should encourage that. I think requiring is too strong, but simply making that request clear is reasonable enough.

> I propose we add a temporary tag to recent set.mm proofs that lets us know whether or not "minimize_with" has been run. Volunteers can, at their leisure, minimize the proofs that haven't been. .,..

> I'd like to hear opinions or suggestions.

I disagree. It does not really help. Minimization is often enabled by adding something *else* later, so such tags would be misleading. In addition, adding them would be a pain & create a lot of useless fluff.

> In the past, every year or two we would run "minimize_with" on the entire set.mm. But as set.mm has grown, doing this has become a somewhat large project.

To me the solution is clear: automation. When we started last time almost nothing was automated. I ended up writing some scripts to automate parts of it, but that was done on the fly *during* the minimization. Instead, let’s play on letting the computers do all the work. If it’s going to happen annually, then let’s treat it as something that automatically happens annually.

--- David A. Wheeler

[Benoit]

Since these things are hard to enforce, maybe we could make clear the following guidelines for contributors (e.g., in ~conventions and mmset.html):

- when adding theorems to Main (be it direct addition or moving from a mathbox) running MINIMIZE_WITH is required;

- when adding a theorem to one's mathbox, running MINIMIZE_WITH is strongly recommended,

- if for some reason, this is not possible, then you should add to its comment "(Minimization pending.)".

If minimization is not desirable, add the tag "(Proof modification is discouraged.)" preceded by a short explanation why this is so (or: which property of the proof should be kept).

Failure to do so will cause the spirit of Metamath to haunt you for seven years.

An idea for bulk minimization: let A be the set of all theorems of Main added/modified since the previous bulk minimization; then run "minimize_with *" on all theorems in A, and run "minimize_with A" on all other theorems in Main.

Alexander: I'm pleasantly surprised that ~bj-eleq2w allows a minimization (probably avoiding a use of ~cv, compared to ~eleq2 ?). Its main goal is to reduce axiom dependencies (actually, that section of my mathbox shows how dependency on ~ax-ext, among others, can be removed from several dozens theorems --- yes, ~ax-ext is used in the eliminability theorem, but this is still interesting).  If Norm agrees and you don't mind, I'll move it to Main, to its place, which is right after df-clel.  Side note: ~bj-eleq2w actually uses fewer axioms than ~eleq2, since the latter does "morally" use ax-5--9 and ax-ext, as bj-dfclel and bj-dfcleq show.

Benoît

[Alexander van der Vekens]

@Benoît: yes, please move both theorems ~bj-eleq1w and ~bj-eleq2w to main set.mm. I will shorten my proof afterwards. The following two lines

13 eleq2         $p |- ( e = c -> ( U e. e <-> U e. c ) )
14 13 cbvrabv    $p |- { e e. E | U e. e } = { c e. E | U e. c }

will be replaced by

13 bj-eleq2w     $p |- ( e = c -> ( U e. e <-> U e. c ) )

14 13 cbvrabv    $p |- { e e. E | U e. e } = { c e. E | U e. c }

The number of steps (all 139, essential 23) of the whole proof will not be decreased, but the number of bytes (especially if the prefix "bj-" is removed).

[Norman Megill]

 It looks like my proposal wouldn't be welcomed, so I will abandon it. As for keeping a list of minimized theorems, I'm not really in favor of that either; it would be one more thing to maintain that people will forget or neglect.

As for mathboxes, we've never had a rule about people minimizing proofs in other people's mathboxes, or even finding shorter proofs manually, adding credit and creating a *OLD for  the original (and still keeping everything in the mathbox). In the past we've done this often, and I always welcomed it. Indeed, there are well over 100 "(Proof shortened by [someone else]...)" tags currently in mathboxes. And if we add, say, a new variation of syl* in main that shortens 50 proofs, we typically apply it to all of them including ones in mathboxes, without consulting the mathbox owners.

What would be the reason someone would not want a proof in their mathbox minimized? I could see a few cases where the proof is still being worked on and minimization would create a merge conflict, but I think that is rare. Most people, once they have a proof (a minimum requirement for the PR checks to pass), go on to the next and only occasionally go back and revise the proof. If a mathbox user doesn't want a proof to be touched because it is still being modified, the tag "(Proof modification is discouraged.)" can be added temporarily until it is finished.

In any case, I strongly encourage people to minimize all proofs they submit, whether in their mathbox or not. An informal rule to minimize proofs when importing to main is nice, but it can't be enforced and I doubt it will always be followed.

On Saturday, December 12, 2020 at 3:42:36 AM UTC-5 Alexander van der Vekens wrote:

I am currently workin within my Mathbox, and I found a minimization of one of my poofs (using minimize_with) using a theorem of Benoît's Mathbox (@Benoît: it's bj-eleq2w - can I move it (together with bj-eleq1w?) to main set.mm? Where is the right place for them?).

 This shouldn't have happened. 'minimize_with' does not consider other mathboxes unless '/include_mathboxes' is specified. Is that what you used, or is this a bug I should investigate?

As for moving theorems out of mathboxes, we have often done that when a theorem is needed for another mathbox. Typically we simply move the theorem to main at an appropriate place (I use 'show trace_back' to help identify where it should best go) and add an entry to the list at the top of set.mm, but we don't necessarily notify the mathbox owner. Sometimes a name change is needed e.g. the "bj-" prefix would be removed or a new name is chosen that better conforms to our informal conventions; this is also documented in the same list entry at the top of set.mm.

BTW that fact that someone else's mathbox theorem shortens a proof isn't necessarily a good reason to move it to main. E.g. there are many trivial variants of existing propositional calculus theorems in some mathboxes that may, by coincidence, slightly shorten a proof elsewhere in set.mm, but that doesn't necessarily mean we should move it out of the mathbox if it doesn't "pay for itself" in terms of shortening many proofs.

 

This example shows that there is a flaw in the approaches we discussed so far: what about minimization if a new theorem is added to main set.mm which would allow for a minimization of following theorems which were minimized before? The global run of "minimize_with" on the entire set.mm would detect and process such cases, but neither the marking proposed by Norm nor the list proposed by @savask nor my proposal would handle such cases.

 I don't think this happens enough to be concerned with much. The global minimization will handle it, and in individual cases it can be dealt with manually. When proposing moving a new basic logic theorem to set.mm, most people will determine what proofs can be minimized with it as justification, and then will perform those minimizations.

Maybe the program/script of my proposal could be extended to check for proofs which could be minimized by the new/modified theorems (and gives a hint to the contributor which proofs to minimize before the pull request can be accepted)?

This isn't practical because for a very large proof, 'minimize_with' may take days to run.

Norm

[Alexander van der Vekens]

Sorry, but maybe my comments were more confusing than helpful for the discussion:

On Sunday, December 13, 2020 at 4:54:33 PM UTC+1 Norman Megill wrote:

 It looks like my proposal wouldn't be welcomed, so I will abandon it. As for keeping a list of minimized theorems, I'm not really in favor of that either; it would be one more thing to maintain that people will forget or neglect.

As for mathboxes, we've never had a rule about people minimizing proofs in other people's mathboxes, or even finding shorter proofs manually, adding credit and creating a *OLD for  the original (and still keeping everything in the mathbox). In the past we've done this often, and I always welcomed it. Indeed, there are well over 100 "(Proof shortened by [someone else]...)" tags currently in mathboxes. And if we add, say, a new variation of syl* in main that shortens 50 proofs, we typically apply it to all of them including ones in mathboxes, without consulting the mathbox owners.

What would be the reason someone would not want a proof in their mathbox minimized? I could see a few cases where the proof is still being worked on and minimization would create a merge conflict, but I think that is rare. Most people, once they have a proof (a minimum requirement for the PR checks to pass), go on to the next and only occasionally go back and revise the proof. If a mathbox user doesn't want a proof to be touched because it is still being modified, the tag "(Proof modification is discouraged.)" can be added temporarily until it is finished.

I did not (intend to) say that it should be forbidden to shorten proofs in other's mathboxes, especially by using "minimize-with". Manual shortenings in other's mathboxes should be marked by the *OLD convention, as described, but I don't duplicate theorems and mark one of them as OLD in my own mathbox, although I put the tag  "Proof shortened by[myself].." to the comment in such cases. I only was concerned about maintaining additional tags in my mathbox as initially proposed, but since the proposal is abandon, there is no problem anymore.

 

In any case, I strongly encourage people to minimize all proofs they submit, whether in their mathbox or not. An informal rule to minimize proofs when importing to main is nice, but it can't be enforced and I doubt it will always be followed.

 

I fully agree.

On Saturday, December 12, 2020 at 3:42:36 AM UTC-5 Alexander van der Vekens wrote:

I am currently workin within my Mathbox, and I found a minimization of one of my poofs (using minimize_with) using a theorem of Benoît's Mathbox (@Benoît: it's bj-eleq2w - can I move it (together with bj-eleq1w?) to main set.mm? Where is the right place for them?).

 This shouldn't have happened. 'minimize_with' does not consider other mathboxes unless '/include_mathboxes' is specified. Is that what you used, or is this a bug I should investigate?

 

Yes, I used  '/include_mathboxes' intentionally.

As for moving theorems out of  mathboxes, we have often done that when a theorem is needed for another mathbox. Typically we simply move the theorem to main at an appropriate place (I use 'show trace_back' to help identify where it should best go) and add an entry to the list at the top of set.mm, but we don't necessarily notify the mathbox owner. Sometimes a name change is needed e.g. the "bj-" prefix would be removed or a new name is chosen that better conforms to our informal conventions; this is also documented in the same list entry at the top of set.mm.

 

Usually, I  move theorems I use in my mathbox to main set.mm by myself, exactly as described. Benoît's therorems are a little bit special, so I wanted to ask him for the right way/place where to move them.

BTW that fact that someone else's mathbox theorem shortens a proof isn't necessarily a good reason to move it to main. E.g. there are many trivial variants of existing propositional calculus theorems in some mathboxes that may, by coincidence, slightly shorten a proof elsewhere in set.mm, but that doesn't necessarily mean we should move it out of the mathbox if it doesn't "pay for itself" in terms of shortening many proofs.

Besides  Benoît's therorem(s), there where two theorems of Glauco's mathbox which shortened my proofs. I moved one of them (~ffnd) to main set.mm, because I think it is meaningful/helpul (deduction version of already existing ~ffn). The second one (~fnvinran ) I did not move, because it was exactly the same as an existing theorem (~ ffvelrnda ), having a shorter label only.

 

This example shows that there is a flaw in the approaches we discussed so far: what about minimization if a new theorem is added to main set.mm which would allow for a minimization of following theorems which were minimized before? The global run of "minimize_with" on the entire set.mm would detect and process such cases, but neither the marking proposed by Norm nor the list proposed by @savask nor my proposal would handle such cases.

 I don't think this happens enough to be concerned with much. The global minimization will handle it, and in individual cases it can be dealt with manually. When proposing moving a new basic logic theorem to set.mm, most people will determine what proofs can be minimized with it as justification, and then will perform those minimizations.

 

If we continue to perform global minimizations, there is no problem. My only concern were theorems being marked as "minimized" which are not minimized (anymore).

Maybe the program/script of my proposal could be extended to check for proofs which could be minimized by the new/modified theorems (and gives a hint to the contributor which proofs to minimize before the pull request can be accepted)?

This isn't practical because for a very large proof, 'minimize_with' may take days to run.

 

Yes, I see - large proof would cause problems. In general, large proofs are problematic (difficult to understand/maintain, containing parts which could be useful as theorems by themselves, etc.). In my opinion proofs should usually not contain more than 100 (essential) steps, and maybe not more than 500 steps in extraordinary cases. Parts of large proofs should be extracted as separate theorems (if general enough) or as lemmata. But this is another topic to be discussed separately...

Norm

[David A. Wheeler]

On Dec 14, 2020, at 12:52 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Yes, I see - large proof would cause problems. In general, large proofs are problematic (difficult to understand/maintain, containing parts which could be useful as theorems by themselves, etc.). In my opinion proofs should usually not contain more than 100 (essential) steps, and maybe not more than 500 steps in extraordinary cases. Parts of large proofs should be extracted as separate theorems (if general enough) or as lemmata. But this is another topic to be discussed separately...

The “conventions” text already hints at limiting size:

       <li><b>Organizing proofs.</b>
       Humans have trouble understanding long proofs.
       It is often preferable to break longer proofs into
       smaller parts (just as with traditional proofs). In Metamath
       this is done by creating separate proofs of the separate parts.
       A proof with the sole purpose of supporting a final proof is a
       lemma; the naming convention for a lemma is the final proof's name
       followed by "lem", and a number if there is more than one. E.g.,
       ~ sbthlem1 is the first lemma for ~ sbth .  Also, consider proving
       reusable results separately, so that others will be able to easily
       reuse that part of your work.
       </li>

I would rather have long proofs than no proofs, so I think we shouldn’t make a hard-and-fast rule.

100 may be too small; perhaps recommend that they be under 200 instead?

How about this revision (note I said 200 instead of 100, discussion welcome)?:

       <li><b>Limit proof size.</b>

       It is often preferable to break longer proofs into
       smaller parts, just as you would do with traditional proofs.

       One reason is that humans have trouble understanding long proofs.

       Another reason is that it’s generally best to prove reusable results separately,

       so that others will be able to easily reuse that part of your work.

       Finally, the “minimize” routine can take much longer with very long proofs.

       We encourage proofs to be no more than 200 essential steps, and

       generally no more than 500 essential steps, though these are simply guidelines and

       not hard-and-fast rules.

       In Metamath this is done by creating separate proofs of the separate parts.

       A proof with the sole purpose of supporting a final proof is a
       lemma; the naming convention for a lemma is the final proof's name
       followed by "lem", and a number if there is more than one. E.g.,
       ~ sbthlem1 is the first lemma for ~ sbth .
       </li>

Feel free to slot in different numbers as guidelines. I know some people with the most expertise

often create long proofs (hi Mario!), so 100, 200, and/or 500 may be too small to be reasonable

in some cases.

But as long as we merely “encourage” smaller proofs as guidelines I think it’d be okay.

--- David A. Wheeler

[Alexander van der Vekens]

On Monday, December 14, 2020 at 7:30:30 PM UTC+1 David A. Wheeler wrote:

On Dec 14, 2020, at 12:52 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Yes, I see - large proof would cause problems. In general, large proofs are problematic (difficult to understand/maintain, containing parts which could be useful as theorems by themselves, etc.). In my opinion proofs should usually not contain more than 100 (essential) steps, and maybe not more than 500 steps in extraordinary cases. Parts of large proofs should be extracted as separate theorems (if general enough) or as lemmata. But this is another topic to be discussed separately...

The “conventions” text already hints at limiting size:

       <li><b>Organizing proofs.</b>
       Humans have trouble understanding long proofs.
       It is often preferable to break longer proofs into
       smaller parts (just as with traditional proofs). In Metamath
       this is done by creating separate proofs of the separate parts.
       A proof with the sole purpose of supporting a final proof is a
       lemma; the naming convention for a lemma is the final proof's name
       followed by "lem", and a number if there is more than one. E.g.,
       ~ sbthlem1 is the first lemma for ~ sbth .  Also, consider proving
       reusable results separately, so that others will be able to easily
       reuse that part of your work.
       </li>

 

Thank you for this hint.

I would rather have long proofs than no proofs, so I think we shouldn’t make a hard-and-fast rule.

100 may be too small; perhaps recommend that they be under 200 instead?

How about this revision (note I said 200 instead of 100, discussion welcome)?:

       <li><b>Limit proof size.</b>

       It is often preferable to break longer proofs into
       smaller parts, just as you would do with traditional proofs.

       One reason is that humans have trouble understanding long proofs.

       Another reason is that it’s generally best to prove reusable results separately,

       so that others will be able to easily reuse that part of your work.

       Finally, the “minimize” routine can take much longer with very long proofs.

       We encourage proofs to be no more than 200 essential steps, and

       generally no more than 500 essential steps, though these are simply guidelines and

       not hard-and-fast rules.

       In Metamath this is done by creating separate proofs of the separate parts.

       A proof with the sole purpose of supporting a final proof is a
       lemma; the naming convention for a lemma is the final proof's name
       followed by "lem", and a number if there is more than one. E.g.,
       ~ sbthlem1 is the first lemma for ~ sbth .
       </li>

I am fine with this revision, even with the encouraged maximum of 200 steps. I think it is a good idea to provide concrete numbers (instead of saying "proofs should not be  large") as a guideline, not a strict rule.

[Mario Carneiro]

I also think that 200 is an okay "soft maximum". I've definitely got some theorems larger than that, some a lot larger, and the MM0 project is going to generate some really large proofs (the largest so far is 673 steps but that's still mostly handwritten; the autogenerated proofs are going to be huge), but given that several verifiers tend to choke on large proofs it's best to keep them out of set.mm.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a0794916-43c7-4c91-8a25-2665c4e46a5an%40googlegroups.com.

[David A. Wheeler]

On Dec 14, 2020, at 3:01 PM, Mario Carneiro <di....@gmail.com> wrote:

I also think that 200 is an okay "soft maximum". I've definitely got some theorems larger than that, some a lot larger, and the MM0 project is going to generate some really large proofs (the largest so far is 673 steps but that's still mostly handwritten; the autogenerated proofs are going to be huge), but given that several verifiers tend to choke on large proofs it's best to keep them out of set.mm.

No one’s going to be shot for exceeding 200. But if it’s really unusual for handwritten proofs to exceed 500, and the vast majority are under 200, then writing this down as a convention has succeeded. I would encourage even smaller proofs than that, especially if they create reusable proofs; I think there are hidden reusable gems in some of our larger proofs.

If autogenerated proofs are huge, I presume it’s because they’re expanding something in place. That’s okay short-term. Longer-term, maybe we can modify the generators to also break up the proofs (e.g., if a template generates something long, create the template as a separate proof), or create a more-general proof that other proofs can directly use. So I think the guideline can help us create long-term improvements to generated proofs as well.

*Verifiers* shouldn’t struggle with large proofs. Can you give an example?

--- David A. Wheeler

[Mario Carneiro]

No, here I mean irreducibly huge. Breaking them up would make them a lot *less* efficient because there are a lot of interconnections and reused terms.

 

*Verifiers* shouldn’t struggle with large proofs. Can you give an example?

Here's the largest definition in MM0 right now (below). It's larger than the largest set.mm definition by a pretty significant margin, I think. Proving the equality theorem for this is already 250 steps, and the 673 step proof I mentioned is the typing statement (i.e. closure) for it. (It is the execution semantics of x86.)

This is peanuts compared to the definition of an actual program, as a sequence of instructions. Currently the plan is to segment the definitions at the function level, which is still going to result in definitions which are about 50 times the size of this one, and the typing/correctness proof of said function will be on the same order of magnitude with a hefty constant factor.

The MM0 verifier makes very short work of this theorem and all others. Currently the entire library (7400 theorems) verifies in 25ms, and I don't expect that to change once I start bringing out the big guns. But MM0 was designed with this use in mind, and it makes much greater use of long theorem statements that can be represented more efficiently in MM0 than in MM due to the use of expression tree deduplication. Eventually I will try to port things over but I expect that some of the proofs being generated will bring one verifier or another to its knees.

Mario

abstract def execXAST (k ast k2: nat): wff =
$ ast e.
  Sum
    (Sum
      (Sum
        (Sum
          (S\ op, S\ sz, {rm | E. q (readEA k sz (RM_EA k rm) q /\ writeUnop k op sz (RM_EA k rm) q k2)})
          (S\ op, S\ sz, {ds | E. d E. s (readEA k sz (destEA k ds) d /\ readEA k sz (srcEA k ds) s /\ writeBinop k op sz (destEA k ds) d s k2)}))
        (Sum
          (S\ _0, {_1 | _0 e.
            ocasep
              (_1 e.
                S\ sz, {rm | E. n E. src E. res (n = wsizeBits sz /\
                  readEA k sz (RM_EA k rm) src /\
                  res = readRegSz k sz RAX * src /\
                  ifp
                    (n = 8)
                    (k2 = writeReg k wSz16 RAX res)
                    (E. lo E. hi (splitBits ((n <> lo) : (n <> hi) : 0) res /\ k2 = writeReg (writeReg k sz RAX lo) sz RDX hi)))})
              {_2 | _1 e.
                S\ sz, {rm | E. n E. a E. b E. d E. m (n = wsizeBits sz /\
                  readEA k sz (RM_EA k rm) b /\
                  divModSz sz a b d m /\
                  ifp
                    (n = 8)
                    (a = readRegSz k wSz16 RAX /\ eraseFlags (writeReg k sz RAX (shl m 8 + d)) k2)
                    (splitBits ((n <> readRegSz k sz RAX) : (n <> readRegSz k sz RDX) : 0) a /\ eraseFlags (writeReg (writeReg k sz RAX d) sz RDX m) k2))}}})
          (S\ sz, {ds | writeEA k sz (destEA k ds) (EA_addr (srcEA k ds)) k2})))
      (Sum
        (S\ _0, {_1 | _0 e.
          {sz | _1 e.
            Sum
              (S\ _2, {_3 | _2 e.
                ocasep
                  (_3 e. S\ ds, {sz2 | E. src (readEA k sz (srcEA k ds) src /\ writeEA k sz2 (destEA k ds) src k2)})
                  {_4 | _3 e. S\ ds, {sz2 | E. src (readEA k sz (srcEA k ds) src /\ writeEA k sz2 (destEA k ds) (sExt (wsizeBits sz) (wsizeBits sz2) src) k2)}}}
              )
              (S\ _2, {_3 | _2 e.
                ocasep
                  (_3 e. S\ rm, {r | E. v (readEA k sz (RM_EA k rm) v /\ writeEA (writeReg k sz r v) sz (RM_EA k rm) (readRegSz k sz r) k2)})
                  (ocasep
                    (_3 e.
                      S\ rm, {r | E. src E. acc E. dst E. ki (acc = readRegSz k sz RAX /\
                        readEA k sz (RM_EA k rm) dst /\
                        writeBinop k binopCmp sz (EA_r r) acc dst ki /\
                        ifp (acc = dst) (writeEA ki sz (RM_EA k rm) (readRegSz k sz r) k2) (writeEA ki sz (EA_r RAX) dst k2))})
                    {_4 | _3 e. S\ rm, {r | E. v (readEA k sz (RM_EA k rm) v /\ writeBinop k binopAdd sz (RM_EA k rm) (readRegSz k sz r) v k2)}})})}})
        (S\ _0, {_1 | _0 e.
          {c | _1 e.
            Sum
              (S\ sz, {ds | ifp (readCond k c) (E. v (readEA k sz (srcEA k ds) v /\ writeEA k sz (destEA k ds) v k2)) (k2 = k)})
              (S\ b, {rm | writeEA k (wSz8 (true b)) (RM_EA k rm) (nat (readCond k c)) k2})}})))
    (Sum
      (Sum
        (Sum
          (Sum {rm | E. v (readEA k wSz64 (RM_EA k rm) v /\ k2 = writeRIP k v)} (S\ c, {q | k2 = if (readCond k c) (writeRIP k (readRIP k +_64 q)) k}))
          (Sum {irm | E. ki (pushRIP k ki /\ EA_jump ki (immRM_EA k irm) k2)} {q | E. ki (popRIP k ki /\ k2 = setReg ki RSP (readReg ki RSP +_64 q))}))
        (ocasep (popWrite (setReg k RSP (readReg k RBP)) (RM_reg RBP) k2) (Sum {irm | pushImmRM k irm k2} {rm | popWrite k rm k2})))
      (ocasep
        (k2 = writeFlags k (setCF (readFlags k) (~CF (readFlags k))))
        (ocasep
          (k2 = writeFlags k (setCF (readFlags k) F.))
          (ocasep
            (k2 = writeFlags k (setCF (readFlags k) T.))
            {_0 | E. r11 (r11 e. u64 /\ k2 = setException (setReg (setReg k RCX (readRIP k)) 11 r11) (suc exSysCall))})))) $;

[Dirk-Anton Broersen]

In despite of large proofs being problematic. They are solutive. The question is if a large proof giver a better understanding then a short proof. Or can a big proof maintain more information. I believe that all bigger proofs van be written as small proofs. There is where I might go wrong. Instead larger proof can maintain more information. So they are uniqe and give more information. That itself is a fact. But what’s the truth about it.

 

Verzonden vanuit Mail voor Windows 10

 

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/D406837B-B1E9-43D3-BA4E-D9B410F38D2A%40dwheeler.com.