[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: [tlaplus] Proofs of integer properties

 Hi Chris,below is a simple proof in TLAPS of what I believe is your intended result. As Leslie remarked, your difficulties seem to be caused by a confusion between /\ and ^, both of which appear to denote conjunction in your module.LEMMA ASSUME NEW R \in Nat, \E a \in Nat : R = 2 * a,             NEW N \in Nat, NEW VARIABLE x, x = R * N      PROVE  \E y \in Nat : x = 2 * yOBVIOUSNote that it doesn't matter for the validity of this lemma if x is declared as a VARIABLE or CONSTANT.And no, TLA+ is not primarily designed for reasoning about propositional logic (temporal or otherwise). Have you had a look at the Hyperbook?Regards,StephanOn 06 Nov 2014, at 01:34, TLA Plus wrote:Hi Chris,I don't know why you expect a raised to the power b to imply b.  Perhaps you meant a conjoined with b, which is typed  a /\ b .  This might fix some of your other problems.  You write 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 * ZI presume you mean that you can prove    x = A * B  /\  A = Y * Z   =>  x = Y * Z * Bbut can't prove   x = A * B  /\  B = X * Y  =>  x = A * Y * ZI don't know why you expect that to be true, but TLAPS does prove   x = A * B  /\  B = X * Y  =>  x = A * X * Yunder the assumption that x, A, B, X, and Y are integers.  Note that this formula is not valid without that assumption.  On the other hand, the formula      x = A * B  /\  B = X * Y  =>  x = A * (X * Y)is valid without that assumption.Leslie Lamport   On Wed, Nov 5, 2014 at 2:33 PM, wrote: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. -- 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.

• Follow-Ups: