Using a Division Operator with TLAPS

[hjh...@vt.edu]

Hi,

I'm working on proving an algorithm using TLAPS that requires dividing integers by two. I understand there's no support for real numbers/division in the backend provers, so I am using an operator:

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

The problem I'm running into is when trying to prove properties using the above operator with set expressions. The following example demonstrates this:

EXTENDS Integers, TLAPS, FiniteSets

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

CONSTANTS N

VARIABLES x

Init == x = divide_by_two(N)

PositiveInvariant == x >= 0

ASSUME NumberAssumption == N \in {2,4,6,8,10}

THEOREM PositiveDivisionProperty == Init => PositiveInvariant

  <1> SUFFICES ASSUME Init

               PROVE  PositiveInvariant

    OBVIOUS

  <1> QED

    BY NumberAssumption DEF Init, PositiveInvariant, divide_by_two

The backend provers are unable to prove the above theorem. SMT specifically times out and increasing the timeout doesn't appear to help. 

Changing the assumption to:

ASSUME NumberAssumption == N = 10

will successfully prove the theorem. Are the backend provers able to work with 'CHOOSE' expression in conjunction with sets? Is there anything wrong with how I'm specifying the assumption? The actual algorithm will require using the division operator with a few 'min'/'max' operators, which may also complicate the proof process, so I'm wondering if TLAPS is able to prove these sort of algorithms that require arithmetic.

Best,

Hans

[Saksham Chand]

The following should work and invoke Z3:

divide_by_two(n) == n \div 2

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5d12aa41-9036-4ba4-856a-bf5070853122%40googlegroups.com.

[Hans He]

I'm able to use the above operator with Z3. Thank you for your help.

Hans

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NLLfoXEvxCU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-_Wo9UhL3_Di9NpLO%2BSDLj-tuSNbLoSPObjwP_-JMKpyQ%40mail.gmail.com.

[Stephan Merz]

Following up on Saksham's reply: integer division is written \div in TLA+ and is supported by the prover. Proving theorems about an expression CHOOSE x \in S : P(x) is more complicated because it usually requires showing that there is some element of S that satisfies P. Since you mention min and max, below is a proof by induction over finite sets that shows that any finite and non-empty set of integers has a maximum element. (Your module needs to extend the modules FiniteSetTheorems, which contains FS_Induction and other useful theorems about finite sets and TLAPS.)

Assuming that you are more interested in proving theorems about an algorithm than about elementary lemmas about data, you may want to leave such lemmas unproved.

Stephan

Max(S) == CHOOSE x \in S : \A y \in S : y <= x

LEMMA MaxIntegers ==

  ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S)

  PROVE  /\ Max(S) \in S

         /\ \A y \in S : y <= Max(S)

<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E x \in T : \A y \in T : y <= x

<1>1. P({})

  OBVIOUS

<1>2. ASSUME NEW T, NEW x, P(T), x \notin T

      PROVE  P(T \cup {x})

  <2>. HAVE T \cup {x} \in SUBSET Int

  <2>1. CASE \A y \in T : y <= x

    BY <2>1, Isa

  <2>2. CASE \E y \in T : ~(y <= x)

    <3>. T # {}

      BY <2>2

    <3>1. PICK y \in T : \A z \in T : z <= y

      BY <1>2

    <3>2. x <= y

      BY <2>2, <3>1

    <3>3. QED  BY <3>1, <3>2

  <2>. QED  BY <2>1, <2>2

<1>. HIDE DEF P

<1>3. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("blast")

<1>. QED  BY <1>3, Zenon DEF Max, P

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACOXEhA-Z-DrYi-rjdd6o0D%2BgGLe9YBZ4-TPUf%2BF%3Dy175-10uQ%40mail.gmail.com.