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