One great thing about KeYmaera X is the combination of a well-documented implementation with a fancy, point-and-click web UI. During proof development, sometimes you really want to visually explore the current proof state or easily target tactical applications on deeply nested formulas. But sometimes you want the flexibility that comes with a full, general-purpose programming language.

To support both modes of theorem prover usage, our Bellerophon tactic language is both a parsed language (the syntax described in our Bellerophon paper and used in the web UI and in .kyt files) and also a Scala Domain-Specific Language library. The parsed language and the DSL have the exact same semantics, but slightly different concrete syntax. The discrepancies between “Scala Bellerophon” and “Parsed Bellerophon” are mostly attributable to cruft and syntactic warts imposed by the Scala DSL that we didn’t want to re-implement in the parsed language.

Fortunately, there’s a very easy way to move proof scripts from the Web UI (or a .kyt file) into the Scala DSL.

As a running example, consider this tactic, implementing a partial proof:

implyR(1); 
andR('R)*;
loop({`x >= 0`}) <(
  master
  ,
  master
  ,
  nil
)

If you type this tactic into Scala directly, you’ll get compiler errors. To use this “parsed Bellerophon” program as a “Scala Bellerophon DSL” program, import the String.asTactic from the edu.cmu.cs.ls.keymaerax.parser package and then use this method to parse the tactic:

import edu.cmu.cs.ls.keymaerax.parser.StringConverter._


val t = """
        |implyR(1); 
        |andR('R)*;
        |loop({`x >= 0`}) <(
        |  master
        |  ,
        |  master
        |  ,
        |  nil
        |)""".stripMargin.asTactic

You can now use t in a larger Scala DSL proof:

t & myFancyInternalTactic

Other Tips

When using the Scala Bellerophon DSL, notice that there are substantial differences in concrete syntax:

  • You may need to import various things from the edu.cmu.cs.ls.kemyaerax.btactics package.
  • Some tactics might need parentheses; e.g., master() instead of master.
  • Use "f".asFormula instead of {`f`}. Remember to import edu.cmu.cs.ls.keymaerax.parser.StringConverter._
  • You may need to (un)curry some operations; e.g., loop("1=1".asFormula)('R) instead of loop({`1=1`}, 'R)
  • You’ll need to initialize any tools you use. See TacticTestBase.withMathematica for an example of how to do this.
  • The KeYmaera X Documentation is your friend, and there’s even a whole section on Bellerophon’s library.
  • The IOListener is a useful tool for extending the interpreter

Especially as you start working with the KeYmaera X source code itself, don’t hesitate to contact me!