For reference, here's the full spec with what I'm trying to prove:
--------------------------- MODULE DieHarderBook ---------------------------
EXTENDS Integers, GCD, FiniteSetTheorems
Min(n,m) == IF n < m THEN n ELSE m
CONSTANTS Goal, Jugs, Capacity
ASSUME CONSTANTS_OK == /\ Goal \in Nat
/\ Capacity \in [Jugs -> Nat \ {0}]
ASSUME TRANSITIVITY_NAT == \A p,q,r \in Nat : p \leq q /\ q \leq r => p \leq r
ASSUME SUB_DECREMENT == \A a,b \in Int : b \geq 0 => a-b \leq a
ASSUME MIN_STAYS_INT == \A a,b \in Int : Min(a,b) \in Int
(***************************************************************************
--fair algorithm DieHarder {
variable injug = [j \in Jugs |-> 0] ;
{ while (~\E j \in Jugs : injug[j] = Goal)
{ either with (j \in Jugs) \* fill jug j
{ injug[j] := Capacity[j] }
or with (j \in Jugs) \* empty jug j
{ injug[j] := 0 }
or with (j \in Jugs, k \in Jugs \ {j}) \* pour from jug j to jug k
{ with ( poured =
Min(injug[j] + injug[k], Capacity[k]) - injug[k] )
{ injug[j] := injug[j] - poured ||
injug[k] := injug[k] + poured
}
}
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "b157a2cd" /\ chksum(tla) = "88d18fa9")
VARIABLES injug, pc
vars == << injug, pc >>
Init == (* Global variables *)
/\ injug = [j \in Jugs |-> 0]
/\ pc = "Lbl_1"
Lbl_1 == \/ /\ ~\E j \in Jugs : injug[j] = Goal
/\ pc = "Lbl_1"
/\ pc' = "Lbl_1"
/\ \/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = Capacity[j]]
\/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
\/ /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
\/ /\ pc' = "Done"
/\ UNCHANGED <<injug>>
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
Termination == <>(pc = "Done")
\* END TRANSLATION
-----------------------------------------------------------------------------------------------------------------------
TypeOK == /\ injug \in [Jugs -> Nat]
/\ \A j \in Jugs : injug[j] \leq Capacity[j]
CommonDivisorsOfSet(S) == {d \in Int : \A s \in S : Divides(d,s)}
IsSetGCD(g,S) == g \in CommonDivisorsOfSet(S) /\ \A d \in CommonDivisorsOfSet(S) : g \geq d
SetGCDDividesAll == \A j \in Jugs : \A g \in Nat : IsSetGCD(g, {Capacity[k] : k \in Jugs}) => Divides(g, injug[j])
InductiveInvariantSetGCDDividesAll == /\ TypeOK
/\ SetGCDDividesAll
THEOREM Spec => []SetGCDDividesAll
<1>1. Init => InductiveInvariantSetGCDDividesAll
<2> SUFFICES ASSUME Init
PROVE InductiveInvariantSetGCDDividesAll
OBVIOUS
<2>1. TypeOK
PROOF BY CONSTANTS_OK DEF Init, TypeOK
<2>2. SetGCDDividesAll
<3> SUFFICES ASSUME NEW j \in Jugs,
NEW g \in Nat,
IsSetGCD(g, {Capacity[k] : k \in Jugs})
PROVE Divides(g, injug[j])
BY DEF SetGCDDividesAll
<3>1. Init => \A k \in Jugs : injug[k] = 0
PROOF BY DEF Init
<3>2. \A n \in Nat : Divides(n,0)
<4> SUFFICES ASSUME NEW n \in Nat
PROVE Divides(n,0)
OBVIOUS
<4>1. 0 = n * 0
OBVIOUS
<4>2. 0 \in Int
OBVIOUS
<4> QED
PROOF BY <4>1, <4>2 DEF Divides
<3> QED
PROOF BY <3>1, <3>2
<2>3. QED
BY <2>1, <2>2 DEF InductiveInvariantSetGCDDividesAll
<1>2. InductiveInvariantSetGCDDividesAll /\ [Next]_vars => InductiveInvariantSetGCDDividesAll '
<2> SUFFICES ASSUME InductiveInvariantSetGCDDividesAll,
[Next]_vars
PROVE InductiveInvariantSetGCDDividesAll '
OBVIOUS
<2>1. CASE Lbl_1
<3>1. TypeOK'
<4>1. ASSUME /\ ~\E j \in Jugs : injug[j] = Goal
/\ pc = "Lbl_1"
/\ pc' = "Lbl_1"
/\ \/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = Capacity[j]]
\/ /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
\/ /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
PROVE TypeOK'
<5>1. ASSUME /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = Capacity[j]]
PROVE TypeOK'
<5>2. ASSUME /\ \E j \in Jugs:
injug' = [injug EXCEPT ![j] = 0]
PROVE TypeOK'
<5>3. ASSUME /\ \E j \in Jugs:
\E k \in Jugs \ {j}:
LET poured == Min(injug[j] + injug[k], Capacity[k]) - injug[k] IN
injug' = [injug EXCEPT ![j] = injug[j] - poured,
![k] = injug[k] + poured]
PROVE TypeOK'
<5>4. QED
BY <4>1, <5>1, <5>2, <5>3
<4>2. ASSUME /\ pc' = "Done"
/\ UNCHANGED <<injug>>
PROVE TypeOK'
<5>1. injug' = injug
BY UNCHANGED <<injug>> DEF vars
<5>2. injug \in [Jugs -> Nat]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll
<5>3. \A j \in Jugs : injug[j] =< Capacity[j]
BY DEF TypeOK, InductiveInvariantSetGCDDividesAll
<5> QED
BY <5>1, <5>2, <5>3 DEF TypeOK
<4>3. QED
BY <2>1, <4>1, <4>2 DEF Lbl_1
<3>2. SetGCDDividesAll'
<3>3. QED
BY <3>1, <3>2 DEF InductiveInvariantSetGCDDividesAll
<2>2. CASE Terminating
BY Terminating DEF InductiveInvariantSetGCDDividesAll, vars, TypeOK, SetGCDDividesAll, Terminating
<2>3. CASE UNCHANGED vars
BY UNCHANGED vars DEF InductiveInvariantSetGCDDividesAll, vars, TypeOK, SetGCDDividesAll
<2>4. QED
BY <2>1, <2>2, <2>3 DEF Next
<1>3. InductiveInvariantSetGCDDividesAll => SetGCDDividesAll
BY DEF InductiveInvariantSetGCDDividesAll
<1>4. QED
PROOF BY <1>1, <1>2, <1>3, PTL DEF Spec
=============================================================================