Fix SMT SetOf n-ary extensionality axiom

[ylht]

Summary

Fix the SMT extensionality helper axiom for SetOf_n so n-ary set comprehensions pass all n bound-domain arguments to the SMT SetOf_n application.

Refs #265.

Scope

This PR is intentionally limited to an SMT backend arity fix. It does not add general TLAPS support for TLA+ constructs that bind more than one variable, and it does not address support in the Zenon or Isabelle backends.

The broader multi-variable binding limitation is discussed in #265 and in the TLAPS unsupported features documentation.

Root Cause

SetOf_n is declared as taking n domain arguments plus one predicate/function argument:

SetOf_n(a1, ..., an, P)

But assert_issetof n encoded the assertion as if every SetOf_n were unary:

SetOf_n(a, P)

This is accidentally correct for n = 1, but wrong for n >= 2.

Changes

• Give P the type idv^n -> idv in assert_issetof n.
• Quantify n bound-domain arguments.
• Build SetOf_n(a1, ..., an, P) in the trigger and assertion.
• Add a minimal SMT regression test using a two-variable set comprehension.

Validation

New regression test on the fixed binary:

tlapm --cleanfp --nofp test/fast/regression/setof_nary_smt_test.tla

Result:

[INFO]: All 2 obligations proved.

The same test fails on 471b481 with fingerprints disabled:

[ERROR]: 1/2 obligations failed.

Build:

DUNE_PROFILE=release OCAMLPARAM='_,O3=1,unbox-closures=1,rounds=2' opam exec -- dune build src/tlapm.exe

[muenchnerkindl]

As noted in the related issue, TLAPS not supporting constructs binding more than one variable applies in a much broader sense than just for the SMT backend. While your fix may go some way for introducing support for the SMT backend specifically, supporting such constructs needs more pervasive changes to tlapm and the different backends. Note that

THEOREM {x+y : x \in {1}, y \in {1}} = 2
OBVIOUS

outputs error message concerning SMT, Zenon, and Isabelle.

[ylht]

Thanks, that makes sense. I agree this PR does not implement general support for multi-variable binders across TLAPS and all backends.

I will update the PR description to make the scope explicit: this is only an SMT backend arity fix for the existing SetOf_n encoding, not a full fix for #265. I will also change "Closes #265" to "Refs #265".

If you prefer not to accept partial SMT-only support for this unsupported construct, I can close the PR.