Re: [tlaplus] Using a Division Operator with TLAPS

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

On 5 Dec 2019, at 04:33, Hans He <hjh2bs@xxxxxx> wrote:

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

Hans

On Wed, Dec 4, 2019 at 6:02 PM Saksham Chand <schand@xxxxxxxxxxxxxxxxx> wrote:
The following should work and invoke Z3:

divide_by_two(n) == n \div 2

On Wed, Dec 4, 2019 at 5:47 PM <hjh2bs@xxxxxx> wrote:
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

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-_Wo9UhL3_Di9NpLO%2BSDLj-tuSNbLoSPObjwP_-JMKpyQ%40mail.gmail.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
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.