Quantifiers and patterns

F* completely turns off the SMT solver's fancy quantifier instantiation techniques (like mbqe) because they are not scalable and too unpredictable. Instead, F* relies entirely on e-matching and quantifier patterns. Basically a forall quantifier is instantiated only when its pattern is triggered, which produces a unifier for all its quantified variables.

While Z3 can sometimes also heuristically infer patterns, a good rule of thumb is that one shouldn't rely on that and instead provide good patterns for all quantifiers one introduces (or alternatively not use quantifiers and instantiate lemmas manually). You can use pattern to provide a pattern to an universal quantifier, and SMTPat to turn a top-level Lemma into a universally quantified formula that gets added to the proof context with the provided pattern (without SMTPat lemmas do not get added to the proof context and have to be called and fully instantiated manually, or using tactics).

The following examples demonstrate 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. Please note that associativity (and commutativity) are known to cause trouble to SMT solvers mixed with non-linear arithmetic; in such cases we advise using our canonicalization tactics.

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.

Multiple patterns can be used as follows:

forall (a:t) (b:t).{:pattern (a + b); (b + a)} a + b == b + a

Separating the patterns with a semicolon requires both to match (it's treated as a logical AND). You can instead allow either of the patterns to match (a logical OR) with \/. For example, consider this pattern from FStar.FunctionalExtensionality:

type gfeq (#a:Type) (#b:Type) (f:gfun a b) (g:gfun a b) =
    (forall x.{:pattern (f x) \/ (g x)} f x == g x)