EWD998: close the nine lemmas that were stated without proof - #218
Open
vasilisnasopoulos-stack wants to merge 1 commit into
Open
EWD998: close the nine lemmas that were stated without proof#218vasilisnasopoulos-stack wants to merge 1 commit into
vasilisnasopoulos-stack wants to merge 1 commit into
Conversation
EWD998_proof.tla asserted nine lemmas with no proof. Steps carrying no proof generate no obligation, so tlapm reported "All 807 obligations proved" and exited 0, and `--strict` (tlaplus/tlapm#278) exits 11. The six FoldFunctionOnSet* lemmas are now imported from FunctionTheorems, where they are proved. SumIsInt, SumIsNat and SumEqual get structured proofs on top of them, using FS_Subset to carry finiteness from Node to the index set. SumIterate and SumUnion do not go through that way: TLAPS cannot instantiate the second-order op(_,_) against the LAMBDA in Sum. They are proved instead from MapThenSumSetAddElement and MapThenSumSetDisjointUnion in FiniteSetsExtTheorems, whose operator is unary, and which coincide with Sum once the definitions are unfolded. Functions.tla gains SumFunctionOnSet and SumFunction, which FunctionTheorems requires and the vendored copy predates. With tlapm 1.6.0-pre: 851 obligations, all proved, `--strict` exit 0. Runtime rose from roughly one minute to a minute and a half locally, so maxRuntimeMinutes goes from 2 to 4. Signed-off-by: Vasilis Nasopoulos <vasilis_nasopoulos@hotmail.com>
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
1 participant
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.
Follow-up to the discussion in tlaplus/CommunityModules#128.
EWD998_proof.tlastates nine lemmas with no proof at all. Steps carrying no proof generate no obligation, sotlapmreports All 807 obligations proved and exits 0 — while--strict(tlaplus/tlapm#278) exits 11. This closes all nine.The six
FoldFunctionOnSet*lemmas are removed and imported fromFunctionTheorems, where they are proved. Their statements are the same up to generalisation; the community versions have weaker hypotheses.SumIsInt,SumIsNat,SumEqualget structured proofs on top of those, usingFS_Subsetto carry finiteness fromNodedown to the index set — which is what the oldBYlines were missing.SumIterateandSumUniondo not go through that route. TLAPS cannot instantiate the second-orderop(_,_)against theLAMBDA x1, x2 : x1 + x2insideSum; the file already carried commented-out attempts marked(* fails *). They are proved instead fromMapThenSumSetAddElementandMapThenSumSetDisjointUnioninFiniteSetsExtTheorems, whose operator is unary, and which coincide withSumonce the definitions are unfolded. Thanks to @muenchnerkindl for the pointer.Functions.tlagainsSumFunctionOnSetandSumFunction(10 added lines, nothing removed).FunctionTheoremsneeds them and the vendored copy predates them.manifest.json:maxRuntimeMinutes2 → 4. Locally the module went from about a minute to 1m33s with--stretch 5on a cold cache.Result
--strictexitVerified with
tlapm 1.6.0-pre(4600b24), invoked as the CI does:AsyncTerminationDetection_proof.tlain the same directory is unaffected (exit 0, 30 obligations).EWD998PCal_proof.tlafails for me withUnknown module "BagsExt"both before and after this change, so that is my include path rather than anything here.