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