Hi Andrew,
I'm afraid your example is more complicated than it looks at first sight. I would expect to be able to prove theorems about your function only when the argument set is finite, and in that sense your second definition may be easier to work with.
Most importantly, you want to prove the following theorem:
LEMMA SetSumDefined ==
ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)
PROVE SetSum(S) = [T \in SUBSET S |-> IF T = {} THEN 0 ELSE ...]
This is not obvious because a TLA+ function definition
f[x \in S] == exp
is really shorthand for
f == CHOOSE f : f = [x \in S |-> exp]
and as with any CHOOSE _expression_, you have to show that a suitable value (here, function) exists. There is some library support for carrying out the required proofs: you want to EXTEND module WellFoundedInduction and use lemma WFInductiveDefLemma, which requires proving several hypotheses. (The last hypothesis is trivial if you remember the expansion explained above.) Most importantly, you need to prove that the subset order is well-founded over subsets of the finite set S introduced in the hypothesis of lemma SetSumDefined. The necessary infrastructure ought to be in place, though I'd be interested in hearing if you run into problems.
I'd suggest that you start with a simpler recursive function definition over natural numbers as a warm-up exercise. Look at module NaturalsInduction, which has the required helper lemmas. At the bottom of the module you'll find an example of how these lemmas are applied for the definition of the factorial function.
Regards,
Stephan
I've been enjoying playing around with TLAPS over the holidays, with the intention of writing a Wikipedia article if I find enough material to work with. I'm impressed with the ability of the SMT solver to prove theorems of arithmetic, but have run into a wall when trying to prove theorems requiring primitive-recursive function definitions.
Let's consider a simple primitive-recursive function, which sums all the elements of a set of numbers in Nat:
SetSumV0[S \in SUBSET Nat] ==
ELSE LET e == CHOOSE val \in S : TRUE IN
e + SetSumV0[S \ {e}]
TLAPS fails to prove this base case theorem:
THEOREM SetSumV0BaseCase == SetSumV0[{}] = 0
Although strangely, if we rewrite SetSum as an operator TLAPS has more success:
SetSumV1(S) ==
LET SS[T \in SUBSET S] ==
IF T = {} THEN 0
ELSE LET e == CHOOSE val \in T : TRUE IN
e + SS[T \ {e}]
IN SS[S]
THEOREM SetSumV1BaseCase == SetSumV1({}) = 0
BY DEF SetSumV1
Q1) Why does TLAPS find SetSumV1 easier to analyze than SetSumV0? Is it because SetSumV1 drops the dependency on Nat?
TLAPS is unable to prove this theorem about SetSumV1:
THEOREM SetSumV1Test == SetSumV1({2}) = 2
I understand this isn't a very useful theorem to prove, but we also run into a wall trying to prove more general statements quantifying over the Natural numbers so this seems a good place to start.
Q2) Is there a way for me to give TLAPS more information about how SetSumV1 works without introducing axioms and assumptions beyond the literal text of the function itself? What information can TLAPS extract from this primitive-recursive function?
Thanks!
Andrew
--
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...@googlegroups.com.
To post to this group, send email to
tla...@googlegroups.com.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.