[tlaplus] Trying to follow along with INRIA's TLAPS tutorial

[Changlin Li <mail@xxxxxxxxxxxxxx>]

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.