Skip to content

Commit 01a56e1

Browse files
EnguerrandPrebetEnguerrandPrebet
committed
Fix and finish moveRandom
1 parent 659e7a4 commit 01a56e1

2 files changed

Lines changed: 192 additions & 139 deletions

File tree

‎keymaerax-core/src/main/scala/org/keymaerax/btactics/Refactor.scala‎

Lines changed: 175 additions & 108 deletions
Original file line numberDiff line numberDiff line change
@@ -564,6 +564,181 @@ object Refactor {
564564
)
565565
}
566566

567+
/**
568+
* Given a program `a;x:=*`, adds a `x:=*` within `a` at position `pos`
569+
* @note
570+
* `pos` refers to the position in `a;x:=*`, not in `a`
571+
* @see
572+
* [[moveRandomIn]] and [[moveRandomOut]]
573+
*/
574+
def moveRandom(a: Program, pos: PosInExpr): ProvableSig = {
575+
a match {
576+
case Compose(b, AssignAny(x)) if pos.head == 0 =>
577+
b.at(pos.child) match {
578+
case (ctx, c: Program) =>
579+
val a_updated = Compose(ctx(Compose(c, AssignAny(x))), AssignAny(x))
580+
proveBy(
581+
ProgramEquivalence(a_updated, a),
582+
moveRandomAux(ctx, c, x, PosInExpr(0 :: Nil)) & useAt(prgEqRefl)(1),
583+
)
584+
case (ctx, e) => ???
585+
}
586+
587+
case _ => ???
588+
}
589+
}
590+
591+
def moveRandomAux(ctx: Context[Program], p: Program, x: Variable, pos: PosInExpr): BelleExpr = {
592+
ctx.ctx match {
593+
case DotProgram =>
594+
val ax = x match {
595+
case _: BaseVariable => prgEqRandomIdem
596+
case _: DifferentialSymbol => prgEqRandomDIdem
597+
}
598+
useAt(refSeqAssoc)(1, pos) & useAt(ax)(1, pos ++ 1)
599+
case Choice(a, b) =>
600+
val (nextPrg, nextPos) =
601+
if (!symbols(a).contains(DotProgram)) { (b, 1) }
602+
else if (!symbols(b).contains(DotProgram)) { (a, 0) }
603+
else ???
604+
useAt(refDistrR)(1, pos) & moveRandomAux(Context(nextPrg), p, x, pos ++ nextPos) &
605+
useAt(refDistrR, PosInExpr(0 :: Nil))(1, pos)
606+
case Compose(a, c) if !symbols(a).contains(DotProgram) =>
607+
useAt(refSeqAssoc)(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 1) &
608+
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos)
609+
case Compose(c, a) if !symbols(a).contains(DotProgram) =>
610+
val ax = x match {
611+
case _: BaseVariable => refAnyFresh
612+
case _: DifferentialSymbol => refAnyDFresh
613+
}
614+
useAt(refSeqAssoc)(1, pos) & useAt(ax, PosInExpr(1 :: Nil))(1, pos ++ 1) &
615+
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 0) &
616+
useAt(refSeqAssoc)(1, pos) & useAt(ax)(1, pos ++ 1) & useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos)
617+
case Loop(c) =>
618+
val axLoop = x match {
619+
case _: BaseVariable => moveRandomLoop
620+
case _: DifferentialSymbol => moveRandomLoopD
621+
}
622+
val assgn = AssignAny(x)
623+
val prg = Context(c)(Compose(p, assgn)) // C(p;x:=*)
624+
625+
// x:=*;C(p;x:=*)*;x:=* == C(p;x:=*)*;x:=*
626+
val fuseBefore = fuseRandom(Loop(prg), x)
627+
// (C(p;x:=*);x:=*)*;x:=* == (C(p;x:=*))*;x:=*
628+
val loopCommBefore = proveBy(
629+
ProgramEquivalence(Compose(Loop(Compose(prg, assgn)), assgn), Compose(Loop(prg), assgn)),
630+
useAt(axLoop, PosInExpr(1 :: Nil))(1) & G(1) & G(1) & byUS(fuseBefore),
631+
)
632+
633+
// x:=*;C(p)*;x:=* == C(p)*;x:=*
634+
val fuseAfter = fuseRandom(Loop(Context(c)(p)), x)
635+
// (C(p);x:=*)*;x:=* == (C(p))*;x:=*
636+
val loopCommAfter = proveBy(
637+
ProgramEquivalence(Compose(Loop(Compose(Context(c)(p), assgn)), assgn), Compose(ctx(p), assgn)),
638+
useAt(axLoop, PosInExpr(1 :: Nil))(1) & G(1) & G(1) & byUS(fuseAfter),
639+
)
640+
// Merging the proof
641+
useAt(loopCommBefore, PosInExpr(1 :: Nil))(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 0 ++ 0) &
642+
useAt(loopCommAfter, PosInExpr(0 :: Nil))(1, pos)
643+
case _ => ???
644+
}
645+
}
646+
647+
/**
648+
* For a subprogram `a;x:=*` at position `posOut`, copies `x:=*` inside `a` just after the position `posIn`
649+
* @note
650+
* if successful, the nondeterministic assignment will be at `posOut ++ posIn ++ (1 :: Nil)`
651+
*/
652+
def moveRandomIn(posIn: PosInExpr): DependentPositionWithAppliedInputTactic = "moveRandomIn".byWithInputs(
653+
List(posIn),
654+
(posOut: Position, sequent: Sequent) => {
655+
sequent.at(posOut) match {
656+
case (_, a: Program) =>
657+
val pr = moveRandom(a, posIn)
658+
useAt(pr, PosInExpr(1 :: Nil))(posOut)
659+
case _ => ???
660+
}
661+
},
662+
)
663+
664+
@Derivation
665+
val moveRandomInInfo: PositionTacticInfo = PositionTacticInfo.create(
666+
name = "moveRandomIn",
667+
displayName = Some("Move Nondeterministic In"),
668+
displayLevel = DisplayLevel.Menu,
669+
displayConclusion = "__C(a);x:=*__ == C(a;x:=*);x:=*",
670+
constructor = TacticConstructor1.create(PosInExprArg("pos"))(moveRandomIn),
671+
)
672+
673+
/**
674+
* For a subprogram `C(a;x:=*);x:=*` at position `posOut`, removes the `x:=*` after `a`
675+
* @note
676+
* `posIn` refers to the position of the hole of `C`. If successful, `a` will be a position `posOut ++ posIn`.
677+
*/
678+
def moveRandomOut(posIn: PosInExpr): DependentPositionWithAppliedInputTactic = "moveRandomOut".byWithInputs(
679+
List(posIn),
680+
(posOut: Position, sequent: Sequent) => {
681+
sequent.at(posOut) match {
682+
case (_, a: Program) =>
683+
// Remove AssignAny
684+
val resPrg = a.at(posIn) match {
685+
case (ctx, Compose(b, AssignAny(_))) => ctx(b)
686+
case _ => ???
687+
}
688+
val pr = moveRandom(resPrg, posIn)
689+
useAt(pr, PosInExpr(0 :: Nil))(posOut)
690+
case _ => ???
691+
}
692+
},
693+
)
694+
695+
@Derivation
696+
val moveRandomOutInfo: PositionTacticInfo = PositionTacticInfo.create(
697+
name = "moveRandomOut",
698+
displayName = Some("Move Nondeterministic Out"),
699+
displayLevel = DisplayLevel.Menu,
700+
displayConclusion = "C(a);x:=* == __C(a;x:=*);x:=*__",
701+
constructor = TacticConstructor1.create(PosInExprArg("pos"))(moveRandomOut),
702+
)
703+
704+
lazy val moveRandomLoop: ProvableSig = proveBy(
705+
"[{a{|^@|};x_:=*;}*][a{|^@|};]{x_:=*;{a{|^@|};}*;x_:=*;}=={{a{|^@|};}*x_:=*;}->{a{|^@|};x_:=*;}*;x_:=*; == {a{|^@|};}*;x_:=*;"
706+
.asFormula,
707+
implyR(1) & useAt(refAntiSym)(1) & andR(1) & Idioms.<(
708+
refTrans("{a{|^@|};x_:=*;}*{a{|^@|};}*x_:=*;".asProgram)(1) & andR(1) & Idioms.<(
709+
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 1 :: 0 :: Nil) & useAt(hideChoiceR)(1, 1 :: 1 :: 0 :: Nil) &
710+
useAt(refSeqIdL)(1, 1 :: 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
711+
useAt(refLoopL)(1) & implyRi & useAt(K)(1) & G(1) & implyR(1) & useAt(refSeqAssoc)(1, 0 :: Nil) &
712+
refTrans("a{|^@|};{a{|^@|};}*;x_:=*;".asProgram)(1) & andR(1) & Idioms.<(
713+
focus(1, 0 :: 1 :: Nil) & useAt(refEq)(-1, 1 :: Nil) & id,
714+
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 0 :: Nil) & useAt(hideChoiceL)(1, 1 :: 0 :: Nil) &
715+
useAt(refSeqAssoc)(1, 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
716+
),
717+
),
718+
useAt(skipRandom)(1, 1 :: 0 :: 0 :: 1 :: Nil) & useAt(refSeqIdR)(1, 1 :: 0 :: 0 :: Nil) &
719+
cohide(1) & useAt(refRefl)(1),
720+
),
721+
)
722+
723+
lazy val moveRandomLoopD: ProvableSig = proveBy(
724+
"[{a{|^@|};x_':=*;}*][a{|^@|};]{x_':=*;{a{|^@|};}*;x_':=*;}=={{a{|^@|};}*x_':=*;}->{a{|^@|};x_':=*;}*;x_':=*; == {a{|^@|};}*;x_':=*;"
725+
.asFormula,
726+
implyR(1) & useAt(refAntiSym)(1) & andR(1) & Idioms.<(
727+
refTrans("{a{|^@|};x_':=*;}*{a{|^@|};}*x_':=*;".asProgram)(1) & andR(1) & Idioms.<(
728+
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 1 :: 0 :: Nil) & useAt(hideChoiceR)(1, 1 :: 1 :: 0 :: Nil) &
729+
useAt(refSeqIdL)(1, 1 :: 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
730+
useAt(refLoopL)(1) & implyRi & useAt(K)(1) & G(1) & implyR(1) & useAt(refSeqAssoc)(1, 0 :: Nil) &
731+
refTrans("a{|^@|};{a{|^@|};}*;x_':=*;".asProgram)(1) & andR(1) & Idioms.<(
732+
focus(1, 0 :: 1 :: Nil) & useAt(refEq)(-1, 1 :: Nil) & id,
733+
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 0 :: Nil) & useAt(hideChoiceL)(1, 1 :: 0 :: Nil) &
734+
useAt(refSeqAssoc)(1, 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
735+
),
736+
),
737+
useAt(skipRandomD)(1, 1 :: 0 :: 0 :: 1 :: Nil) & useAt(refSeqIdR)(1, 1 :: 0 :: 0 :: Nil) &
738+
cohide(1) & useAt(refRefl)(1),
739+
),
740+
)
741+
567742
/**
568743
* Generalisation of [[refAnyFresh]] to the specific cases where the only occurrences of `x` are of the form:
569744
* - `x:=*`
@@ -678,112 +853,4 @@ object Refactor {
678853
}
679854
}
680855
}
681-
682-
lazy val randomLoop: ProvableSig = proveBy(
683-
"[{a_{|^@|};x_:=*;}*][a_{|^@|};]{x_:=*;{a_{|^@|};}*}=={{a_{|^@|};}*x_:=*;}->{a_{|^@|};x_:=*;}*;x_:=*; == {a_{|^@|};}*;x_:=*;"
684-
.asFormula,
685-
implyR(1) & useAt(refAntiSym)(1) & andR(1) & Idioms.<(
686-
refTrans("{a_{|^@|};x_:=*;}*{a_{|^@|};}*x_:=*;".asProgram)(1) & andR(1) & Idioms.<(
687-
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 1 :: 0 :: Nil) & useAt(hideChoiceR)(1, 1 :: 1 :: 0 :: Nil) &
688-
useAt(refSeqIdL)(1, 1 :: 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
689-
useAt(refLoopL)(1) & implyRi & useAt(K)(1) & G(1) & implyR(1) & useAt(refSeqAssoc)(1, 0 :: Nil) &
690-
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: 1 :: Nil) &
691-
refTrans("a_{|^@|};{{a_{|^@|};}*x_:=*;}x_:=*;".asProgram)(1) & andR(1) & Idioms.<(
692-
focus(1, 0 :: 1 :: 0 :: Nil) & useAt(refEq)(-1, 1 :: Nil) & id,
693-
useAt(refSeqAssoc)(1, 0 :: 1 :: Nil) & useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: Nil) &
694-
useAt(prgEqRandomIdem)(1, 0 :: 1 :: Nil) & useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 0 :: Nil) &
695-
useAt(hideChoiceL)(1, 1 :: 0 :: Nil) & cohide(1) & useAt(refRefl)(1),
696-
),
697-
),
698-
useAt(refSeqIdR, PosInExpr(1 :: Nil))(1, 0 :: 0 :: 0 :: Nil) & focus(1, List(0, 0, 0, 1)) &
699-
useAt(skipRandom)(1, 1 :: 1 :: 1 :: Nil) & G(1) & G(1) & useAt(refRefl)(1),
700-
),
701-
)
702-
703-
lazy val randomDLoop: ProvableSig = proveBy(
704-
"[{a_{|^@|};x_':=*;}*][a_{|^@|};]{x_':=*;{a_{|^@|};}*}=={{a_{|^@|};}*x_':=*;}->{a_{|^@|};x_':=*;}*;x_':=*; == {a_{|^@|};}*;x_':=*;"
705-
.asFormula,
706-
implyR(1) & useAt(refAntiSym)(1) & andR(1) & Idioms.<(
707-
refTrans("{a_{|^@|};x_':=*;}*{a_{|^@|};}*x_':=*;".asProgram)(1) & andR(1) & Idioms.<(
708-
useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 1 :: 0 :: Nil) & useAt(hideChoiceR)(1, 1 :: 1 :: 0 :: Nil) &
709-
useAt(refSeqIdL)(1, 1 :: 1 :: Nil) & cohide(1) & useAt(refRefl)(1),
710-
useAt(refLoopL)(1) & implyRi & useAt(K)(1) & G(1) & implyR(1) & useAt(refSeqAssoc)(1, 0 :: Nil) &
711-
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: 1 :: Nil) &
712-
refTrans("a_{|^@|};{{a_{|^@|};}*x_':=*;}x_':=*;".asProgram)(1) & andR(1) & Idioms.<(
713-
focus(1, 0 :: 1 :: 0 :: Nil) & useAt(refEq)(-1, 1 :: Nil) & id,
714-
useAt(refSeqAssoc)(1, 0 :: 1 :: Nil) & useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: Nil) &
715-
useAt(prgEqRandomDIdem)(1, 0 :: 1 :: Nil) & useAt(refUnfoldL, PosInExpr(1 :: Nil))(1, 1 :: 0 :: Nil) &
716-
useAt(hideChoiceL)(1, 1 :: 0 :: Nil) & cohide(1) & useAt(refRefl)(1),
717-
),
718-
),
719-
useAt(refSeqIdR, PosInExpr(1 :: Nil))(1, 0 :: 0 :: 0 :: Nil) & focus(1, List(0, 0, 0, 1)) &
720-
useAt(skipRandomD)(1, 1 :: 1 :: 1 :: Nil) & G(1) & G(1) & useAt(refRefl)(1),
721-
),
722-
)
723-
724-
/** Given a program `a;x:=*`, adds a `x:=*` within `a` at position `pos` */
725-
def moveRandom(a: Program, pos: PosInExpr): ProvableSig = {
726-
a match {
727-
case Compose(b, AssignAny(x)) if pos.head == 0 =>
728-
b.at(pos.child) match {
729-
case (ctx, c: Program) =>
730-
val a_updated = Compose(ctx(Compose(c, AssignAny(x))), AssignAny(x))
731-
proveBy(
732-
ProgramEquivalence(a_updated, a),
733-
moveRandomAux(ctx, c, x, PosInExpr(0 :: Nil)) & useAt(prgEqRefl)(1),
734-
)
735-
case (ctx, e) => ???
736-
}
737-
738-
case _ => ???
739-
}
740-
}
741-
742-
def moveRandomAux(ctx: Context[Program], p: Program, x: Variable, pos: PosInExpr): BelleExpr = {
743-
ctx.ctx match {
744-
case DotProgram =>
745-
val ax = x match {
746-
case _: BaseVariable => prgEqRandomIdem
747-
case _: DifferentialSymbol => prgEqRandomDIdem
748-
}
749-
useAt(refSeqAssoc)(1, pos) & useAt(ax)(1, pos ++ 1)
750-
case Choice(a, b) =>
751-
val (nextPrg, nextPos) =
752-
if (!symbols(a).contains(DotProgram)) { (b, 1) }
753-
else if (!symbols(b).contains(DotProgram)) { (a, 0) }
754-
else ???
755-
useAt(refDistrR)(1, pos) & moveRandomAux(Context(nextPrg), p, x, pos ++ nextPos) &
756-
useAt(refDistrR, PosInExpr(0 :: Nil))(1, pos)
757-
case Compose(a, c) if !symbols(a).contains(DotProgram) =>
758-
useAt(refSeqAssoc)(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 1) &
759-
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos)
760-
case Compose(c, a) if !symbols(a).contains(DotProgram) =>
761-
val ax = x match {
762-
case _: BaseVariable => refAnyFresh
763-
case _: DifferentialSymbol => refAnyDFresh
764-
}
765-
useAt(refSeqAssoc)(1, pos) & useAt(ax, PosInExpr(1 :: Nil))(1, pos ++ 1) &
766-
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 0) &
767-
useAt(refSeqAssoc)(1, pos) & useAt(ax)(1, pos ++ 1) & useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, pos)
768-
case Loop(c) =>
769-
val (axLoop, axFresh) = x match {
770-
case _: BaseVariable => (randomLoop, refAnyFresh)
771-
case _: DifferentialSymbol => (randomDLoop, refAnyDFresh)
772-
}
773-
val assgn = AssignAny(x)
774-
val prg = Context(c)(Compose(p, assgn))
775-
val test = refAnyGenAux(Loop(prg), x)
776-
val loopCommBefore = proveBy(
777-
ProgramEquivalence(Compose(Loop(Compose(prg, assgn)), assgn), Compose(Loop(prg), assgn)),
778-
useAt(axLoop, PosInExpr(1 :: Nil))(1) & G(1) & G(1) & byUS(test),
779-
)
780-
val loopCommAfter = proveBy(
781-
ProgramEquivalence(Compose(Loop(Compose(Context(c)(p), assgn)), assgn), Compose(ctx(p), assgn)),
782-
useAt(axLoop, PosInExpr(1 :: Nil))(1) & G(1) & G(1) & byUS(axFresh),
783-
)
784-
useAt(loopCommBefore, PosInExpr(1 :: Nil))(1, pos) & moveRandomAux(Context(c), p, x, pos ++ 0 ++ 0) &
785-
useAt(loopCommAfter, PosInExpr(0 :: Nil))(1, pos)
786-
case _ => ???
787-
}
788-
}
789856
}

