Work variables

[GinoGiotto]

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 https://github.com/metamath/set.mm/pull/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.

[tirix]

Thanks for opening the issue!

I completely agree with the need to correctly handle work variables. Rumm is relying on metamath-knife, so ideally metamath-knife itself would provide this service, and I've been attempting to introduce work variables in set.mm. See for example metamath/metamath-knife#89.

To be sure I understand what you wish, let me write down what I think you expect with your last example:

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

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
  Subst: &C1 class { &S1 | &W1 }
  Subst: &C2 class { &S1 | &W2 }
  Proving |- ( A = B -> ( &W1 <-> &W2 ) )
    << Skipped
Failure
Done.

So Rumm would autonomously allocate 3 new work variables &S1, &W1, and &W2, and unify with those? Or what is it you'd expect?

[tirix]

Another note: working on the minimizer (metamath/metamath-knife#156), I had a kind of epiphany regarding how to run unification "at the same time" for hypotheses and main statement.

The extend function I've added to the Substitution structure allows checking that substitutions for each formula agree. This was previously not done correctly and led to some problems when unifying. Rumm would benefit from this improvement, too.

[GinoGiotto]

So Rumm would autonomously allocate 3 new work variables &S1, &W1, and &W2, and unify with those? Or what is it you'd expect?

Thanks for your interest, your output is precisely what I expect. The only difference would be in the input; I would prefer the use of work variables to be the default behavior (so if the user does not provide with together with apply, then Rumm will automatically use work variables, rather than assuming a statement for the unknown variables).

In summary my dream would be:

Input:

load "set.mm"

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

Output:

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

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
  Subst: &C1 class { &S1 | &W1 }
  Subst: &C2 class { &S1 | &W2 }
  Proving |- ( A = B -> ( &W1 <-> &W2 ) )
    << Skipped
Failure
Done.

It wouldn't even be needed to declare the names of work variables in the .mm file, the program would generate them for you (like mmj2 does).

Rumm is relying on metamath-knife, so ideally metamath-knife itself would provide this service, and I've been attempting to introduce work variables in set.mm. See for example https://github.com/metamath/metamath-knife/pull/89.

I did not know that this was already an ongoing project, I definitely support the merge of this PR!

---

Tangent topic

The extend function I've added to the Substitution structure allows checking that substitutions for each formula agree. This was previously not done correctly and led to some problems when unifying. Rumm would benefit from this improvement, too.

Now, my knowledge of metamath-knife is very much limited. But could your examination be related to the following observation?

Input:

load "set.mm"

proof ~opeq1
{ apply ~3eqtr4g
   ?
   ?
   ?
   with ~3eqtr4g.1 statement ~rabeqf
}

Output:

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

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
Subst: 3eqtr4g.1 |- ( A = B -> { x e. A | ph } = { x e. B | ph } )
 Attempting apply 3eqtr4g
 Proving |- ( A = B -> A = B )
 >> Skip
 << Skipped!
Failure
Done.

I know that with ~3eqtr4g.1 statement ~rabeqf is an improper use of the with feature, but the weird thing is that it doesn't even give an error, it accepts the apply tactic I provided, but the goal doesn't match the statement I gave to 3eqtr4g.1. I'm guessing that statement ≈THM was designed to generate formulas without metavariables (so every symbol in that formula behaves like a costant and matches only with itself). So, considering that, the intuitive operation for me would be to unify:

|- ( A = B -> &C1 = &C2 ) which is the "hidden" goal (not displayed on the output yet). with |- ( A = B -> { x e. A | ph } = { x e. B | ph } ) which is the statement of rabeqf.

Therefore I'd expect:

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

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
Subst: 3eqtr4g.1 |- ( A = B -> { x e. A | ph } = { x e. B | ph } )
 Attempting apply 3eqtr4g
 Proving |- ( A = B -> { x e. A | ph } = { x e. B | ph } )
 >> Skip
 << Skipped!
Failure
Done.

Which I would expect to be the same output generated by:

load "set.mm"

proof ~opeq1
{ apply ~3eqtr4g
   ?
   ?
   ?
   with ~3eqtr4g.1 $ ( A = B -> { x e. A | ph } = { x e. B | ph } ) $
}

But instead this one even fails to apply 3eqtr4g (notice how the following output differs from the one above):

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

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
Failure
Done.

If I add a turnstile |- to the formula assigned to with, Rumm just gives an error (I initially thought that the issue might be caused by accidentally unifying a wff with a provable statement).

In the end I was basically expecting the example above to generate the same goal as:

load "set.mm"

proof ~opeq1
{ apply ~3eqtr4g
   ?
   ?
   ?
   with ~cA $ { x e. A | ph } $ ~cB $ { x e. B | ph } $
}

Which expectedly generates:

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

Proof for "opeq1":
Proving |- ( A = B -> <. A , C >. = <. B , C >. )
>> Apply 3eqtr4g
Subst: cB class { x e. B | ph }
Subst: cA class { x e. A | ph }
 Attempting apply 3eqtr4g
 Proving |- ( A = B -> { x e. A | ph } = { x e. B | ph } )
 >> Skip
 << Skipped!
Failure
Done.

Note that I'm not asking to resolve this other issue, as it's not important to me (work variables are definitely more important). This is just a question whether you were aware of this behaviour.