Hi,
I am trying to learn TLA+ by implementing some simple proofs. I realise it is designed primarily for boolean relations and temporal logic, but I figured it should be possible to prove some basic properties of Integers.
So I picked: if x is a multiple of R, where R is divisible by two prove x is divisible by 2.
I hit a number of issues, and I can't find a successful path to proof.
Specifically:
- I needed to add basic facts I thought should be "obvious" like a ^ b => b
- I had a lot of trouble taking proof steps relating to manipulation of equations eg. I had to define an axiom for a * b = b * a, and failed to prove or use the proof of a more complex fact, a * b * c = c * a * b
- Proofs requiring algebraic substitution only seem to work when the term to substitute is the first term, ie. if (1) x = A * B, I can prove the substition A = Y * Z into (1) == x = Y * Z * B, but not B = X * Y into (1) == x = A * Y * Z
Am I barking up the wrong tree here and using the wrong tool for this kind of proof? Or am I missing something?
Full proof follows.
Regards,
Chris.
(*
* We want to prove if x is divisible by and number R, that is divisible by 2, then x is divisible by 2
*)
EXTENDS Integers, TLAPS, TLC
CONSTANT N, R
(* Pick an arbitrary N >= 1 *)
ASSUME NAssumption == N \in Nat /\ N >= 1
(* R is any natural number that is a multiple of 2 *)
ASSUME RAssumption == R \in Nat /\ \E a \in Nat : R = 2 * a
VARIABLES x
XNat == x \in Nat
XChooseRN == x = R * N
(* X is a multiple N of R *)
Init == XNat ^ XChooseRN
(* We want to prove x is divisible by 2 *)
Result == \E y \in Nat : x = 2 * y
(* Some basic facts that the TLA+ solvers don't seem to know *)
AXIOM AndB == \A a,b : a ^ b => b
AXIOM NCommutatMult == \A a,b \in Nat : a * b <=> b * a
(*AXIOM NMultSubst == \A a,b,c,r \in Nat : (a = b * c) ^ (r = b * c) => (a = r)
AXIOM NMultSubst3 == \A a,b,c,d,r \in Nat : (r = a * b * c) ^ (d = b * c) => (r = a * d)
THEOREM NMultSubst3a == \A a,b,c,d,r : (d = b * c) => ((r = a * b * c) <=> (r = a * d))
<1> SUFFICES ASSUME NEW a, NEW b, NEW c, NEW d, NEW r,
d = b * c
PROVE (r = a * b * c) <=> (r = a * d)
OBVIOUS
<1> QED
*)
AXIOM NCommutatMult312 == \A a,b,c \in Nat : a * b * c = c * a * b
(* PROOF OMITTED*)
(* Try direct substitution *)
THEOREM XIsEven1 == Init => Result
<1> USE NAssumption, RAssumption DEF Init
<1> SUFFICES ASSUME Init PROVE Result
OBVIOUS
<1>2. x = R * N
BY Init, AndB DEF XNat, XChooseRN
<1>3. PICK q \in Nat : R = 2 * q
BY RAssumption, AndB
<1>4. x = 2 * q * N
BY <1>2, <1>3
<1>5. PICK y \in Nat : y = q * N
OBVIOUS
<1>6. x = 2 * y
BY <1>4, <1>5
<1> QED
(* Try to prove that by comparison *)
THEOREM XIsEven2 == Init => Result
<1> USE NAssumption, RAssumption DEF Init
<1> SUFFICES ASSUME Init PROVE Result
OBVIOUS
<1>2. x = R * N
BY Init, AndB DEF XNat, XChooseRN
<1>3. PICK q \in Nat : R = 2 * q
BY RAssumption, AndB
<1>4. x = 2 * q * N
BY <1>2, <1>3
<1>5. PICK y \in Nat : y = q * N
OBVIOUS
<1>6. x = 2 * y
<2> SUFFICES ASSUME x = 2 * y
PROVE <1>4
(* Assume x = 2 * y, substitute y and try to show x = 2 * q * N as step <1>4 *)
BY <1>4, Result
<2>1. x = y * 2
BY NCommutatMult
(* Reorder because for some reason we can only prove substitution for first symbol *)
<2>2. x = q * N * 2
BY <2>1, <1>5
<2>3. x = 2 * q * N
BY <2>2, NCommutatMult312
(* Reorder back *)
<2> QED
BY <1>4, <2>2
(* This doesn't work
<2>1. x = 2 * q * N
BY <1>5
<2> QED
BY <1>4, <2>1
*)
<1> QED
=============================================================================
\* Modification History
\* Last modified Wed Nov 05 11:30:16 PST 2014 by Chris.Nott
\* Created Tue Nov 04 11:05:21 PST 2014 by Chris.Nott
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.