‎keymaerax-webui/src/test/scala/org/keymaerax/btactics/RefactorTests.scala‎

Lines changed: 17 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,6 @@ class RefactorTests extends TacticTestBase {
2626
congrImpR,
2727
congrRefL,
2828
congrRefR,
29-
randomLoop,
30-
randomDLoop,
31-
prgEqLoopComm,
32-
prgEqIsolComm,
33-
prgEqIsolCommFix,
3429
prgEqBoundRandom,
3530
prgEqBoundRandomD,
3631
prgEqBoundAssign,
@@ -39,6 +34,11 @@ class RefactorTests extends TacticTestBase {
3934
fuseLoopAuxD,
4035
fuseLoop,
4136
fuseLoopD,
37+
moveRandomLoop,
38+
moveRandomLoopD,
39+
prgEqLoopComm,
40+
prgEqIsolComm,
41+
prgEqIsolCommFix,
4242
)
4343
axioms.map(axiom => axiom.isProved shouldBe true)
4444
}
@@ -193,9 +193,6 @@ class RefactorTests extends TacticTestBase {
193193
pr4.proved shouldBe "==> {{x:=*;y:=*;++x:=0;z:=*;}*z:=*;}=={{x:=*;y:=*;++x:=0;}*z:=*;}".asSequent
194194
}
195195

