I read an earlier very useful post on using the seq.foldl function and decided to (unsuccessfully) prove sum of a list using it:
(declare-const in (Seq Int))
(declare-const i Int)
(declare-const acc Int)
(define-fun sum_seq ((s (Seq Int))) Int
(seq.foldl (lambda ((acc Int) (x Int)) (+ acc x)) 0 s)
)
(assert
(not
(=>
(and (>= i 0) (< i (seq.len in))
(= acc (sum_seq (seq.extract in 0 i) ))
)
(and
(<= i (seq.len in))
(= (+ acc (seq.nth in i))
(sum_seq (seq.extract in 0 (+ 1 i)) ))
)
)
))
z3 got stuck and never returned. Can someone please point out what I did wrong?
You're not doing anything wrong; it's just that neither z3 nor any other current SMT solver is capable of proving such facts out-of-the-box.
seq.foldl captures the recursive nature of folding down a sequence, and whenever you have a recursive definition, any interesting property you want to prove about it will have to use induction. And SMT solvers don't do induction. This is the state-of-art as of 2023, though of course maybe the SMT solvers 10 years from now will prove these without breaking a sweat.
But if your goal is to prove properties of recursive functions (whether they're defined using fold, or directly using define-fun-rec), you should know that SMT solvers are not very good at such tasks. In practice, one uses a proper theorem prover (such as Isabelle, ACL2, Coq, HOL,.. you name it), which might use an SMT solver to dispatch subgoals. That is, they would set up the inductive proof, and then ask the SMT solver to prove the base case and the inductive step. (They don't have to, of course, but they can.) This is the best use of SMT solvers in these domains. Another example system is Dafny (https://dafny.org) which takes this idea quite far afield, using z3 underneath.
To sum up, SMT solvers (as they stand today) are not good at inductive reasoning. They're better at many other things of course, and many systems employ them to great effect to take advantage of their reasoning power.
Just as a side note, the following is how I'd write your problem, which is more idiomatic:
(define-fun sum_seq ((s (Seq Int))) Int
(seq.foldl (lambda ((acc Int) (x Int)) (+ acc x)) 0 s)
)
(declare-const i Int)
(declare-const in (Seq Int))
(assert (and (>= i 0) (< i (- (seq.len in) 1))))
(define-const uptoi Int (sum_seq (seq.extract in 0 i)))
(define-const uptoip1 Int (sum_seq (seq.extract in 0 (+ 1 i))))
(assert (not (= uptoip1 (+ (seq.nth in i) uptoi))))
(check-sat)
Not that this'll make any difference; the solver will still loop on it.