Removing hypotheses

How to remove hypotheses

This page covers how to remove hypotheses when the hypothesis are unused or redundant. Essentially, the goal is to replace such hypotheses with zero or more steps, while keeping the rest of the proof.

Let's say we want to remove addcld.1 from addcld in set.mm (this is impossible, but it is a good example)

1. In metamath.exe:

   read set.mm
   show proof addcld /normal
   

   Copy the normal proof (and paste it into an empty notepad window, if clipboard history is not enabled).
2. In the database file (for example set.mm), duplicate the theorem you want to change, and change it as follows:
   1. Rename the copy to a temporary label (for example, addcld can be .ddcld).
   2. The copy should have as its proof: the normal proof from above.
   3. In the normal proof, replace all addcld.1 with ?
3. In metamath.exe:

   erase
   read set.mm
   prove .ddcld
   <prove the first instance of each hypothesis to be removed, then run `improve all`>
   save new /compressed
   write source set.mm
   

4. Minimize all theorems using the old proof (there is a tool for this: ./scripts/min.cmd)
5. Delete the old copy or mark it as OLD, and then replace all uses of temporary label with the original label (.ddcld → addcld)
6. Add a Revised by tag and regenerate the discouraged file if necessary.

As an alternative to using the normal proof for the copy, one can manually delete step <step> for all steps corresponding to hypotheses (using show new to show all the steps), but this is usually slower.

Slight modification

In the case where a hypothesis like I e. V is replaced with a proof that I e. _V, notice how V is not the same as _V. In order for metamath.exe to have I e. &?? as a goal instead of I e. V, within step 2, replace all cV in the normal proof with ?.

A similar strategy may be possible for other cases, but in general the strategy will be more extensive.