CODEWITHSUNDEEP
z3
JRR
JRR

Reputation: 6152

does z3 support proving inductive facts at all?

I understand that z3 cannot verify inductive proofs in general. But I am curious if there is a way to make it check something simple like:

; 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)

Right now it just loops forever on my machine.

Upvotes: 3

Views: 370

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Z3 will not make inductive arguments on its own. You can manually give it the induction hypothesis and ask it to finish the proof. This works for your example as follows:

(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

Upvotes: 5

Related Questions