Re: [tlaplus] TypeOK => TypeOK' with no other assumptions

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

Hello,

this is a known bug that has been fixed in the development version of TLAPS that is hopefully soon going to give rise to a new release. Indeed, you should not be using PTL for proving non-temporal (i.e., state- or action-level) proof obligations, but only for steps involving operators of temporal logic.

Sorry for the confusion,
Stephan


> On 19 Feb 2018, at 11:39, tal...@xxxxxxxxx wrote:
> 
> Hi. I'm new to TLA+ and just tried my first proof. It appeared to work, and everything went green, but it seemed a bit too easy. After simplifying things, I ended up with this, which also goes all green:
> 
> ------------------------------- MODULE False -------------------------------
> 
> EXTENDS TLAPS
> 
> VARIABLE x
> 
> TypeOK == x = {}
> 
> THEOREM T0 ==
>  ASSUME TypeOK
>  PROVE  TypeOK'
>  BY PTL DEF TypeOK
> 
> =============================================================================
> 
> Oddly, if I replace TypeOK with its definition then it no longer accepts it. It does still accept it if I remove the "DEF TypeOK" bit completely though.
> 
> Maybe I shouldn't be using "BY PTL" here, but could someone explain what this means?
> 
> This is Version 1.5.6 of 29 January 2018 and includes:
>  - SANY Version 2.1 of 23 July 2017
>  - TLC Version 2.12 of 29 January 2018
>  - PlusCal Version 1.8 of 07 December 2015
>  - TLATeX Version 1.0 of 20 September 2017
> 
> Thanks!
> 
> -- 
> 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.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.