theorem library for fold operators #116
Conversation
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
muenchnerkindl
force-pushed
the
fold_proofs
branch
from
b346abd to
bb74c66
Compare
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
|
Any comments on these theorems? Are they ready to be merged? |
…rems and proofs Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
modules/FoldTheorems.tla
Outdated
| @@ -0,0 +1,77 @@ | |||
| --------------------------- MODULE FoldTheorems --------------------------- | |||
There was a problem hiding this comment.
You used snake_case for FiniteSetsExt_theorems earlier, but camelCase here.
There was a problem hiding this comment.
In fact, @kape1395 used snake_case for that module, but we had used camelCase for all other modules (in the standard library and here). I just changed FiniteSetExt_theorems to FiniteSetExtTheorems for consistency.
Related, FoldTheorems should perhaps be renamed to FoldsTheorems, even if it sounds ugly?
modules/FoldTheorems.tla
Outdated
| (* This module only lists theorem statements for reference. The proofs *) | ||
| (* can be found in module FoldTheorems_proofs.tla. *) | ||
| (*************************************************************************) | ||
| EXTENDS Folds, FiniteSets, TLAPS |
modules/FiniteSetsExtTheorems.tla
Outdated
| EXTENDS FiniteSetsExt, FiniteSets, Integers | ||
| (*************************************************************************) | ||
| (* This module only lists theorem statements for reference. The proofs *) | ||
| (* can be found in module FiniteSetsExt_theorems_proofs.tla. *) |
| ASSUME NEW S \in SUBSET Int, IsFiniteSet(S) | ||
| PROVE ProductSet(S) \in Int | ||
|
|
||
| THEOREM ProductSetNonempty == |
There was a problem hiding this comment.
Also add ProductSetEmpty (THEOREM ProductSetEmpty == ProductSet({}) = 1) for consistency with SumSetEmpty?
|
|
||
| THEOREM SumSetNatZero == | ||
| ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S) | ||
| PROVE SumSet(S) = 0 <=> S \subseteq {0} |
There was a problem hiding this comment.
S \subseteq {0} is elegant, but perhaps the more explicit (S = {} \/ S = {0}) instead of S \subseteq {0} (same below for ProductSetNatOne) is easier to understand?
lemmy
left a comment
lemmy
left a comment
There was a problem hiding this comment.
Adding comments would make the theorems in FoldTheorems.tla and FiniteSetsExtTheorems.tla more accessible.
We should integrate TLAPS into the CI. Related question: which version (release vs. HEAD) of TLAPS discharges these proofs?
This comment was marked as outdated.
This comment was marked as outdated.
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
|
@lemmy Thank you for your review. I addressed all of the remarks except leaving The proofs are checked with the HEAD of TLAPS: the binary release is too outdated to make much sense anymore. |
|
Assuming the pre-release at https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz is sufficient to prove these theorems, https://github.com/tlaplus-workshops/ewd998/blob/36880a06bc5e251eb3ad982a0d03a3fd55670a0a/.github/workflows/main.yml#L26 shows an extremely simple integration of TLAPS into Github CI. |
This PR adds a library of theorems for the fold operators defined in modules Fold.tla and FiniteSetsExt.tla.
@kape1395: These theorems essentially supersede those that (I believe) you introduced for the operator MapThenSumSet of module FIniteSetsExt, using proofs about the underlying MapThenFoldSet operator rather than going through an auxiliary operator. Your theorems and proofs are still there, below the end module separator, but it looks to me that they are not needed anymore.