196-
// Ghost existential: {c & p};x':=*;x:=* == x:=f();{c,x'=g(x)&p};x':=*;x:=*
197-
// use refDE to use line above for x'
198-
199196
"refAnyGenAux" should "prove correct program" in {
200197
val pr = refAnyGenAux("x:=*;y:=*; ++ x:=0;".asProgram, "z".asVariable)
201198
pr.proved shouldBe "==> z:=*;{x:=*;y:=*;++x:=0;} == {x:=*;y:=*;++x:=0;}z:=*;".asSequent
@@ -245,29 +242,18 @@ class RefactorTests extends TacticTestBase {
245242
pr4.proved shouldBe
246243
"==> t':=*;{x:=0;t:=0;{x'=x,t'=1};t':=*;}*t':=*; == {x:=0;t:=0;{x'=x,t'=1};t':=*;}*t':=*;".asSequent
247244
}
248-
249-
"refDG" should "be applicable locally" in {
250-
val pr = ProvableSig
251-
.startPlainProof("{x:=0;{x'=1};}*;t:=*;t':=*; == {x:=0;t:=0;{x'=1,t'=1};}*;t:=*;t':=*;".asFormula)
252-
val move = moveRandom("{x:=0;{x'=1};}*;t:=*;".asProgram, PosInExpr(0 :: 0 :: 1 :: Nil))
253-
move.proved shouldBe "==> {x:=0;{x'=1};t:=*;}*;t:=*; == {x:=0;{x'=1};}*;t:=*;".asSequent
254-
val pr2 = pr
255-
.apply(useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: Nil), 0)
256-
.apply(useAt(move, PosInExpr(1 :: Nil))(1, 0 :: 0 :: Nil), 0)
257-
pr2.subgoals.head shouldBe
258-
"==> {{x:=0;{x'=1};t:=*;}*;t:=*;}t':=*; == {x:=0;t:=0;{x'=1,t'=1};}*;t:=*;t':=*;".asSequent
259-
val move2 = moveRandom("{{x:=0;{x'=1};t:=*;}*;t:=*;}t':=*;".asProgram, PosInExpr(List(0, 0, 0, 1, 0)))
260-
move2.proved shouldBe
261-
"==> {{x:=0;{{x'=1};t':=*;}t:=*;}*;t:=*;}t':=*; == {{x:=0;{x'=1};t:=*;}*;t:=*;}t':=*;".asSequent
262-
val pr3 = pr2
263-
.apply(useAt(move2, PosInExpr(1 :: Nil))(1, 0 :: Nil), 0)
264-
.apply(useAt(refSeqAssoc)(1, 0 :: Nil), 0)
265-
.apply(useAt(refSeqAssoc)(1, 0 :: 0 :: 0 :: 1 :: Nil), 0)
266-
pr3.subgoals.head shouldBe
267-
"==> {x:=0;{x'=1};t':=*;t:=*;}*;t:=*;t':=*; == {x:=0;t:=0;{x'=1,t'=1};}*;t:=*;t':=*;".asSequent
268-
val pr4 = proveBy(pr3, refDGCst("t".asVariable, "0".asTerm, "1".asTerm)(1, 0 :: 0 :: 0 :: 1 :: Nil))
269-
pr4.subgoals.head shouldBe
270-
"==> {x:=0;t:=0;{x'=1,t'=1};t':=*;t:=*;}*;t:=*;t':=*; == {x:=0;t:=0;{x'=1,t'=1};}*;t:=*;t':=*;".asSequent
245+
"refDGCst" should "be applicable locally by moving nondeterministic assignment" in {
246+
val pr = TactixLibrary.proveBy(
247+
"{x:=0;{x'=1};}*;t:=*;t':=*; == {x:=0;t:=0;{x'=1,t'=1};}*;t:=*;t':=*;".asFormula,
248+
useAt(refSeqAssoc, PosInExpr(0 :: Nil))(1, 0 :: Nil) &
249+
moveRandomIn(PosInExpr(0 :: 0 :: 1 :: Nil))(1, 0 :: 0 :: Nil) &
250+
moveRandomIn(PosInExpr(List(0, 0, 0, 1, 1)))(1, 0 :: Nil) &
251+
refDGCst("t".asVariable, "0".asTerm, "1".asTerm)(1, 0 :: 0 :: 0 :: 0 :: 1 :: Nil) &
252+
moveRandomOut(PosInExpr(List(0, 0, 0, 1, 1, 1)))(1, 0 :: Nil) &
253+
moveRandomOut(PosInExpr(List(0, 0, 1, 1)))(1, 0 :: 0 :: Nil) & useAt(refSeqAssoc)(1, 0 :: Nil) &
254+
useAt(prgEqRefl)(1),
255+
)
256+
pr.isProved shouldBe true
271257
}
272258

273259
}

0 commit comments

Comments
 (0)