z3 - z3 完全支持证明归纳事实吗？

Question

我知道 z3 无法验证一般的归纳证明。但我很好奇是否有办法让它检查一些简单的东西，比如:

; returns the same input list after iterating through each element
(declare-fun iterate ((List Int)) (List Int))

(declare-const l (List Int))

(assert (forall ((l (List Int)))
  (ite (= l nil)
    (= (iterate l) nil)
    (= (iterate l) (insert (head l) (iterate (tail l))))
  )
))

(assert (not (= l (iterate l))))
(check-sat)

现在它只是在我的机器上永远循环。

Answer 1

Z3不会自己做归纳论证。你可以手动给它归纳假设，让它完成证明。这适用于您的示例，如下所示:

(declare-fun iterate ((List Int)) (List Int))

(assert (forall ((l (List Int)))
  (ite (= l nil)
    (= (iterate l) nil)
    (= (iterate l) (insert (head l) (iterate (tail l)))))))

; define list length for convenience in stating the induction hypothesis
(declare-fun length ((List Int)) Int)
(assert (= (length nil) 0))
(assert (forall ((x Int) (l (List Int)))
  (= (length (insert x l)) (+ 1 (length l)))))

(declare-const l (List Int))

; here comes the induction hypothesis: 
; that the statement is true for all lists shorter than l
(assert (forall ((ihl (List Int))) 
  (=> (< (length ihl) (length l))
      (= ihl (iterate ihl)))))

; we now ask Z3 to show that the result follows for l        
(assert (not (= l (iterate l))))
(check-sat)  ; reports unsat as desired