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/8f2088b9-3116-4c48-948e-d263f529b9c7%40googlegroups.com.
