The `use` tactic does not substitute metavariables

[GinoGiotto]

I'm going to show an example first and then explain what I mean.

Input file:

load "examples.mm"

tactics tactic ( +V )
{ match +V
  $ ( &W2 <-> &W3 ) $ ? 
}

proof ~abbi
{ match goal
	$ ( A. x &W1 <-> &C1 = &C2 ) $ { use tactic $ &W1 $ }
}

Output:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Use tactic
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Match
  Target wff &W1
  Trying wff ( &W2 <-> &W3 )
  << -- Match failed --
 << tactic complete
NoMatchFound
<< -- Match failed --
Failure
Done.

The output I expect:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Use tactic
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Match
  Target wff ( ph <-> ps )
  Trying wff ( &W2 <-> &W3 )
  Matched wff ( ph <-> ps ) with wff ( &W2 <-> &W3 )
   Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
   >> Skip
   << Skipped!
  Skipped
  << -- Match failed --
 << tactic complete
NoMatchFound
<< -- Match failed --
Failure
Done.

I'm using the example file example.mm of this repository, which uses set.mm.

Statement of ~abbi: $p |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) $

The problem is that { use tactic $ &W1 $ } should substitute the expression &W1 into the expression ( ph <-> ps ) when calling a tactic, but it doesn't. Note that this is unrelated to the issue about work variables #12, because the use tactic is actually the only one to have this unsound behaviour. All other Rumm tactics do susbtitute &W1 with ( ph <-> ps ) when utilized.

---

The other tactics do not behave this way

Below I show analogous examples with the other built-in tactics, to demonstrate that they do not behave like the use tactic (so use is the exception among them).

Input with apply tactic:

load "examples.mm"

proof ~abbi
{ match goal
	$ ( A. x &W1 <-> &C1 = &C2 ) $ { apply ~mpbi ? ? with ~wph $ &W1 $ }
}

Output:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Apply mpbi
 Subst: wph wff &W1
  Attempting apply mpbi
  Proving |- ( ph <-> ps )
  >> Skip
  << Skipped!
Skipped
<< -- Match failed --
Failure
Done.

We can see that the &W1 in with ~wph $ &W1 $ is correctly subsituted with ( ph <-> ps ) when read by Rumm, since it shows Proving |- ( ph <-> ps ) and not Proving |- &W1.

Input with subgoal tactic:

load "examples.mm"

proof ~abbi
{ match goal
	$ ( A. x &W1 <-> &C1 = &C2 ) $ { subgoal ? $ &W1 $ ? }
}

Output:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Subgoal
  Proving wff ( ph <-> ps )
  >> Skip
  << Skipped!
 << -- Subgoal failed --
Skipped
<< -- Match failed --
Failure
Done.

Here as well the &W1 in { subgoal ? $ &W1 $ ? } is correctly subsituted with ( ph <-> ps ) when read by Rumm.

Input with find tactic:

load "examples.mm"

proof ~abbi
{ match goal
	$ ( A. x &W1 <-> &C1 = &C2 ) $ { find ? $ &C1 = &C2 $ ? }
}

Output:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Find wff { x | ph } = { x | ps }
 Found match with abbii
   Proving |- ( ph <-> ps )
   >> Skip
   << Skipped!
 Found match with args
 Unification success
   subgoal = |- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Skip
  << Skipped!
 Found match with abrexco
   Proving |- B e. _V
   >> Skip
   << Skipped!
   Proving |- ( y = B -> C = D )
   >> Skip
   << Skipped!
 Found match with sprid
 Unification success
   subgoal = |- { p | E. a e. _V E. b e. _V p = { a , b } } = { p | E. a E. b p = { a , b } }
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Skip
  << Skipped!
 << Find: No match found
NoMatchFound
<< -- Match failed --
Failure
Done.

Here again the &C1 = &C2 in { find ? $ &C1 = &C2 $ ? } is correctly subsituted with { x | ph } = { x | ps } when read by Rumm.
(For the find tactic I used the expression $ &C1 = &C2 $ instead of $ &W1 $, because the latter matched with too many theorems, generating an output that was too long.)

Input with match tactic:

load "examples.mm"

proof ~abbi
{ match goal
	$ ( A. x &W1 <-> &C1 = &C2 ) $ { match $ &W1 $ $ ( &W2 <-> &W3 ) $ ? }
}

Output:

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

Proof for "abbi":
Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
>> Match
Target |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Trying wff ( A. x &W1 <-> &C1 = &C2 )
Matched |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } ) with wff ( A. x &W1 <-> &C1 = &C2 )
 Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
 >> Match
 Target wff ( ph <-> ps )
 Trying wff ( &W2 <-> &W3 )
 Matched wff ( ph <-> ps ) with wff ( &W2 <-> &W3 )
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Skip
  << Skipped!
 Skipped
 << -- Match failed --
NoMatchFound
<< -- Match failed --
Failure
Done.

Here also the &W1 in { match $ &W1 $ $ ( &W2 <-> &W3 ) $ ? } is correctly subsituted with ( ph <-> ps ) when read by Rumm (and so it will match with ( &W2 <-> &W3 ), which would not have happened if the substitution was not performed).

---

This is quite important for practical use of Rumm functionalities, in fact I recently noticed that fixing this use issue would overcome most problems of not having work variables #12, because I would be able to take advantage of substitution among tactics to simulate some pseudo work-variables behaviour. It wouldn't be as straightforward as just having work variables, but it would be enough to make a few ideas I've been developing for a while actually work.

[GinoGiotto]

This issue also occurs when a substitution list is provided as parameter to the use tactics, as described in #14 (comment)

[GinoGiotto]

@tirix Is there a plan to address this use issue any time soon? In July you replied that it would be looked at "this weekend", but it's January now and yet I have not been informed about any update (I don't even know if you agree that this is a bug, since no comment has been provided so far).

I also mentioned this issue in the mailing list a week ago, but even there I got no replies. My claim is that fixing it would be good enough to address the lack of work variables. Even if it's not a perfect solution, it's a solution (and it should probably be fixed anyway, independently of work variables).

If there will be no progress in reasonable time I'm afraid I'll have to abandon my contribution to this project. Rumm is potentially a great tool, but it's not sufficient to use it for complex projects in its current condition.

For the record, I also attempted to use your work-variables branch of metamath-knife in Rumm, but I got a bunch of compiling errors, so that option didn't work either.

[tirix]

Sorry, I should not have made promises I could not keep!

I'll certainly need a bit of time to revive the Work Variable work I had started, but this issue here seems to be a lower hanging fruit, at first sight. I'll be busy with other things this weekend, and I certainly should avoid making more promises I can't keep, but I was really very happy to see someone use Rumm, and I should not let you down.