| Hello,
I had not understood that you were trying to use TLAPS to prove this theorem. This being said, the problem is finitary, and TLC evaluating the assertion of the theorem to TRUE would be good enough for me.
Anyway, below is a proof of your theorem, as well as of the overall theorem for comparing two bit-vectors, checked by TLAPS, for my definitions of xor and cmp_bv4, i.e. using plain operators instead of function definitions. The proof about xor is immediate, the other proof needs a little help, in particular for converting the interval into an explicitly enumerated set. I imagine that the analogous proof for bit vectors of parametric length N would be simpler to write. I have not tried writing the proof for your version of the definitions: reasoning about functions is always a little harder because the provers have to understand the function domains.
Hope this helps, Stephan
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 NOT_XOR_EQ ==
\A x,y \in {TRUE, FALSE} : ~xor(x,y) => x=y
BY DEF xor
THEOREM CMP_CORRECT ==
ASSUME NEW x \in BV4, NEW y \in BV4
PROVE cmp_bv4(x,y) <=> x = y
<1>1. ASSUME cmp_bv4(x,y) PROVE x = y
<2>. SUFFICES x[0] = y[0] /\ x[1] = y[1] /\ x[2] = y[2] /\ x[3] = y[3]
BY DEF BV4
<2>. (0 .. 3) = {0,1,2,3}
OBVIOUS
<2>. /\ x[0] \in {TRUE, FALSE}
/\ x[1] \in {TRUE, FALSE}
/\ x[2] \in {TRUE, FALSE}
/\ x[3] \in {TRUE, FALSE}
/\ y[0] \in {TRUE, FALSE}
/\ y[1] \in {TRUE, FALSE}
/\ y[2] \in {TRUE, FALSE}
/\ y[3] \in {TRUE, FALSE}
BY DEF BV4
<2>. QED BY <1>1, NOT_XOR_EQ DEF BV4, cmp_bv4
<1>2. ASSUME x = y PROVE cmp_bv4(x,y)
BY <1>2 DEF BV4, cmp_bv4, xor
<1>. QED BY <1>1, <1>2
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>
<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+unsubscribe@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e9e17f38-0154-4a92-a34d-1559f0f78168n%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/52722E8B-458B-4110-B33F-1FCA821E3F86%40gmail.com.
|