[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLAPS: how to take a \beta-reduction step?



Dear Stephan,

Stephan Merz <stephan.merz@xxxxxxxxx> writes:

> Hello,
>
> TLAPS only supports functions of one argument. It’s probably best to replace your function of type

thanks!!! That did it.

Best regards,

Marko

> [ Elems \X SUBSET Elems -> SUBSET Elems ]
>
> by a “curried” function
>
> [ Elems -> [ SUBSET Elems -> SUBSET Elems ] ]
>
> and correspondingly write
>
> ASSUME ...
> PROVE  x \in [new \in Elems |-> [set_1 \in SUBSET Elems |-> set_1 \cup {new}]][x][set]
>
> Regards,
> Stephan
>
>
>> On 20 Jun 2019, at 18:39, 'Marko Schuetz-Schmuck' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
>> 
>> Dear All,
>> 
>> I have a function Insert and an operator InsertOp as in the attached
>> file. When I make the definition of the operator available TLAPS proves
>> the corresponding theorem, but when I make the definition of the
>> function available the function gets rewritten leading to the goal
>> 
>> ASSUME NEW CONSTANT Elems,
>>       NEW CONSTANT x \in Elems,
>>       NEW CONSTANT set \in SUBSET Elems
>> PROVE  x
>>       \in [new \in Elems, set_1 \in SUBSET Elems |-> set_1 \cup {new}][x,
>>                                                                    set]
>> 
>> How do I tell TLAPS to take the \beta-reduction step?
>> 
>> I was unable to find this in all the TLAPS documentation I checked.
>> 
>> Thanks and best regards,
>> 
>> Marko
>> 
>> -- 
>> 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
>> Visit this group at https://groups.google.com/group/tlaplus.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736k4us6d.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
>> For more options, visit https://groups.google.com/d/optout.
>> ------------------------------- MODULE Dummy -------------------------------
>> EXTENDS TLAPS
>> CONSTANT Elems
>> ASSUME \E x : x \in Elems
>> 
>> Insert[new \in Elems, set \in SUBSET Elems] ==
>>  set \cup {new} 
>> 
>> InsertOp(new, set) ==
>>  set \cup {new}
>> 
>> THEOREM \A x \in Elems, set \in SUBSET Elems: 
>>  x \in Insert[x, set]
>>  <1> SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
>>               PROVE  x \in Insert[x, set]
>>    OBVIOUS
>>  <1> QED
>>    BY DEF Insert
>> 
>> THEOREM \A x \in Elems, set \in SUBSET Elems:
>>  x \in InsertOp(x, set)
>>  <1>a SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
>>               PROVE  x \in InsertOp(x, set)
>>    OBVIOUS
>>  <1>b QED
>>    BY DEF InsertOp
>> =============================================================================
>> \* Modification History
>> \* Last modified Thu Jun 20 12:30:32 AST 2019 by marko
>> \* Created Thu Jun 13 13:34:49 AST 2019 by marko
>> 
>> -- 
>> 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
>> Visit this group at https://groups.google.com/group/tlaplus.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736k4us6d.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
>> For more options, visit https://groups.google.com/d/optout.
>
> -- 
> 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/944861DF-5AC1-4DEA-A37E-6D581E5A0F04%40gmail.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87wohgt6qr.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
For more options, visit https://groups.google.com/d/optout.

Attachment: signature.asc
Description: PGP signature