[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 7 Nov 2022 17:22:35 +0100*References*: <bcd0ac97-be4f-4b5e-b91b-d347dde2cb61n@googlegroups.com> <2B4AEC9D-EBDE-4E4D-8380-536FA81C4AD2@gmail.com> <e9e17f38-0154-4a92-a34d-1559f0f78168n@googlegroups.com>

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

**Follow-Ups**:

**References**:**[tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?***From:*Amjad Ali

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

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

- Prev by Date:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Next by Date:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Previous by thread:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Next by thread:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Index(es):