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