What does s/ mean?

[GinoGiotto]

The set.rmm file contains this expression: s/ $ X $ / $ Y $ / $ &C1 $, for example here:

rumm/set.rmm

Line 131 in 789b5ff

$ ( X = Y -> &C1 = &C2 ) $ { apply ~syl6eqr { use equality } ! with ~cB s/ $ X $ / $ Y $ / $ &C1 $ }

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:

rumm/rumm/src/lang/expression.rs

Lines 37 to 44 in 789b5ff

	FormulaExpression::DirectSubstitution(what, with, in_expr) => {
	fmt.write_str("s/")?;
	what.format(fmt, db)?;
	fmt.write_str("/")?;
	with.format(fmt, db)?;
	fmt.write_str("/")?;
	in_expr.format(fmt, db)
	}

It seems FormulaExpression also has something similar called ListSubstitution, what is that instead?

rumm/rumm/src/lang/expression.rs

Lines 45 to 48 in 789b5ff

	FormulaExpression::ListSubstitution(id, in_expr) => {
	fmt.write_fmt(format_args!("s/ *{id} /"))?;
	in_expr.format(fmt, db)
	}

[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.

rumm/rumm/src/tactics/use_script_tactics.rs

Lines 13 to 16 in 1ab8d60

	pub struct UseScriptTactics {
	name: String,
	parameters: Vec<Expression>,
	}

rumm/rumm/src/lang/expression.rs

Lines 218 to 223 in 1ab8d60

	pub enum Expression {
	Formula(FormulaExpression),
	Statement(StatementExpression),
	Tactics(TacticsExpression),
	SubstitutionList(SubstitutionListExpression),
	}

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 #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 #17.