Quantifiers and patterns

Use SMTPat and pattern for fine control over SMT proof.

The following example demonstrates the use of patterns in lemmas and universal quantifiers.

The proof of the test lemma below uses an assumed associativity lemma for the operation (+): t -> t -> t and the forall quantified formula in the pre-condition, stating commutativity of (+).

assume type t

assume val (+): t -> t -> t

assume val plus_associative: x:t -> y:t -> z:t -> Lemma
  (requires True)
  (ensures  ((x + y) + z == x + (y + z)))
  [SMTPat ((x + y) + z)]

irreducible let trigger (x:t) (y:t) = True

val test: x:t -> y:t -> z:t -> Lemma
  (requires (forall (a:t) (b:t).{:pattern (trigger a b)} trigger a b /\ a + b == b + a))
  (ensures  ((x + y) + z == (z + y) + x))
let test x y z = cut (trigger z y /\ trigger x (z + y))

The SMTPat annotation in plus_associative results in the lemma being instantiated for x,y, and z whenever Z3 creates a term that matches the pattern (x + y) + z during proof search.

The :pattern annotation in the quantifier in the requires clause of test plays a similar role, instantiating the quantifier for a and b whenever proof search creates a term trigger a b. The proof of test creates two such terms explicitly using cut. Note that irreducible increases verification performance.

The proof of the test lemma follows from:

(x + y) + z == x + (y + z)     SMTPat ((x + y) + z)    (x + y) + z == x + (y + z)
            == x + (z + y)     trigger z y             z + y == y + z
            == (z + y) + x     trigger x (z + y)       x + (z + y) == (z + y) + x
QED

This hints at one possible strategy that Z3 could use to deduce the validity of the lemma.