Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Before diving into subproofs, it is good practice to get the overall structure of the proof right: start by checking if you can prove the level-1 QED step from the preceding level-1 steps. In your case, since you are claiming an equivalence, you'll need both your step <1>3 and the reverse implication. Your step <1>4 should be one of several level-2 steps beneath step <1>3.

Below is how I would set up the proof, for bit vectors of arbitrary (but fixed) length. Note that the assumption that N is a natural number is not needed for this proof but will probably be useful elsewhere.

Stephan

–––

CONSTANT N
ASSUME NNat == N \in Nat

BVN == [1 .. N -> BOOLEAN]

bv_and(bv1, bv2) == [i \in 1 .. N |-> bv1[i] /\ bv2[i]]

THEOREM 
  ASSUME NEW bv1 \in BVN, NEW bv2 \in BVN, NEW i \in 1 .. N
  PROVE  bv_and(bv1, bv2)[i] <=> bv1[i] /\ bv2[i]
BY DEF BVN, bv_and

On 10 Nov 2022, at 04:58, Amjad Ali <amjad.hamdi.ali@xxxxxxxxx> wrote:

I've defined a 4 bit value as such:

bv4 == [ 0..3 -> {TRUE,FALSE} ]

and a function that does an AND operation on two 4 bit values:

AND4 == [f,g \in bv4 |-> [i \in 0..3 |-> (i=0 /\ f[0] /\ g[0]) \/ 

                                                                (i=1 /\ f[1] /\ g[1]) \/

                                                                (i=2 /\ f[2] /\ g[2]) \/

                                                                (i=3 /\ f[3] /\ g[3])     ]]

This function should behave like any an AND operation in any assembly language. For example,  AND 0b1010, 0b0010 == 0b0010

In TLA+, a 4-bit binary number is represented in a form of a function. So, AND4 takes in. two functions and outputs a function.

It's pretty straight forward to see that AND4 would behave as it should, but how can I prove it for any given 4-bit. values.

I tried starting it. Please tell me if I'm on the right track:

THEOREM AND4_CORRECT==

    \A f,g \in bv4 : \A i \in 0..3 : AND4[f,g][i] <=> f[i] /\ g[i]

PROOF

    <1>1 TAKE f,g \in bv4

    <1>2 TAKE i \in 0..3

    <1>3 ASSUME AND4[f,g][i] PROVE f[i] /\ g[i]

    <1>4 CASE i = 0

        <2>1 f[0] /\ g[0]

            

        <2> QED

    

    <1> QED

--
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/a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n%40googlegroups.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/C80DC618-2D06-4746-8C89-4951E2A78E92%40gmail.com.