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)