infrastruct

package infrastruct

The infrastruct package provides central prover infrastructure such as unification and augmented formula analysis. This infrastructure is of basic interest and useful independently of any particular tactic language etc.

Main functionality:

Position with PosInExpr positioning within subformulas.
Context Convenience representation of formulas used as contexts that provide ways of substituting expressions in by conceptually splitting and managing the context around a position in a formula.
RenUSubst Renaming Uniform Substitutions that quickly combine and ultimately reduce to uniform renaming and uniform substitution of the kernel.
UnificationMatch single-sided matching unification algorithms.
Augmentors: Implicit convenience additions of helper functions to formulas, terms, programs, sequents that are useful for analysis and transformation.
ExpressionTraversal generic functionality for traversing expressions for analysis or transformation.

See also: edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

infrastruct
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Type Members

trait AntePosition extends Position
A position guaranteed to identify an antecedent position, so on the left-hand side of the sequent turnstile.
A position guaranteed to identify an antecedent position, so on the left-hand side of the sequent turnstile.

See also
AntePos
Sequent
trait BaseMatcher extends Matcher with Logging
Basic matcher infrastructure that simply forwards all unification functionality to BaseMatcher.unify().
Basic matcher infrastructure that simply forwards all unification functionality to BaseMatcher.unify(). Only apply() functions wrap exceptions in context while unify() functions simply pass it upwards.
sealed trait Context[+T <: Expression] extends (Expression) ⇒ Formula
Convenience wrapper around contexts such as f(.) or p(.) or C{_} to make it easy to instantiate their arguments.
Convenience wrapper around contexts such as f(.) or p(.) or C{_} to make it easy to instantiate their arguments.
T
the type/kind of expression that this context is representing.
Example:
1. Split a formula at a position into subformula and its context, then instantiate this context with other subformulas:
  val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1") // split f into context ctx and subformula g such that f is ctx{g} val (ctx,g) = Context.at(f, PosInExpr(1::1::Nil)) println(f + " is the same as " + ctx(g)) // put another formula h in in place of g val h = parser("x^2>y") // x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x^2>y) val result = ctx(h) println(result)
final class DirectUSubstAboveURen extends RenUSubstBase
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substitution.
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substitution.
```
s(RG) |- s(RD)
-------------- USubst
  RG  |- RD
-------------- URen
   G  |- D
```
Semantic renaming may be supported if need be.
DirectUSubstAboveURen is a direct implementation in tactics land of a joint renaming and substitution algorithm. It uses a single direct fast USubstRen for direct internal applications via DirectUSubstAboveURen.apply() but schedules separate uniform substitutions and uniform renamings to the core when asked. The first fast pass supports semantic renaming, which is useful during unification to "apply" renamings already to predicationals without clash. The final core pass does not support semantic renaming, but is only needed for the final unifier.
Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
See also
FastUSubstAboveURen
final class FastURenAboveUSubst extends RenUSubst
Fast implementation of: Renaming Uniform Substitution that, in goal-directed backwards Sequent direction, first runs a uniform substitution below and on the result subsequently the uniform renaming above it.
Fast implementation of: Renaming Uniform Substitution that, in goal-directed backwards Sequent direction, first runs a uniform substitution below and on the result subsequently the uniform renaming above it.
```
R(s(G)) |- R(s(D))
------------------ URen
   s(G) |- s(D)
------------------ USubst
     G  |- D
```
The direct application mechanism via apply() fast-forwards to the fast joint USubstRen infrastructure. Its tactical / prover core implementation works in sync using prover core operations by scheduling separate uniform substitutions and uniform renamings to the core when asked.
Cleverly exploits semantic renaming on Provables on demand (although not in full generality yet).
Note
reading in Hilbert direction from top to bottom, the uniform renaming comes abiove first then the subsequent uniform substitution comes below as second.
See also
USubstRen
final class FastUSubstAboveURen extends RenUSubst
Fast implementation of: Renaming Uniform Substitution that, in goal-directed backwards Sequent direction, first runs a uniform renaming below and on the result subsequently the uniform substitution above it.
Fast implementation of: Renaming Uniform Substitution that, in goal-directed backwards Sequent direction, first runs a uniform renaming below and on the result subsequently the uniform substitution above it.
```
s(RG) |- s(RD)
-------------- USubst
  RG  |- RD
-------------- URen
   G  |- D
```
The direct application mechanism via apply() fast-forwards to the fast joint USubstRen infrastructure. Its tactical / prover core implementation works in sync using prover core operations by scheduling separate uniform substitutions and uniform renamings to the core when asked.
Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
See also
USubstRen
DirectUSubstAboveURen
class FreshUnificationMatch extends SchematicComposedUnificationMatch
Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms).
Unification/matching algorithm for fresh shapes (with built-in names such as those in axioms). Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher.

