Quantifiers and patterns

Use SMTPat and pattern for fine control over SMT proof.

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

The proof of the test lemma below uses an assumed associativity lemma for (+): t -> t -> t and the forall pre-condition requiring 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.

The proof of the test lemma from the 3 equalities:

(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.