searching for theorem manually in Metamath lamp/

[Marshall Stoner]

Hi all.

I'm in the process of writing my own Metamath database.  To start, it's basically a refactoring of the logic portion of the set.mm database but with my own numbered naming system for theorems in order to correspond with a pdf book that explains things informally but in more detail.  Anyways I will share more later if anyone is interested.

My main issue is when writing proofs I sometimes wish to use a specific theorem for the sake of clarity, but the proof assistant will automatically complete the proof with a different theorem.  This happens because proof assistant seems to always choose the earliest theorem, while, for the sake of presentation, I might prefer to use a later version that accomplishes the same thing.  Sometimes I will restate earlier theorems just to group them ( for instance, restating all natural deduction rules in one place ).

In any case, this means I sometimes need to clear the justification field and carefully type in the name of the theorem I wish to use.  This process would be faster if there was a feature where instead of using the proof assistant I could simply type a search query and pick from a list.

[Igor Ieskov]

If I correctly understand the issue, then a feature similar to what you described already exists in Metamath-lamp. In order to change a justification, you may do the following:

1. Select the checkbox to the left of the step you want to modify the justification for.

2. Click the “Unify all” button.

3. In the text field “Label of root justification” select another assertion you want to use. It is enough to type only a part of another assertion name.

4. If the new assertion requires another set of arguments, then make sure the parameter “Allowed statements: first level” is set to “All”. If the arguments are the same, then you may leave this parameters as is.

5. Click the “Prove” button.

6. If a proof is found then clicking the “Apply” button will modify the justification in the editor to use the new assertion you selected.

Here is a short demo - https://drive.google.com/file/d/1R4waaGFS2WUT-Apq7RMXVuaUIJMVhh8q/view?usp=sharing 

–

Igor

[Marshall Stoner]

Thank you.  This works.