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

*From*: TLA Plus <tlapl...@xxxxxxxxx>*Date*: Wed, 5 Nov 2014 16:34:28 -0800*References*: <27780607-9e0a-4101-92fa-ccbb15043611@googlegroups.com>

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 * Z

I presume you mean that you can prove

x = A * B /\ A = Y * Z => x = Y * Z * B

but can't prove

x = A * B /\ B = X * Y => x = A * Y * Z

I don't know why you expect that to be true, but TLAPS does prove

x = A * B /\ B = X * Y => x = A * X * Y

under 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, <chris...@xxxxxxxxx> 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.

**Follow-Ups**:**Re: [tlaplus] Proofs of integer properties***From:*chris . . .

**Re: [tlaplus] Proofs of integer properties***From:*Stephan Merz

**References**:**Proofs of integer properties***From:*chris . . .

- Prev by Date:
**Proofs of integer properties** - Next by Date:
**Re: [tlaplus] Proofs of integer properties** - Previous by thread:
**Proofs of integer properties** - Next by thread:
**Re: [tlaplus] Proofs of integer properties** - Index(es):