# Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?

Wow! I appreciate the help, but how can I actually write the proof to the theorem. It will be great help if you can help me prove this smaller theorem for the xor function. I'm trying to prove it by case but it's not working:

THEOREM NOT_XOR_EQ ==

\A x,y \in {TRUE, FALSE} : ~xor[x,y] => x=y

PROOF

<1> TAKE x,y \in {TRUE, FALSE}

<1>1 CASE x=FALSE /\ y=FALSE

<2>1 ~xor[x,y] = TRUE BY DEF xor

<2>2 QED BY <2>1

<1>2 x=FALSE /\ y=TRUE

<2>3 ~xor[x,y] = FALSE BY DEF xor

<2>4 QED BY <2>3

<1>3 x=TRUE /\ y=FALSE

<2>5 ~xor[x,y] = FALSE BY DEF xor

<2>6 QED BY <2>5

<1>4 x=TRUE /\ y=TRUE

<2>7 ~xor[x,y] = TRUE BY DEF xor

<2>8 QED BY <2>7

<1>5 QED BY <1>1, <1>2, <1>3, <1>4

On Sunday, November 6, 2022 at 2:36:04 AM UTC-6 Stephan Merz wrote:
Hello,

first of all, please do not send screen shots unless you want to illustrate some behavior of the GUI: TLA+ source is pure ASCII and can be copied and pasted into messages.

Since you apply Boolean operations to the elements of your bit vectors, you want to change the co-domain from {0,1} to {TRUE, FALSE}. After that change, TLC can easily evaluate your formula. In my version below, I made xor and cmp_bv4 plain operators rather than definitions of functions (which you get with your version using square brackets). This should not make a difference, but I consider this style to be more idiomatic. (See also section 6.4 of Specifying Systems.) I also strengthened the assertion of your theorem to make it an equivalence and to assert equality of the two bit vectors.

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

xor(b0, b1) == (b0 /\ ~ b1) \/ (~ b0 /\ b1)
cmp_bv4(bv0, bv1) ==
/\ ~ xor(bv0[0], bv1[0])
/\ ~ xor(bv0[1], bv1[1])
/\ ~ xor(bv0[2], bv1[2])
/\ ~ xor(bv0[3], bv1[3])

THEOREM CMP_CORRECT ==
\A x,y \in BV4 : cmp_bv4(x,y) <=> x = y

Now, create a model in the Toolbox and click on "evaluate constant _expression_". Paste the assertion of the theorem, i.e., the formula

\A x,y \in BV4 : cmp_bv4(x,y) <=> x = y

into the "_expression_" field of the window and click on the green triangle. TLC will report that the _expression_ evaluates to TRUE.

Stephan

I want to prove cmp_bv4 for all 4-bit binary numbers is correct. As seen below, a binary value of 4 bits is represented as a set of functions with domain 0-3 and range 0 and 1. Then, an xor function with domain 0 and 1 that outputs 0 if the two inputs match (or 1 other, otherwise). Finally,  cmp_bv4 takes in two 4-bit binary numbers and uses the xor function to determine if the values match. Why do this and not just use (=) ? In the machine I'm building, a comparator is not available and I need to build one from scratch.
<Screen Shot 2022-11-06 at 12.43.42 AM.png>

--
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.