Quantifiers and patterns

See this section of PoP-in-FStar for more information about quantifiers and triggers, and especially this section on opaque definitions and triggers for more details and explanation.

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 when mixed with non-linear arithmetic; in such cases we advise not using patterns but 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.

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:

let feq_g (#a:Type) (#b:a -> Type) (f:arrow_g a b) (g:arrow_g a b)
  = forall x.{:pattern (f x) \/ (g x)} f x == g x

Interaction of triggers and the simplifier

Consider the following example:

assume val f(x: int) : int
assume val g(x: int) : int

let finfo (x: int)
  : Lemma (ensures f x = g x)
          [SMTPat (f (f x))] =
  admit()

[@@expect_failure]
let useit (x: int)
  : Lemma (ensures f x = g x) =
  assert (f (f x) = f (f x)) //this trivial equality is simplified to True before the SMT solver sees it

The proof of useit fails because what the SMT solver sees is something close to True ==> f x = g x and there is no trigger for the pattern of finfo.

Here's an (artificial) variant that succeeds, since the assertion cannot be simplified.

let useit (x: int)
  : Lemma (ensures f x = g x) =
  assert (1 + f (f x) = f (f x) + 1) //But this one isn't simplified and works as a trigger

Another way to specifically introduce a trigger is like this:

let trigger (#a:Type) (x:a) = True

let useit2 (x: int)
  : Lemma (ensures f x = g x) =
  assert (trigger (f (f x)))

Since the simplifier does not unfold definitions by default, the assertion remains, the SMT solver sees trigger (f (f x)) ==> f x = g x and now finfo's pattern can be instantiated.

This style of explicit triggering is a bit unusual. If you really know exactly how to instantiate a lemma, it's often better to just call it. But, sometimes this style can be useful, e.g., if there is a long chain of lemmas to call, and the SMT solver can do most of it, except for one step which is missing a trigger.