I think there is no contradiction in the approaches of Wolf and Benoît: Wolf is talking about the main proofs, and Benoît about alternate proofs, providing criteria to keep (ALT) or to delete (OLD) theorems with different proofs. Therefore, both opinons are valid. A good, additional example is my theorem cayleyhamilton, which I provided with two proofs: the main one using ($e statement) definitions, and an ALT variant which does not use these definitions, but expand them, resulting in longer lines in the proof (for details see https://groups.google.com/d/msg/metamath/-RLnH6BcNTo/_kIagCsqAgAJ).
On Thursday, November 28, 2019 at 5:25:43 PM UTC+1, Benoit wrote: > > On Thursday, November 28, 2019 at 2:18:19 PM UTC+1, ookami wrote: >> >> The rules by which a proof is considered shorter were explained to me by >> Norm about 10 years ago: First look at the size of the encoding of the >> compressed proof, not taking the references into account. On tie, count the >> number of symbols used in the HTML display of the proof. >> > > We all agree with this, and nothing in my previous post contradicts this. > > >> I used the second rule extremely seldom in the past years, maybe twice or >> so. And I extended these rules by allowing one proof to be longer, if >> another/others benefit such, that in total their combined proof size >> shrinks. A recent example of this is neneqad. eqcom is an example that uses >> more definitions than the OLD one, and eqeq12i has the essential steps >> increased. All of these cases combined are rare, fewer than 5% I guess out >> of hand. >> > > Applying what I proposed in my previous post, eqeq12iOLD should be > relabeled eqeq12iALT (with both discouragement tags), its comment could > read "Alternate proof of ~ eqeq12i , longer but with fewer essential steps" > and the comment of eqeq12i could mention "See also ~ eqeq12iALT for a > longer proof, but with fewer essential steps." > > As for eqcom, I think that eqcomOLD can be deleted (referring to the part > of my previous post where I wrote "this [keeping the longer proof as ALT] > is not automatic"). > > As for neneqad: I would keep neneqadOLD and relabel it neneqadALT (since, > as I wrote in my previous post, "I lean to the side...") but I admit that > here, this is debatable. > > Are shorter proofs less readable than others? >> > > No, they need not be, and most of the times, they are not. As I wrote in > my previous post, "shorter proof does not always mean easier-to-understand > proof". Not the same thing. > > >> IMO, certain techniques making twisted use of negation (like nsyl) force >> me occasionally to look/think twice. So, yes, from my personal >> perspective... it can happen. But not being able to grasp negated formulas >> that easily I consider my personal disadvantage. This is not really an >> objective argument As for the avoidance of definitions... well, what are >> they meant for, then? Is it really a good idea to expand them? >> > > I did not suggest this. What I meant is that if a "naturally obtained" > proof turns out to use fewer definitions, then it may be the case (as I > wrote in my previous post, "this is not automatic") that this proof has an > interesting feature which might make us want to keep it as an ALT proof. > > >> And to take the idea further, theorems are again obstacles on the way to >> simplify proofs to just a sequence of axioms. I cannot quite follow here. >> But please, see and decide yourself whether the results mandate a change of >> rules. I gave you the examples above >> > > The rules neet not be changed. As before, if the proof you obtain is > shorter (according to the rules that you stated), then this should be the > main proof. What I meant to say is: the older proof may sometimes be worth > keeping as an ALT proof, because of this or that special feature. > > Benoît > -- 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/87c871ba-0cbd-40c6-9873-6663feb31953%40googlegroups.com.
