antecedents

When I develop a proof I rarely have the courage to abandon an antecedent in the list of antecedents because I'm never sure I won't need this antecedent later. However very often I realize that I've kept many antecedents I could have dropped sooner because they reveal themselves irrelevant but in that case I'm often too much bored by the proof or too much tired to remake the proof and clean the unnecessary antecedents.

Therefore (as Alexander likes to say):

Would it be possible to have a routine or a script which removes the antecedents for me (either in metamath or in mmj2) or a way to highlight the never used antecedents or any clever device which would help me in this fastidious task. – fl 11-May-2008

One challenge in fulfilling your request is that an antecedent in a WFF might in some cases be needed for Unification, and therefore, after the "cleansing" operation is completed you would be left with a bogus proof or subproof. On the other hand, if an antecedent is merely a needless subtree in a unification substitution "payload" of a WFF then erasing the antecedent from all locations in the proof would have no ill effects.

There is one feature that might do exactly what you want in some cases. It was added in the recent release at Norm's request and is found on the Unification Menu:

• Unify+Erase and Rederive Formulas – Same as 'Unify (check proof)', but before the unification process begins the formula is erased on every non-qed Derivation Step which has a Ref label; if there are no errors the 'Derive' feature will rederive the formulas.

An alternative, low tech for sure, is Edit/Copy the entire Proof Worksheet, paste into a separate text editor which has a Search/Replace function, make the fix-up changes, and then paste the text back into mmj2 – mmj2 maintains no "state information" about the work in progress, so you can paste anything into the main GUI window and start over at any time (mmj2 does maintain a "next" index number used for forward and backward paging requests.)

I've always been thinking that walking is a good workaround for car. :-) Look that (I was checking what a workaround is) it's a specific American institution ("the bulletin board") in a famous school ("MIT"). Emotion ! : [[1]] – fl

I never walk anymore, except in circles around my swimming pool while I read. It is too dangerous because of the gangs of gunmen wearing police uniforms :-) Seriously, mon cher, if I had spare cogitons and life force I would write you a prover, then you wouldn't have to worry about details like this! --ocat

Swimming is as well a good workaround for boat. Well this problem seems a bit less difficult than proving a theorem automatically. I think there could an answer, even a partial (but interesting) answer. – fl

My first suggestion, re: the "Unify+Erase And Rederive Formulas" function is very good at making the useless bits go away – but it doesn't help if the formulas in question do not have a justifying Ref. I do like enhancement ideas, but… this mmj2 Swiss Army Knife will always be seen as inadequate when what you really need is an electric chainsaw or an atom bomb :-) A total rewrite is in order, but I am just a poor American struggling to survive in the global economy, and I have no corporate benefactors…(((weeping, sobbing, whining, gnashing of teeth…)))

I must remember you that Americans are the most Favoured Race in the Struggle for Life and when one compares the vitality of computer industry in the States with what exists in France one regrets to have chosen the bad country to be born. Courage! – fl

It is not the US vs. France but the Corporations vs. People :-) You should not judge us by our politicians and television propaganda. (Many of us don't even know where France is :-) --ocat

Workaround for the metamath program

Unfortunately, there is currently no automated way to drop redundant antecedents or even identify them. You still have to look at the final proof manually to find the places where they aren't needed, then revise those parts of the proof by hand.

Like ocat suggests, the "Unify+Erase And Rederive Formulas" can be a good way to repair proofs in mmj2. In terms of future mmj2 features, thinking about what might be helpful to assist the general problem of "proof repair" could be useful.

For the metamath program, there is a script that I often use to assist this and other proof-repair tasks. The following script, "makeproof.cmd", when run inside of "MM-PA>" for a completed proof, will generate a script "p.tmp" that will regenerate the proof from scratch.

  set width 999
  open log p.tmp
  show new_proof
  close log
  set width 79
  tools
  match p.tmp $ y
  delete p.tmp "" =
  delete p.tmp " " ""
  add p.tmp "assign last " " /no_unify"
  reverse p.tmp
  exit

Let's look at how to use it, taking the example syl:

  MM> prove syl
  MM-PA> submit makeproof.cmd

This will generate a file p.tmp that will have commands to build the syl proof. To erase and regenerate the whole proof, type the following:

  MM-PA> delete all
  MM-PA> submit p.tmp

In practice, I will extract a section of p.tmp to rebuild the part of a proof section I deleted for revision. For example, suppose I want to move an "adantl" 3 steps later in the proof (i.e. 3 steps earlier in the proof building). I'll delete the proof section at the point where the new adantl will be added and extract from p.tmp the commands to rebuild that section. In the extracted p.tmp section, I'll move the adantl up 3 steps.

It takes some practice to identify the necessary lines in p.tmp based on the pattern of label assignments. Usually I will have a listing of the original proof in another window for reference. To save time, often I'll identify just the first place in p.tmp that I need, and copy from it to the end of file. After the necessary lines from the p.tmp script complete the proof, the extra lines just cause harmless error messages that can be ignored.

I always save the proof ("save new_proof") just before submitting a p.tmp section so that I can easily recover ("q/f", "prove"). A simple error, like being one line off, can make a mess of the proof.

By no means is this an ideal solution, but it is just a way to save time in a lot of cases when I need to rewrite proofs to make them shorter. Whether it is worth doing depends on the situation. If I just need to re-enter 5 steps, it's quicker to type them in, but for 50 steps, a section extracted from p.tmp can save a lot of time.

By the way, I always drop redundant antecedents in the official set.mm sections to obtain shorter proofs, even if it is a lot of work, and I strongly encourage you to do that. If you are too tired or too bored, then at least put a note in the comment indicating that the proof has or might have redundant antecedents that need to be dropped. This way, someone else (like me, if I'm making a sandbox proof "official") will know that the proof needs to be cleaned up. Without such a comment, I would have to assume that every proof needs to be cleaned up, even if it already has been, and that wastes a lot of my time. – norm 14 May 2008

OK Thank you Norm and Ocat for this help it is not what I hope but I understand this problem is not exactly trivial either. – fl 19 May 2008