I'm looking at
https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html and the proofs there don't seem to be working for me.
The non-temporal proofs seem to require a lot more hand-holding (i.e. introducing a lot more axioms) than what's being displayed on the page and I can't seem to prove the temporal proof with ls4 backend at all.
Is there something I'm missing here?
On a separate note the TLAPS module doesn't seem to be found by my TLA+ Toolbox installation and I had to inline it as a module in the same spec as Euclid.
I've included the module I ended up writing here (with the large number of axioms I had to introduce). The Correctness theorem still isn't accepted by tlapm.
------------------------------- MODULE Euclid -------------------------------
EXTENDS Integers, TLAPS
p | q == \E d \in 1..q : q = p * d
Divisors(q) == {d \in 1..q : d | q}
Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y
GCD(p, q) == Maximum(Divisors(p) \intersect Divisors(q))
Number == Nat \ {0}
CONSTANTS M, N
VARIABLES x, y
Init == (x = M) /\ (y = N)
Next ==
\/ /\ x < y
/\ y' = y - x
/\ x' = x
\/ /\ y < x
/\ x ' = x - y
/\ y' = y
Spec == Init /\ [][Next]_<<x, y>>
ResultCorrect == (x = y) => x = GCD(M, N)
InductiveInvariant ==
/\ x \in Number
/\ y \in Number
/\ GCD(x, y) = GCD(M, N)
ASSUME NumberAssumption == M \in Number /\ N \in Number
THEOREM InitProperty == Init => InductiveInvariant
BY NumberAssumption DEF Init, InductiveInvariant
AXIOM GCDProperty1 == \A p \in Number : GCD(p, p) = p
AXIOM GCDProperty2 == \A p, q \in Number : GCD(p, q) = GCD(q, p)
AXIOM GCDProperty3 == \A p, q \in Number : (p < q) => GCD(p, q) = GCD(p, q-p)
AXIOM LessThanIsAntiSymmetric == \A p, q \in Nat : (p < q) => ~(q < p)
AXIOM LessThanImpliesInequality == \A p, q \in Nat : (p < q) => p /= q
AXIOM NatsClosedUnderLessThanSubtraction == \A p, q \in Nat : (p < q) => q - p \in Nat
AXIOM NatIsSuperSetOfNumber == \A p \in Number : p \in Nat
AXIOM NatIsNumberIfNotZero == \A p \in Nat : p /= 0 => p \in Number
AXIOM LessThanRespectsZero == \A p, q \in Nat : q < p => p - q > 0
THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'
<1> SUFFICES ASSUME InductiveInvariant, Next
PROVE InductiveInvariant'
OBVIOUS
<1> USE DEF InductiveInvariant, Next
<1>1 (x < y) \/ (y < x)
OBVIOUS
<1>2 y \in Nat
BY NatIsSuperSetOfNumber
<1>3 x \in Nat
BY NatIsSuperSetOfNumber
<1>4 CASE x < y
<2>1 ~(y < x)
BY <1>2, <1>3, <1>4, LessThanIsAntiSymmetric
<2>2 (y - x \in Nat)
BY <1>4, NatsClosedUnderLessThanSubtraction, NatIsSuperSetOfNumber
<2>3 (y - x > 0)
BY <1>2, <1>3, <1>4, LessThanRespectsZero
<2>4 (y - x /= 0)
BY <2>3, LessThanImpliesInequality
<2>5 (y - x \in Number)
BY <2>2, NatIsNumberIfNotZero, <2>4
<2>6 (y - x \in Number) /\ ~(y < x)
BY <2>1, <2>5
<2> QED BY <1>4, <2>6, GCDProperty3
<1>5 CASE y < x
<2>1 ~(x < y)
BY <1>2, <1>3, <1>5, LessThanIsAntiSymmetric
<2>2 (x - y \in Nat)
BY <1>5, NatsClosedUnderLessThanSubtraction, NatIsSuperSetOfNumber
<2>3 (x - y > 0)
BY <1>2, <1>3, <1>5, LessThanRespectsZero
<2>4 (x - y /= 0)
BY <2>3, LessThanImpliesInequality
<2>5 (x - y \in Number)
BY <2>2, NatIsNumberIfNotZero, <2>4
<2>6 (x - y \in Number) /\ ~(x < y)
BY <2>1, <2>5
<2>7 GCD(y', x') = GCD(y, x)
BY <1>5, <2>1, GCDProperty3
<2> QED BY <1>5, <2>6, <2>7, GCDProperty2
<1>6 QED BY <1>1, <1>4, <1>5
THEOREM Correctness == Spec => []ResultCorrect
<1>1 InductiveInvariant /\ UNCHANGED <<x,y>> => InductiveInvariant' BY DEF InductiveInvariant
<1>2 Spec => []InductiveInvariant BY PTL, InitProperty, NextProperty, <1>1 DEF Spec
<1>3 InductiveInvariant => ResultCorrect BY GCDProperty1 DEF InductiveInvariant, ResultCorrect
<1> QED BY PTL, <1>2, <1>3
=============================================================================
\* Modification History
\* Last modified Tue Jul 30 21:04:57 EDT 2019 by changlin
\* Created Mon Jul 29 15:58:58 EDT 2019 by changlin
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/ee434bd4-83cd-0d61-498c-2fc24a984cb6%40changlinli.com.