Re: [tlaplus] Function domains in TLAPS

[Stephan Merz <stepha...@xxxxxxxxx>]

On 14 Jun 2016, at 16:25, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

On Tuesday, June 14, 2016 at 5:18:04 PM UTC+3, Stephan Merz wrote:

Just knowing that g[3] = 8 doesn't allow you to infer that g is a function or to conclude anything about DOMAIN g, so TLAPS does the right thing. (For example, 42[3] denotes some unspecified value in TLA+, would you want to conclude that 42 is a function?) You want to state "type predicates" for the functions that appear in your specification – typically as ASSUME clauses for constant parameters, and as invariants for variables.

But this doesn't help, either:

    CONSTANT f

    ASSUME A1 == f = [x \in DOMAIN f |-> f[x]]

    ASSUME A2 == f[3] = 8

    LEMMA  3 \in DOMAIN f BY A1, A2

So now we know it's a function, but still don't infer anything about the domain from the mapping.

Correct, this is still too unspecific because f[3] denotes some value even if 3 is not an element of the domain of f. I was thinking of assumptions of the kind

f \in [ 0 .. 10 -> Nat ]

that help you reduce DOMAIN f to a specific set.

Stephan