How to simplify my CMP32 function in terms of N?

[Amjad Ali]

Given the following  definitions below, how can I generalize my CMP32 function to work for any domain 0..N (like the XORN function)? The CMP function should have a range {TRUE, FALSE}. Which is TRUE when both inputs are equal and FALSE otherwise:

CONSTANT N

ASSUME NNAT == N \in Nat

BVN == [0..N -> {TRUE,FALSE}]

XORN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> ((f[i] /\ ~g[i]) \/ (~f[i] /\ g[i]))]]]

CMP32 == [f \in BVN |-> [g \in BVN |->  

                                       ~XORN[f][g][0]  /\ ~XORN[f][g][1]  /\ ~XORN[f][g][2]  /\ 

                                       ~XORN[f][g][3]  /\ ~XORN[f][g][4]  /\ ~XORN[f][g][5]  /\ 

                                       ~XORN[f][g][6]  /\ ~XORN[f][g][7]  /\ ~XORN[f][g][8]  /\

                                       ~XORN[f][g][9]  /\ ~XORN[f][g][10] /\ ~XORN[f][g][11] /\

                                       ~XORN[f][g][12] /\ ~XORN[f][g][13] /\ ~XORN[f][g][14] /\

                                       ~XORN[f][g][15] /\ ~XORN[f][g][16] /\ ~XORN[f][g][17] /\

                                       ~XORN[f][g][18] /\ ~XORN[f][g][19] /\ ~XORN[f][g][20] /\

                                       ~XORN[f][g][21] /\ ~XORN[f][g][22] /\ ~XORN[f][g][23] /\

                                       ~XORN[f][g][24] /\ ~XORN[f][g][25] /\ ~XORN[f][g][26] /\

                                       ~XORN[f][g][27] /\ ~XORN[f][g][28] /\ ~XORN[f][g][29] /\

                                       ~XORN[f][g][30] /\ ~XORN[f][g][31] ]]

I would like something like :

CMP32 == [f \in BVN |-> [g \in BVN |->  

                                       ~XORN[f][g][0]  /\ ~XORN[f][g][1]  /\ .. /\ ~XORN[f][g][N] 

[Stephan Merz]

The "fold" operators defined in the CommunityModules [1] are your friend here. Something along the lines of

CMPN == [f \in BVN |-> [g \in BVN |-> 

           FoldFunction(LAMBDA x,y : x /\ y, TRUE, [i \in 0 .. N |-> ~XOR[f][g][i]])]

where the operator FoldFunction comes from the modules Functions of the CommunityModules. I have not actually tried this, though. Also, be aware that at this point the standard proof library does not yet contain lemmas about fold operators, so you will want to state (without proof) basic lemmas such as the ones asserted below (copied from [2]).

Stephan

[1] https://github.com/tlaplus/CommunityModules/tree/master/modules

[2] https://github.com/tlaplus/Examples/blob/ISoLA2022/specifications/ewd998/EWD998_proof.tla 

IsAssociativeOn(op(_,_), S) ==
  \A x,y,z \in S : op(x, op(y,z)) = op(op(x,y), z)
  
IsCommutativeOn(op(_,_), S) ==
  \A x,y \in S : op(x,y) = op(y,x)
  
IsIdentityOn(op(_,_), e, S) ==
  \A x \in S : op(e,x) = x

LEMMA FoldFunctionIsFoldFunctionOnSet ==
  ASSUME NEW op(_,_), NEW base, NEW fun
  PROVE  FoldFunction(op, base, fun) = FoldFunctionOnSet(op, base, fun, DOMAIN fun)

LEMMA FoldFunctionOnSetEmpty ==
  ASSUME NEW op(_,_), NEW base, NEW fun
  PROVE  FoldFunctionOnSet(op, base, fun, {}) = base 

LEMMA FoldFunctionOnSetIterate ==
  ASSUME NEW op(_,_), 
         NEW S, IsFiniteSet(S), NEW T, 
         NEW base \in T, NEW fun \in [S -> T], 
         NEW inds \in SUBSET S, NEW e \in inds,
         IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T)
  PROVE  FoldFunctionOnSet(op, base, fun, inds)
       = op(fun[e], FoldFunctionOnSet(op, base, fun, inds \ {e}))

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/823518f4-8176-47ed-9b68-9d8d6f7291f9n%40googlegroups.com.