ModelPlex ODE Euler-approximation (non-system)

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/ModelPlex.scala

@@ -162,23 +162,71 @@ object ModelPlex extends ModelPlexTrait {
     * @see [[createMonitorSpecificationConjecture]]
     * @return The tactic.
     */
-  def modelMonitorByChase: DependentPositionTactic = "modelMonitor" by ((pos: Position, seq: Sequent) => chase(3,3, (e:Expression) => e match {
+  lazy val modelMonitorByChase: DependentPositionTactic = modelMonitorByChase()
+  def modelMonitorByChase(ode: DependentPositionTactic = solveAllIn): DependentPositionTactic = "modelMonitor" by ((pos: Position, seq: Sequent) => chase(3,3, (e:Expression) => e match {
     // remove loops
     case Diamond(Loop(_), _) => "<*> approx" :: Nil
     // keep ODEs, solve later
     case Diamond(ODESystem(_, _), _) => Nil
     case _ => println("Chasing " + e.prettyString); AxiomIndex.axiomsFor(e)
-  })(pos) & solveAllIn(pos))
+  })(pos) & ode(pos))
 
   /** Solve all ODEs somewhere underneath pos */
-  private def solveAllIn: DependentPositionTactic = TacticFactory.anon((pos: Position, sequent: Sequent) => {
+  def solveAllIn: DependentPositionTactic = TacticFactory.anon((pos: Position, sequent: Sequent) => {
     val positions: List[BelleExpr] = mapSubpositions(pos, sequent, {
       case (Diamond(_: ODESystem, _), pp) => Some(AxiomaticODESolver.axiomaticSolve()(pp))
       case _ => None
     })
     positions.reduceRightOption[BelleExpr](_ & _).getOrElse(skip)
   })
 
+  /** Euler-approximates all ODEs somewhere underneat pos */
+  def eulerAllIn: DependentPositionTactic = "ANON" by ((pos: Position, sequent: Sequent) => {
+    //@todo evolution domain
+    val eulerAxiom = "<{x_'=f(x_)}>p(x_) <-> \\exists t_ (t_>=0 & \\forall e_ (e_>0 -> \\forall h0_ (h0_>0 -> \\exists h_ (0<h_&h_<h0_&<{x_:=x_+h_*f(x_);}*>(t_>=0 -> \\exists y_ (abs(x_-y_) < e_ & p(y_))) ))))".asFormula
+    //@todo systems as follows?
+    //val eulerAxiom = "<{x_'=f(x_),c&q(||)}>p(x_) <-> <{c,x_'=f(x_)&q(||)}>(\\exists t_ (t_>=0 & \\forall e_ (e_>0 -> \\forall h0_ (h0_>0 -> \\exists h_ (0<h_&h_<h0_&<{x_:=x_+h_*f(x);}*>(t_>=0 -> \\exists y_ (abs(x_-y_) < e_ & p(y_)) )))))".asFormula
+
+    val positions: List[BelleExpr] = mapSubpositions(pos, sequent, {
+      case (Diamond(_: ODESystem, _), pp) => Some(useAt(ProvableSig.startProof(eulerAxiom), PosInExpr(0::Nil))(pp))
+      case _ => None
+    })
+    positions.reduceRightOption[BelleExpr](_ & _).getOrElse(skip)
+  })
+
+  /** Unsound approximation step */
+  def flipUniversalEulerQuantifiers(fml: Formula): Formula = {
+    ExpressionTraversal.traverse(new ExpressionTraversalFunction() {
+      override def preF(p: PosInExpr, f: Formula): Either[Option[StopTraversal], Formula] = f match {
+        case Forall(e, Imply(pe, Forall(h0, Imply(ph0, ph)))) => Right(Exists(e, And(pe, Exists(h0, And(ph0,ph)))))
+        case _ => Left(None)
+      }
+    }, fml).getOrElse(fml)
+  }
+
+  /** Unrolls diamond loops */
+  def unrollLoop(n: Int): DependentPositionTactic = "ANON" by ((pos: Position, sequent: Sequent) => {
+    if (n <= 0) skip
+    else {
+      val positions: List[BelleExpr] = mapSubpositions(pos, sequent, {
+        case (Diamond(_: Loop, _), pp) =>
+          if (n == 1) Some(useAt("<*> approx")(pp))
+          else Some(useAt("<*> iterate", PosInExpr(0 :: Nil))(pp))
+        case _ => None
+      })
+      positions.reduceRightOption[BelleExpr](_ & _).getOrElse(skip) & unrollLoop(n-1)(pos)
+    }
+  })
+
+  /** Chases remaining assignments. */
+  lazy val chaseEulerAssignments: DependentPositionTactic = "ANON" by ((pos: Position, sequent: Sequent) => {
+    val positions: List[BelleExpr] = mapSubpositions(pos, sequent, {
+      case (Diamond(_: Assign, _), pp) => Some(chase(pp))
+      case _ => None
+    })
+    positions.lastOption.getOrElse(skip)
+  })
+
   /**
    * ModelPlex sequent-style synthesis technique, i.e., with branching so that the tactic can operate on top-level
    * operators. Operates on monitor specification conjectures.

keymaerax-webui/src/test/scala/btactics/ModelplexTacticTests.scala

@@ -147,6 +147,32 @@ class ModelplexTacticTests extends TacticTestBase {
     result.subgoals.head.succ should contain only "(-1<=fpost()&fpost()<=(m-l)/ep)&(0=cpost()&(lpost()=l&(fpost() < 0&(0=ep&l>=0|ep>0&l>=0)|(ep>=0&l>=0)&fpost()>0)|((fpost()=0&l=lpost())&ep>=0)&l>=0)|(cpost()>0&ep>=cpost())&(l>=0&(fpost()=0&l=lpost()|lpost()=cpost()*fpost()+l&fpost()>0)|(lpost()=cpost()*fpost()+l&fpost() < 0)&cpost()*fpost()+l>=0))".asFormula
   }
 
+  it should "find euler model monitor condition" in withMathematica { tool =>
+    val model = "true -> [x:=2;{x'=-3*x}]x>0".asFormula
+    val (modelplexInput, assumptions) = createMonitorSpecificationConjecture(model, Variable("x"))
+
+    val simplifier = SimplifierV3.simpTac(taxs=composeIndex(groundEqualityIndex,defaultTaxs))
+    val tactic = ModelPlex.modelMonitorByChase(ModelPlex.eulerAllIn)(1) & Idioms.<(
+      ModelPlex.unrollLoop(2)(1) & ModelPlex.chaseEulerAssignments(1),
+      skip)
+    val result = proveBy(modelplexInput, tactic)
+
+    result.subgoals should have size 2
+    result.subgoals.head.ante shouldBe empty
+    result.subgoals.head.succ should contain only "\\forall x (x=2->\\exists t_ (t_>=0&\\forall e_ (e_>0->\\forall h0_ (h0_>0->\\exists h_ (0 < h_&h_ < h0_&((t_>=0->\\exists y_ (abs(x-y_) < e_&xpost()=y_))|(t_>=0->\\exists y_ (abs(x+h_*(-3*x)+h_*(-3*(x+h_*(-3*x)))-y_) < e_&xpost()=y_))))))))".asFormula
+    // don't care about second branch, that's only because euler formula is not an axiom
+
+    //@note unsound approximation step
+    val flipped = ModelPlex.flipUniversalEulerQuantifiers(result.subgoals.head.succ.head)
+    flipped shouldBe "\\forall x (x=2->\\exists t_ (t_>=0&\\exists e_ (e_>0&\\exists h0_ (h0_>0&\\exists h_ (0 < h_&h_ < h0_&((t_>=0->\\exists y_ (abs(x-y_) < e_&xpost()=y_))|(t_>=0->\\exists y_ (abs(x+h_*(-3*x)+h_*(-3*(x+h_*(-3*x)))-y_) < e_&xpost()=y_))))))))".asFormula
+
+    val simplified = proveBy(flipped, ModelPlex.optimizationOneWithSearch(tool, assumptions)(1) & simplifier(1))
+    simplified.subgoals should have size 1
+    simplified.subgoals.head.ante shouldBe empty
+    //@todo auto-generated post names are somewhat weird here for parameters t, e, h0, h
+    simplified.subgoals.head.succ should contain only "tpost_0()>=0&epost_0()>0&h0post_0()>0&0 < hpost_0()&hpost_0() < h0post_0()&(abs(2-xpost()) < epost_0()|abs(2+hpost_0()*-6+hpost_0()*(-3*(2+hpost_0()*-6))-xpost()) < epost_0())".asFormula
+  }
+
   it should "find correct model monitor condition by chase" in withMathematica { tool =>
     val in = getClass.getResourceAsStream("/examples/casestudies/modelplex/watertank/watertank.key")
     val model = KeYmaeraXProblemParser(io.Source.fromInputStream(in).mkString)