# Re: [tlaplus] Re: Parsing issues with prime operator in user-defined operators

In your lemma, IdxSet is indeed under a quantifier and thus a constant, so your lemma is true.
But in the definition of WellFormedTest, IdxSet is a parameter, which is not necessarily a constant. When you pass a non-constant _expression_ as argument to WellFormedTest, it is simply substituted for IdxSet. When you then apply the prime operator to it, it gets primed just like the rest of the body of WellFormedTest.

In other words, your lemma doesn't prove that IdxSet is a constant, it proves that, when you substitute IdxSet with a constant, then your equation is true.

It's important to understand that, unlike variables quantified with \A and \E, the parameter of an operator is not restricted to be a constant.

On Thursday, July 11, 2024 at 7:55:00 AM UTC+2 Ugur Y. Yavuz wrote:
@Damien: That is also correct, but IdxSet = IdxSet' as IdxSet is a constant (under the quantifier). On my end, the following claim goes through trivially:

WellFormedTest(IdxSet) == \A p \in ProcSet :
CASE pc[p] = "L0" -> TRUE
[] pc[p] = "L1" /\ l[p] \in IdxSet -> TRUE
[] pc[p] = "L1" /\ l[p] \notin IdxSet -> FALSE

LEMMA WellFormedTestPrime ==
\A IdxSet \in 0..L'-1 :
WellFormedTest(IdxSet)' = (\A p \in ProcSet :
CASE pc'[p] = "L0" -> TRUE
[] pc'[p] = "L1" /\ l'[p] \in IdxSet -> TRUE
[] pc'[p] = "L1" /\ l'[p] \notin IdxSet -> FALSE)
BY DEF WellFormedTest

On Wednesday 10 July 2024 at 10:46:27 UTC-4 Ugur Y. Yavuz wrote:

> Is this an issue with SANY or the TLAPM parser?

This is regarding SANY. It came up while I was working on a TLAPS proof, but it would also happen if I tried to define the action elsewhere.

> It's not a bug. The _expression_ WellFormed(full_indices)' has a double prime.

It doesn't have a double prime, in the sense that once you substitute the provided argument's definition in the predicate, there is no variable which is double primed (see the _expression_ it is semantically equivalent to). That's why I wasn't sure if the parser rejecting this _expression_ was intended behavior.

On Wednesday 10 July 2024 at 00:13:07 UTC-4 Leslie Lamport wrote:

It’s not a bug.  The _expression_ WellFormed(full_indices)' has a double prime.

From: tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> On Behalf Of Andrew Helwer
Sent: Tuesday, July 9, 2024 18:51
To: tlaplus <tla...@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Re: Parsing issues with prime operator in user-defined operators

Is this an issue with SANY or the TLAPM parser?

On Monday, July 8, 2024 at 10:48:54AM UTC-4 Ugur Y. Yavuz wrote:

Hello, I have a question about the prime operator, particularly how it gets parsed in conjunction with user-defined operators.

Consider the following operator definition, where pc and l are among the variables of the specification, and ProcSet is a constant:

WellFormed(IdxSet) ==
\A p \in ProcSet :
CASE pc[p] = "L0"                       -> TRUE
[] pc[p] = "L1" /\ l[p] \in IdxSet    -> TRUE
[] pc[p] = "L1" /\ l[p] \notin IdxSet -> FALSE

Note that we have:

WellFormed(IdxSet)' =
\A p \in ProcSet :
CASE pc'[p] = "L0"                        -> TRUE
[] pc'[p] = "L1" /\ l'[p] in IdxSet     -> TRUE
[] pc'[p] = "L1" /\ l'[p] \notin IdxSet -> FALSE

Suppose L and A are also variables of the specification, and that we aim to prove the invariant \E IdxSet \in SUBSET 0..L-1 : WellFormed(IdxSet) in TLAPS. After proving it for the initial configuration, we need to prove it for a subsequent configuration, reached from one where the inductive invariant holds; i.e., \E IdxSet \in SUBSET 0..L'-1 : WellFormed(IdxSet)'. Suppose the witness for this claim needs to be a function of the specification variables' values in the next configuration. Say we want to proceed as follows:

...
<3> DEFINE full_indices == {idx \in 0..(L'-1) : A'[idx] > 0}
<3>1. WellFormed(full_indices)'

However, this results in a parser error: "Level error in applying operator ': The level of argument 1 exceeds the maximum level allowed by the operator."

Is this intended behavior? The _expression_ seems equivalent to:

\A p \in ProcSet :
CASE pc'[p] = "L0" -> TRUE
[] pc'[p] = "L1" /\ l'[p] in {idx \in 0..(L'-1) : A'[idx] > 0} -> TRUE
[] pc'[p] = "L1" /\ l'[p] \notin {idx \in 0..(L'-1) : A'[idx] > 0} -> FALSE

which I can express in TLA+. This issue arose in a larger proof, and I simplified it as much as possible. I circumvented it with several rewrites, which I believe shouldn't be necessary at a first glance. I can provide more context if needed.

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