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 uses an assumed lemma that defines associativity for (+): t -> t -> t and the forall pre-condition requiring commutativity for all (a:t) * (b:t).

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); cut (trigger x (z + y))

The SMTPat pattern in the associativity lemma results in the equality ((x + y) + z == x + (y + z)) being added to Z3's environment, whenever F* sees the pattern ((x + y) + z).

The :pattern in the forall defines an explicit trigger that adds the equality a + b == b + a whenever the trigger (a + b) appears in a cut.

The proof of the test lemma follows 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