title: Proving inductive facts in Z3
body: <p>I am trying to prove an inductive fact in Z3, an SMT solver by Microsoft. I know that Z3 does not provide this functionality in general, as explained in the <a href="http://rise4fun.com/z3/tutorial/guide" rel="nofollow">Z3 guide</a> (section 8: Datatypes), but it looks like this is possible when we constrain the domain over which we want to prove the fact. Consider the following example:</p>
  
  <pre><code>(declare-fun p (Int) Bool)
  (assert (p 0))
  
  (assert (forall ((x Int)) 
      (=&gt; 
      (and (&gt; x 0) (&lt;= x 20))
      (= (p (- x 1)) (p x) ))))
  (assert (not (p 20)))
  
  (check-sat)
  </code></pre>
  
  <p>The solver responds correctly with <code>unsat</code>, which means that <code>(p 20)</code> is valid. The problem is that when we relax this constraint any further (we replace <code>20</code> in the previous example by any integer greater than 20), the solver responds with <code>unknown</code>. </p>
  
  <p>I find this strange because it does not take Z3 long to solve the original problem, but when we increase the upper limit by one it becomes suddenly impossible. I have tried to add a pattern to the quantifier as follows:</p>
  
  <pre><code>(declare-fun p (Int) Bool)
  (assert (p 0))
  
  (assert (forall ((x Int)) 
      (! (=&gt; 
      (and (&gt; x 0) (&lt;= x 40))
      (= (p (- x 1)) (p x) )) :pattern ((&lt;= x 40)))))
  (assert (not (p 40)))
  
  (check-sat)
  </code></pre>
  
  <p>Which seems to work better, but now the upper limit is 40. Does this mean that I can better not use Z3 to prove such facts, or am I formulating my problem incorrectly?</p>