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))