Quantifiers and patterns

Use SMTPat and pattern for fine control over SMT proof.

Example

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