I tried to compile it and the metamath_knife::diag::Notation type doesn't exist. Neither https://github.com/david-a-wheeler/metamath-knife nor https://github.com/tirix/metamath-knife contains a definition of this type, and the toml file here refers to your local copy of metamath-knife, which presumably has the required changes. Could you push those changes to https://github.com/tirix/metamath-knife for reproducibility?

(The reason I wanted to compile it was to see how others are using metamath-knife API to generate new theorems.)

Hi, just forked this repo and am trying to run some example. New to rust, can you pls point me to the right direction?

Best regards
JA

Lately I've developed a few strategies to reduce axiom usage, but most of the time they require manual work, which is difficult to scale up. I've used Rumm for quite some time now, and it looks the closest tool that matches my needs. There is only one big problem that prevents me from doing anything useful with it: work variables are not supported.

In Metamath, work variables are temporary variables that are used during the proof process to allow the user to unify statements without knowing how the goal looks like. In metamath-exe those are indicated with $nn, while in mmj2 and yamma they are prefixed depending on their sort (wff, class or setvar), and suffixed with a number. All work variables disappear after the proof is completed.

Documentation about mmj2 work variables: https://github.com/digama0/mmj2/blob/master/doc/WorkVariables.html:

The primary purpose of Work Variables is to facilitate proof
entry using just assertion labels (aka "Ref"s) on the Proof Assistant
GUI screen, thus providing basic functional compatibility with the
metamath.exe Proof Assistant. Instead of entering formulas the user can
enter Ref's and allow the Proof Assistant to generate (derive) proof
step formulas.

Rumm has what I call "pseudo work variables", which are just defined as regular metamath variables, but with the notation of mmj2 and yamma (such as &W1, &C3, &S2 ecc..). The reason I call them "pseudo" is because, despite using the same notation of mmj2, they don't behave like work variables at all, and it took me a long time to get over that confusion and understand what's was going on.

Let's say, I want to revise he proof of opeq1, like I did in a recent PR metamath/set.mm#4015. The first theorem to apply is 3eqtr4g.

Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 44619913 bytes
44619913 bytes were read into the source buffer.
The source has 214112 statements; 2824 are $a and 42363 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> PROVE opeq1
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT opeq1"):
16206 opeq1 $p |- ( A = B -> <. A , C >. = <. B , C >. ) $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> DELETE ALL
The entire proof was deleted.
1    opeq1=? $? |- ( A = B -> <. A , C >. = <. B , C >. )
MM-PA> ASSIGN LAST 3eqtr4g
6 -2   3eqtr4g.1=?   $? |- ( A = B -> $4 = $5 )
7 -1   3eqtr4g.2=?   $? |- <. A , C >. = $4
8      3eqtr4g.3=?   $? |- <. B , C >. = $5
MM-PA>

We can see that temporary $nn variables appear, this feature allows me to unify the first missing step with abbidv without knowing the full statement of the goal:

MM-PA> ASSIGN -2 abbidv
10 -2     abbidv.1=?       $? |- ( A = B -> ( $8 <-> $9 ) )
12 -1   3eqtr4g.2=?      $? |- <. A , C >. = { $7 | $8 }
13      3eqtr4g.3=?      $? |- <. B , C >. = { $7 | $9 }
MM-PA>

Current proof of opeq1 for reference:

We can see that indeed metamath-exe unified without complaining. Now let's try to do the same with Rumm:

load "set.mm"

proof ~opeq1
{ apply ~3eqtr4g
   { apply ~abbidv
       ?
   }
   ?
   ?
}

The output is:

====================================================

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
 Attempting apply 3eqtr4g
 Proving |- ( A = B -> A = B )
 >> Apply abbidv
  Attempting apply abbidv
 << Apply statement doesn't match
Failure
Done.

The problem is: if the user does not provide with together with apply then Rumm will automatically assume the value of unkown variables to be the same as the ones written in 3eqtr4g itself. Therefore, the program will produce a dead-end goal and will not unify with abbidv.

This is a nasty behaviour, because the user needs information about the goal before applying any theorem, and more often than not the user does not know that (especially after a long running series of tactics). I also believe that this behaviour is not sound, because there is no reason to prioritize one statement as substitution for an unknown metavariable over an other. Not only the metamath-exe $nn variables are easier to work with, but they also make sense in the metamath perspective.

The mmj2-like variable naming in https://github.com/tirix/rumm/blob/master/rumm/examples/examples.mm could deceive the user into thinking that &C1 and &C2 are proper work variables, and attempt to make this edit:

load "examples.mm"

proof ~opeq1
{ apply ~3eqtr4g
   { apply ~abbidv
       ?
   }
   ?
   ?
   with ~cA $ &C1 $ ~cB $ &C2 $
}

But that doesn't work, as shown in the output below:

====================================================

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
Subst: cB class &C2
Subst: cA class &C1
 Attempting apply 3eqtr4g
 Proving |- ( A = B -> &C1 = &C2 )
 >> Apply abbidv
  Attempting apply abbidv
 << Apply statement doesn't match
Failure
Done.

This is because &C1 and &C2 are not work variables, they are defined as regular metamath variables.

Therefore I propose to add work variables in Rumm. The notation can stay the same as mmj2. This would make all the difference for me, because I could actually use Rumm to provide some interesting results that would require much more work with other proof assistants. I definitely see the potential of using tactics in metamath, and I wish some time in the future they will be added in the set.mm main repository (as a separate file, since I think tactics should be used to create proofs, but not to save proofs).

Note: I know that some sort of work variable behaviour is derivable with a match tactic preceding the apply tactic I want to implement. I won't enter into detailes, but I attempted to use this method many times and I always failed (there was always a point where I needed to know something about the goal). Even trying to combine it with the subgoal tactic just doesn't work. So, at the moment, I am stuck because of this.