Note
Expects shape to have fresh names that do not occur in the input. Usually shape has all built-in names ending in underscore _ and no input is like that.
trait InsistentMatcher extends Matcher with Logging
A matcher that insists on always matching as if there were arbitrary expressions as opposed to specializing to Term versus Formula etc.
trait Matcher extends (Expression, Expression) ⇒ RenUSubst
Matcher(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa.
Matcher(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape, i.e., gives a single-sided matcher.
The following notation is used to indicate that u is the unifier computed for matching input t against shape s:
```
s = t | u
```
That is u is the result of calling Matcher.apply(s,t).
Examples:
1. val s = Matcher("p()&q()".asFormula, "x<=0 & x^2>=0".asFormula) // gives {p() ~> x<=0, q() ~> x^2>=0} println(s)
2. val s = Matcher("[a;++b;]p()".asFormula, "[x:=x+1; ++ {x'=-x}]y<=0".asFormula) // gives {a ~> x:=x+1, b ~> {x'=-x}, p() ~> y<=0} println(s)
3. val s = Matcher("[a;++b;]p(||)".asFormula, "[x:=x+1; ++ {x'=-x}]x>=0".asFormula) // gives {a ~> x:=x+1, b ~> {x'=-x}, p(||) ~> x>=0} println(s)
4. // will throw UnificationException val s = Matcher("[a;++b;]p(||)".asFormula, "[x:=x+1;{x'=-x}]x>=0".asFormula)
See also
UnificationException
UnificationMatch
SchematicUnificationMatch
final case class MultiRename(rens: Seq[(Variable, Variable)], semantic: Boolean = true) extends (Expression) ⇒ Expression with Product with Serializable
Uniformly rename multiple variables at once.
Uniformly rename multiple variables at once. Uniformly all occurrences of what and what' to repl and repl' and vice versa, for all (what,repl) in renames.
Performs semantic renaming, i.e. leaves program constants etc. unmodified.
semantic
true to also support program constants, predicationals etc and leaving them unmodified. 'false' to clash instead.

See also
edu.cmu.cs.ls.keymaerax.core.URename

sealed case class PosInExpr(pos: List[Int] = Nil) extends Product with Serializable

Positions identify subexpressions of an expression.

Positions identify subexpressions of an expression. A position is a finite sequence of binary numbers where

0 identifies the left or only subexpression of an expression and
1 identifies the right subexpression of an expression. For example, 0.1 is the right child of the left child. And, 0.1.0.0 is the left child of the left child of the right child of the left child.

See also: edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.positionOf()
Context.at()
Context.replaceAt()
Context.splitPos()
Augmentors

sealed trait Position extends AnyRef
Position at which formula and subexpresion ofa a sequent to apply a tactic.
Position at which formula and subexpresion ofa a sequent to apply a tactic.

To do
use AntePos and SuccPos directly instead of index etc.
Position should essentially become a nice type-preserving name for a pair of a SeqPos and a PosInExpr.
See also
edu.cmu.cs.ls.keymaerax.core.SeqPos
sealed trait RenUSubst extends (Expression) ⇒ Expression
Renaming Uniform Substitution, combining URename and USubst in a way that has both a direct application like apply functions of USubstRen as well as a translation to equivalent tactical/core prover operations.
Renaming Uniform Substitution, combining URename and USubst in a way that has both a direct application like apply functions of USubstRen as well as a translation to equivalent tactical/core prover operations.
Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution.

See also
edu.cmu.cs.ls.keymaerax.core.URename
edu.cmu.cs.ls.keymaerax.core.USubst
USubstRen
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()
abstract class RenUSubstBase extends RenUSubst
Base class for many common Renaming Uniform Substitution, combining URename and USubst.
Base class for many common Renaming Uniform Substitution, combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution.

See also
edu.cmu.cs.ls.keymaerax.core.URename
edu.cmu.cs.ls.keymaerax.core.USubst
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()
class RestrictedBiDiUnificationMatch extends FreshUnificationMatch
abstract class SchematicComposedUnificationMatch extends SchematicUnificationMatch
Generic schematic unification/matching algorithm for tactics.
Generic schematic unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher. Defined by recursive unification from compositions.
abstract class SchematicUnificationMatch extends BaseMatcher
Generic schematic unification/matching algorithm for tactics.
Generic schematic unification/matching algorithm for tactics. Their unify(shape, input) function matches second argument input against the pattern shape of the first argument, but not vice versa. Thus, the matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher that is defined by recursive unification from compositions.

Note
Central recursive unification implementation.
See also
UniformMatching
class SubstitutionHelper extends AnyRef
trait SuccPosition extends Position
A position guaranteed to identify a succedent position, so on the right-hand side of the sequent turnstile.
A position guaranteed to identify a succedent position, so on the right-hand side of the sequent turnstile.

See also
SuccPos
Sequent
trait TopAntePosition extends AntePosition with TopPosition
A top-level antecedent position
trait TopPosition extends Position
A position guaranteed to identify a top-level position
trait TopSuccPosition extends SuccPosition with TopPosition
A top-level succedent position
final case class URenSubstitutionPair(what: Expression, repl: Expression) extends Product with Serializable
Like a edu.cmu.cs.ls.keymaerax.core.SubstitutionPair replacing what~>repl but not checked for substitutability.
Like a edu.cmu.cs.ls.keymaerax.core.SubstitutionPair replacing what~>repl but not checked for substitutability.

See also
edu.cmu.cs.ls.keymaerax.core.SubstitutionPair
USubstRenOne
final class USubstAboveURen extends RenUSubstBase
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
```
s(RG) |- s(RD)
-------------- USubst
  RG  |- RD
-------------- URen
   G  |- D
```
Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
type USubstRen = USubstRenOne
Choice of standalone Renaming Uniform Substitution operation implementation
final case class USubstRenChurch(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst.
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst. This implementation uses Church-style uniform substitution implementation a la USubstChurch. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution, simultaneously.

Note
This implementation performs semantic renaming.
See also
edu.cmu.cs.ls.keymaerax.core.URename
edu.cmu.cs.ls.keymaerax.core.USubstChurch
MultiRename
USubstRenOne
final case class USubstRenOne(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst to uniformly substitute while simultaneously uniformly renaming multiple variables.
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst to uniformly substitute while simultaneously uniformly renaming multiple variables.
This implementation uses one-pass uniform substitution implementation a la USubstOne. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution, simultaneously.

Note
This implementation performs semantic renaming.
See also
edu.cmu.cs.ls.keymaerax.core.URename
edu.cmu.cs.ls.keymaerax.core.USubstOne
MultiRename
USubstRenChurch
class UnificationMatchBase extends SchematicComposedUnificationMatch
Generic base for unification/matching algorithm for tactics.
Generic base for unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast single-pass matcher.
class UnificationMatchUSubstAboveURen extends Matcher with Logging
class UniformMatcher extends UniformMatching
abstract class UniformMatching extends BaseMatcher
Uniform Matching algorithm for tactics by sweeping.
Uniform Matching algorithm for tactics by sweeping. Their unify(shape, input) function matches second argument input against the pattern shape of the first argument, but not vice versa. Uniform matching leaves input alone and only substitutes into shape. Fast single-pass matcher that is defined by sweeping uniform matching.
Sweeping Uniform Matching is provably sound and is fast but not necessarily complete.

Note
Central recursive unification implementation.
,
a more comprehensive unification matcher would be found when jointly abstracting replacements at join conflicts if those have a joint lattice sup/inf.
See also
SchematicUnificationMatch

Value Members

def USubstRen(subsDefsInput: Seq[(Expression, Expression)]): USubstRen
USubstRen factory method for standalone Renaming Uniform Substitution operation implementation, forwards to constructor.
object AntePosition
An antecedent position of a sequent indexed base 1, so positions 1, 2, 3, ...
object Augmentors
If imported, automatically augments core data structures with convenience wrappers for tactic purposes such as subexpression positioning, context splitting, and replacements.
If imported, automatically augments core data structures with convenience wrappers for tactic purposes such as subexpression positioning, context splitting, and replacements.
Example:
1. To use this implicit augmentation automatically, import it via
  import edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors._
  Then use it as if its methods were part of the data structures
  val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1") // will obtain the x>=1 part val someSub = f.sub(PosInExpr(1::1::Nil)) println(someSub) // construct x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x^2>y val other = f.replaceAt(PosInExpr(1::1::Nil), parser("x^2>y")) println(other)
See also
Context
object Context
Context management, position splitting, and extraction tools.
Context management, position splitting, and extraction tools. Useful for splitting a formula at a position into the subexpression at that position and the remaining context around it. Or for replacing a subexpression by another subexpression at all cost. Or for splitting a position into a formula position and a term position.
Example:
1. Split a formula at a position into subformula and its context
  val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1") // split f into context ctx and subformula g such that f is ctx{g} val (ctx,g) = Context.at(f, PosInExpr(1::1::Nil)) // x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]_ println(ctx) // x>=1 println(f) println(f + " is the same as " + ctx(g))
See also
PosInExpr
Augmentors
object DependencyAnalysis
Dependency Analysis For a set of output variables, determine the set of input variables across a hybrid program that could affect their values
object ExpressionTraversal
Generic traversal functionality for expressions for pre/post/infix traversal.
object FormulaTools extends Logging
Tactic tools for formula manipulation and extraction.
object LinearMatcher extends SchematicUnificationMatch
LinearMatcher(shape, input) matches second argument input against the LINEAR pattern shape of the first argument but not vice versa.
LinearMatcher(shape, input) matches second argument input against the LINEAR pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into linear shape.
Linear matchers require linear shapes, so no symbol can occur twice in the shape. If a symbol does occur twice, it is assumed that the identical match is found in all use cases, which is a strong assumption and can lead to unpredictable behavior. Implemented by a fast single pass. Possibly depends on using straight USubstRenOne
Examples:
1. Matching the formula on the right against a linear pattern shape
  LinearMatcher.unify("[a;](p(||)&q(||))".asFormula, "[x:=2*x;{x'=5}](0<=x&x>=y)".asFormula)
2. Except when lucky, nonlinear patterns will not be matched correctly by LinearMatcher even if they are unifiable.
  LinearMatcher.unify("p(f())<->[x:=f()]p(x)".asFormula, "(2*x)^2>=2*x<->[x:=2*x;]x^2>=x".asFormula)
object Matcher
object NonSubstUnificationMatch extends FreshUnificationMatch
Unify any term for variables in ODEs.
object PosInExpr extends Serializable
object Position
object ProvableHelper
Non-critical infrastructure to transform and substitute provables.
object RenUSubst
object RestrictedBiDiUnificationMatch extends RestrictedBiDiUnificationMatch
object StaticSemanticsTools
Additional tools read off from the static semantics for the tactics.
Additional tools read off from the static semantics for the tactics.

See also
edu.cmu.cs.ls.keymaerax.core.StaticSemantics
object Statistics
Formula, term, and tactic statistics.
object SubstitutionHelper
Created by smitsch on 2/19/15.
Created by smitsch on 2/19/15.

To do
generalize to replacing formula by formula, too.
object SuccPosition
A succedent position of a sequent indexed base 1, so positions 1, 2, 3, ...
object TreeForm
Represent terms as recursive lists of logical symbols.
Represent terms as recursive lists of logical symbols. This simplified structure is useful for certain analyses that treat all the operators in a relatively uniform way. This representation flattens the term's structure as much as possible (e.g. turning a+(b+c) into (a+b+c)), to make analyses that consider the depth of a term more meaningful. Created by bbohrer on 10/23/15.
object USubstRenChurch extends Serializable
object UnificationMatch extends FreshUnificationMatch
Unification/matching algorithm for tactics.
Unification/matching algorithm for tactics. Unify(shape, input) matches second argument input against the pattern shape of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape, i.e., gives a single-sided matcher.

See also
Matcher
object UnificationTools
object UniformMatcher extends UniformMatcher

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

KeYmaera X Kernel

Usage Overview

Constructing Proofs

Combining Proofs

Differential Dynamic Logic

Syntax

Static Semantics

Theorem Prover

Axioms

Uniform Substitutions

Sequent Proof Rules

Additional Capabilities

Stored Provable Mechanism

Error Reporting

Set Lattice

Overall Code Complexity

Lemma Mechanism

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

infrastruct 

package infrastruct

Type Members

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

infrastruct