| The issue is that the current version of TLAPS does not support tuple constructions [1] and you have to reformulate your function definition in "curried" form, see below. Still, my advice would be to prefer operator definitions over function definitions when you have a choice.
Stephan
CONSTANT N
ASSUME NNat == N \in Nat
BVN == [0..N -> {TRUE, FALSE}]
ANDN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> f[i] /\ g[i]]]]
THEOREM ANDN_CORRECT==
\A f,g \in BVN : \A i \in 0..N :
ANDN[f][g][i] <=> f[i] /\ g[i]
\* BY DEF BVN, ANDN \* also works <1>1 TAKE f,g \in BVN
<1>2 TAKE i \in 0..N
<1>3 ANDN[f][g][i] <=> f[i] /\ g[i]
BY DEF BVN, ANDN
<1> QED BY <1>3
It's weird how defining bv_and as an operator makes this much simpler. Why is this the case?
I have ANDN defined as a function and ANDN2 as an operator. They do the same thing but the proof fails on line <1>3 for ANDN . Under "Poorly Supported Tla Features" in the TLAPS Documentation page, it reads, "For records, the provers usually need to be told explicitly to use a fact of the form r.f = e even when they are given the fact r = [f |-> e, ...]." My guess is this poorly supported feature applies to functions as well because, in my case, the prover cannot see that:
PROVE [i \in 0..N |-> f[i] /\ g[i]] = [f_1, g_1 \in BVN |-> [i \in 0..N |-> f_1[i] /\ g_1[i]]] [f, g]
All it literally needs to do is apply the [f,g] to the function on the right side and see that it equals the left function.
BVN == [0..N -> {TRUE, FALSE}] ANDN == [f,g \in BVN |-> [i \in 0..N |-> f[i] /\ g[i]]] ANDN2(f,g) == [i \in 0..N |-> f[i] /\ g[i]] THEOREM ANDN2_CORRECT== \A f,g \in BVN : \A i \in 0..N : ANDN2(f,g)[i] <=> f[i] /\ g[i] PROOF <1>1 TAKE f,g \in BVN <1>2 TAKE i \in 0..N <1>3 ANDN2(f,g)[i] <=> f[i] /\ g[i] BY DEF BVN, ANDN2
<1> QED BY <1>3
THEOREM ANDN_CORRECT== \A f,g \in BVN : \A i \in 0..N : ANDN[f,g][i] <=> f[i] /\ g[i] PROOF <1>1 TAKE f,g \in BVN <1>2 TAKE i \in 0..N <1>3 ANDN[f,g][i] <=> f[i] /\ g[i] >>>>>>>>>>>>>>>>>>>> Fails Here BY DEF BVN, ANDN
<1> QED BY <1>3 On Thursday, November 10, 2022 at 3:06:42 AM UTC-6 Stephan Merz wrote:
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
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/4e50b05c-19bb-4673-ba06-7933b41412cen%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/F69485A6-AAAB-4105-8C1D-682E4835476B%40gmail.com.
|