Conversation
Collaborator
There was a problem hiding this comment.
Sure, it is nonsense to copy the proof of type preservation in this proof. Factoring out this step as an extra lemma is one solution. The one that I tend to use, given that Spec => []TypeOK has already been established, is to set up the subsequent invariant proof as follows:
THEOREM Spec => []Safety
<1>1. Init => Safety
<1>2. TypeOK /\ TypeOK' /\ Safety => Safety'
<1>. QED
BY <1>1, <1>2, TypeCorrect, PTL DEF Spec
The extra hypotheses TypeOK and TypeOK' are justified by the type-correctness theorem. This saves you from defining the extra predicate Inv as the conjunction of the two invariants.
SafetyCorrect went through Inv == TypeOK /\ Safety, whose inductive step had to re-establish TypeOK' and so duplicated the proof already given for TypeCorrect. Since Spec => []TypeOK is established, TypeOK can enter the step as a hypothesis and be discharged in the QED step by citing TypeCorrect: <1>2. TypeOK /\ Safety /\ [Next]_vars => Safety' <1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec The TypeOK step becomes LEMMA TypeOKStep. The case analyses are unchanged; tlapm --nofp proves all 193 obligations. Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
SafetyStep re-derived TypeOK /\ [Next]_vars => TypeOK' inline: the step existed only inside the proof of THEOREM TypeCorrect, and proof steps are not citable from another theorem, while Spec => []TypeOK is temporal and SafetyStep assumes no temporal hypothesis.
Hoist the step to a top-level lemma; TypeCorrect's <1>2 and SafetyStep's <1>typok now both cite it. The proof body is unchanged, step levels included. tlapm --nofp proves all 199 obligations.