What does `s/` mean?

[GinoGiotto]

The set.rmm file contains this expression: s/ $ X $ / $ Y $ / $ &C1 $, for example here: https://github.com/tirix/rumm/blob/789b5ffdfae05d598cbd614e734c736b0affa4f0/set.rmm#L131

There is no mention of s/ in the specification rumm.md and I've done some testing without being able to figure out what it does. What does it mean? @tirix

[tirix]

It's a substitution. For example, s/ $ X $ / $ Y $ / $ ( X + 1 ) $ replaces X by Y in ( X + 1 ), so it would result in ( Y + 1 ).

The issue with syl6eqr (which became eqtr4di in the mean time), is that the the B does not appear in the final statement:

  ${
    eqtr4di.1 $e |- ( ph -> A = B ) $.
    eqtr4di.2 $e |- C = B $.
    $( An equality transitivity deduction.  (Contributed by NM,
       21-Jun-1993.) $)
    eqtr4di $p |- ( ph -> A = C ) $=
      ( eqcomi eqtrdi ) ABCDEDCFGH $.
  $}

So, we have to tell to Rumm what to use for B.

Let's take the proof of isufd as an example.

At step 7, we are facing the goal formula |- ( r = R -> ( PrmIdeal ` r ) = I ). Here, we need to use the hypothesis |- I = ( PrmIdeal ` R ) to get to |- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ). We want to apply eqtr4di/syl6eqr. Obviously, ph is r = R, A is ( PrmIdeal ` r ) and C is I, but the value of B is the result of a substitution.

So, we take the &C1, which is evaluated to ( PrmIdeal ` r ), and substitute r for R in this formula. The result is ( PrmIdeal ` R ), which is what we need for B.

[GinoGiotto]

Ok, so I guess it corresponds to DirectSubstitution in FormulaExpression: https://github.com/tirix/rumm/blob/789b5ffdfae05d598cbd614e734c736b0affa4f0/rumm/src/lang/expression.rs#L37-L44

It seems FormulaExpression also has something similar called ListSubstitution, what is that instead? https://github.com/tirix/rumm/blob/789b5ffdfae05d598cbd614e734c736b0affa4f0/rumm/src/lang/expression.rs#L45-L48

[tirix]

Yes, exactly, it corresponds to DirectSubstitution in FormulaExpression.

As far as ListSubstitution is concerned, it looks like it is not used yet in the code committed to GitHub, but here is the idea:

It allows the tactics to act essentially like apply, i.e. to provide to the tactics the substitutions it cannot guess. Some tactics scripts will have the with keyword in their parameters, and a name for the substitutions, like this:

tactics deduction_apply ( ≈THM @T with *R )

Then, within the tactics script's body, *R can be used like any other substitution, for example in a with keyword when using apply, or if using another script tactics. This allows e.g.

{ apply ~syl { use deduction } @T with *R }

Which would use syl with any substitution listed in *R . This somehow exposes the inner workings of the tactics to its user, but this is actually more or less the same way apply works.

[GinoGiotto]

Ok, there are a lot of things to say, I'll try to be concise and focus on what's important:

First of all, the specification says that the use tactic supports three kind of parameters: a <formula>, a theorem <statement> and a tactic <tactics>, but they are not three, they are four, because as you mentioned a with keyword is also a valid parameter. We can see this in the code as well. parameters is a vector of elements of type Expression and Expression is an enum of four variants. The fourth variant is called SubstitutionList which corresponds to the with keyword you just mentioned.

https://github.com/tirix/rumm/blob/1ab8d60a929d0788bc02b590a06b7eebd011a66c/rumm/src/tactics/use_script_tactics.rs#L13-L16

https://github.com/tirix/rumm/blob/1ab8d60a929d0788bc02b590a06b7eebd011a66c/rumm/src/lang/expression.rs#L218-L223

So the specification needs an update, I can help you with it since I've gained a bit of familiarity with Rumm and I don't want future users to face the same headache I've gone through to understand what's missing in the specification.

---

But what's even more important is that the same bug I mentioned in https://github.com/tirix/rumm/issues/13 does appear for the with keyword as well. Here is a minimal example:

Input:

load "examples.mm"

tactics tactic ( with *R )
{ apply ~mpbi ? ? with *R }

proof ~abbi
{ match goal
        $ ( A. x &W1 <-> &C1 = &C2 ) $ { use tactic 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 } )
 >> Use tactic
  Proving |- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
  >> Apply mpbi
  Subst: wph wff &W1
   Attempting apply mpbi
   Proving |- &W1
   >> Skip
   << Skipped!
 << tactic complete
Skipped
<< -- Match failed --
Failure
Done.

We can see that at the end it shows Proving |- &W1 which is not what we want. The variable &W1 should be substituted with ( ph <-> ps ) (as all other tactics do, see #13), therefore the expected output should be:

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

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 } )
  >> Apply mpbi
  Subst: wph wff ( ph <-> ps )
   Attempting apply mpbi
   Proving |- ( ph <-> ps )
   >> Skip
   << Skipped!
 << tactic complete
Skipped
<< -- Match failed --
Failure
Done.

[tirix]

So the specification needs an update, I can help you with it since I've gained a bit of familiarity with Rumm and I don't want future users to face the same headache I've gone through to understand what's missing in the specification.

Yes! Thanks for the help, and sorry for the lack of specification of that feature. I might have added it after writing the specs.

I'll try to have a look at this issue and #13 this weekend!

[GinoGiotto]

Closing since specification for this keyword has been added in https://github.com/tirix/rumm/pull/17.