# Re: [tlaplus] Using a Division Operator with TLAPS

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, FiniteSetsdivide_by_two(n) == CHOOSE k \in Nat: n=2*kCONSTANTS NVARIABLES xInit == x = divide_by_two(N)PositiveInvariant == x >= 0ASSUME 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.