# An Overview of Tactics

In this chapter, we quickly introduce several of the main concepts underlying Meta-F* and its use in writing tactics for proof automation. The goal is to get you quickly up to speed on basic uses of tactics. Subsequent chapters will revisit the concepts covered here in more detail, introduce more advanced aspects of Meta-F*, and show them at use in several case studies.

## Decorating assertions with tactics

As you know already, F* verifies programs by computing verification conditions (VCs) and calling an SMT solver (Z3) to prove them. Most simple proof obligations are handled completely automatically by Z3, and for more complex statements we can help the solver find a proof via lemma calls and intermediate assertions. Even when using lemma calls and assertions, the VC for a definition is sent to Z3 in one single piece (though SMT queries can be split via an option.). This “monolithic” style of proof can become unwieldy rapidly, particularly when the solver is being pushed to its limits.

The first ability Meta-F* provides is allowing to attach specific tactics to assertions. These tactics operate on the “goal” that we want to prove, and can “massage” the assertion by simplifying it, splitting it into several sub-goals, tweaking particular SMT options, etc.

For instance, let us take the the following example, where we want to
guarantee that `pow2 x`

is less than one million given that `x`

is
at most `19`

. One way of going about this proof is by noting that
`pow2`

is an increasing function, and that `pow2 19`

is less than
one million, so we try to write something like this:

```
let pow2_bound_19 (x:nat{x <= 19}) : Lemma (pow2 x < 1000000) =
assert (forall (x y : nat). x <= y ==> pow2 x <= pow2 y);
assert (pow2 19 == 524288);
assert (pow2 x < 1000000);
()
```

Sadly, this doesn’t work. First of all, Z3 cannot automatically
prove that `pow2`

is increasing, but that is to be expected.
We could prove this by a straightforward induction. However, we
only need this fact for `x`

and `19`

, so we can simply call
`FStar.Math.Lemmas.pow2_le_compat`

from the library:

```
let pow2_bound_19' (x:nat{x <= 19}) : Lemma (pow2 x < 1000000) =
FStar.Math.Lemmas.pow2_le_compat 19 x;
assert (pow2 19 == 524288);
assert (pow2 x < 1000000);
()
```

Now, the second assertion fails. Z3 will not, with the default fuel
limits, unfold pow2 enough times to compute `pow2 19`

precisely. (You can read more about how F* uses “fuel” to
control the SMT solver’s ability to unfold recursive definitions.) Here we will use our first call into Meta-F*: via
the `by`

keyword, we can attach a tactic to an assertion. In this
case, we’ll ask Meta-F* to `compute()`

over the goal, simplifying as
much as it can via F*’s normalizer, like this:

```
let pow2_bound_19'' (x:nat{x <= 19}) : Lemma (pow2 x < 1000000) =
FStar.Math.Lemmas.pow2_le_compat 19 x;
assert (pow2 19 == 524288) by compute ();
assert (pow2 x < 1000000);
()
```

Now the lemma verifies! Meta-F* reduced the proof obligation into a
trivial equality. Crucially, however, the `pow2 19 == 524288`

shape is
kept as-is in the postcondition of the assertion, so we can make use of
it! If we were just to rewrite the assertion into `524288 == 524288`

that would not be useful at all.

How can we know what Meta-F* is doing? We can use the `dump`

tactic to
print the state of the proof after the call to `compute()`

.

```
let pow2_bound_19''' (x:nat{x <= 19}) : Lemma (pow2 x < 1000000) =
FStar.Math.Lemmas.pow2_le_compat 19 x;
assert (pow2 19 == 524288) by (compute (); dump "after compute");
assert (pow2 x < 1000000);
()
```

With this version, you should see something like:

```
Goal 1/1
x: x: nat{x < 20}
p: pure_post unit
uu___: forall (pure_result: unit). pow2 x < 1000000 ==> p pure_result
pure_result: unit
uu___'0: pow2 x <= pow2 19
--------------------------------------------------------------------------------
squash (524288 == 524288)
(*?u144*) _
```

as output from F* (or in the goals buffer if you are using emacs with fstar-mode.el).
The `print`

primitive can also be useful.

A “goal” is some proof obligation that is yet to be solved. Meta-F*
allows you to capture goals (e.g. via `assert..by`

), modify them (such
as with `compute`

), and even to completely solve them. In this case, we
can solve the goal (without Z3) by calling `trivial()`

, a helper
tactic that discharges trivial goals (such as trivial equalities).

```
let pow2_bound_19'''' (x:nat{x <= 19}) : Lemma (pow2 x < 1000000) =
FStar.Math.Lemmas.pow2_le_compat 19 x;
assert (pow2 19 == 524288) by (
compute ();
trivial ();
qed ()
);
assert (pow2 x < 1000000);
()
```

If you `dump`

the state just after the `trivial()`

call, you should
see no more goals remain (this is what `qed()`

checks).

Note

Meta-F* does not yet allow a fully interactive style of proof, and hence we need to re-check the entire proof after every edit. We hope to improve this soon.

There is still the “rest” of the proof, namely that `pow2 x < 1000000`

given the hypothesis and the fact that the assertion holds. We call
this *skeleton* of the proof, and it is (by default) not handled by
Meta-F*. In general, we only use tactics on those assertions that are
particularly hard for the SMT solver, but leave all the rest to it.

## The `Tac`

effect

Note

Although we have seen a bit about monads and computational
effects in a previous chapter, we have yet to fully
describe F*’s effect system. So, some of what follows may be a bit
confusing. However, you don’t need to fully understand how the
`Tac`

effect is implemented to use tactics. Feel free to skip
ahead, if this section doesn’t make much sense to you.

What, concretely, are tactics? So far we’ve written a few simple ones, without too much attention to their structure.

Tactics and metaprograms in F* are really just F* terms, but *in a
particular effect*, namely `Tac`

. To construct interesting
metaprograms, we have to use the set of *primitives* provided by Meta-F*.
Their full list is in the `FStar.Tactics.Builtins`

module.
So far, we have actually not used any primitive directly, but
only *derived* metaprograms present in the standard library.

Internally, `Tac`

is implemented via a combination of 1) a state
monad, over a `proofstate`

, 2) exceptions and 3) divergence or
non-termination. The state monad is used to implicitly carry the
proofstate, without us manually having to handle all goals
explicitly. Exceptions are a useful way of doing error handling. Any
declared exception can be `raise`

’d within a metaprogram, and the
`try..with`

construct works exactly as for normal programs. There
are also `fail`

, `catch`

and `recover`

primitives.

Metaprograms cannot be run directly. This is needed to retain the
soundness of pure computations, in the same way that stateful and
exception-raising computations are isolated from the `Pure`

fragment
(and from each other). Metaprograms can only be used where F* expects
them , such as in an `assert..by`

construct. Here, F* will run the
metaprogram on an initial proofstate consisting (usually) of a single
goal, and allow the metaprogram to modify it.

To guarantee soundness, i.e., that metaprograms do not prove false things, all of the primitives are designed to perform small and correct modifications of the goals. Any metaprogram constructed from them cannot do anything to the proofstate (which is abstract) except modifying it via the primitives.

Having divergence as part of the `Tac`

effect may seem a bit odd,
since allowing for diverging terms usually implies that one can form a
proof of false, via a non-well-founded recursion. However, we should
note that this possible divergence happens at the *meta* level. If we
call a divergent tactic, F* will loop forever waiting for it to finish,
never actually accepting the assertion being checked.

As you know, F* already has exceptions and divergence. All `Dv`

and
`Ex`

functions can readily be used in Meta-F* metaprograms, as well as
all `Tot`

and `Pure`

functions. For instance, you can use all of the
`FStar.List.Tot`

module if your metaprogram uses lists.

## Goals

Essentially, a Meta-F* tactic manipulates a *proofstate*, which is
essentially a set of *goals*. Tactic primitives usually work on the
goals, for example by simplifying (like `compute()`

) or by breaking
them down into smaller *sub*-goals.

When proving assertions, all of our goals will be of the shape ```
squash
phi
```

, where `phi`

is some logical formula we must prove. One way to
break down a goal into subparts is by using the `mapply`

tactic, which
attempts to prove the goal by instantiating the given lemma or function,
perhaps adding subgoals for the hypothesis and arguments of the lemma.
This “working backwards” style is very common in tactics frameworks.

For instance, we could have proved the assertion that `pow2 x <= pow2 19`

in the following way:

```
assert (pow2 x <= pow2 19) by (mapply (`FStar.Math.Lemmas.pow2_le_compat));
```

This reduces the proof of `pow2 x <= pow2 19`

to `x <= 19`

(the
precondition of the lemma), which is trivially provably by Z3 in this
context. Note that we do not have to provide the arguments to the lemma:
they are inferred by F* through *unification*. In a nutshell, this means
F* finds there is an obvious instantiation of the arguments to make the
postcondition of the lemma and the current assertion coincide. When some
argument is *not* found via unification, Meta-F* will present a new goal
for it.

This style of proof is more *surgical* than the one above, since the
proof that `pow2 x <= pow2 19`

does not “leak” into the rest of the
function. If the proof of this assertion required several auxiliary
lemmas, or a tweak to the solver’s options, etc, this kind of style can
pay off in robustness.

Most tactics works on the *current* goal, which is the first one in
the proofstate. When a tactic reduces a goal `g`

into `g1,...,gn`

, the
new `g1,..,gn`

will (usually) be added to the beginning of the list of
goals.

In the following simplified example, we are looking to prove `s`

from `p`

given some lemmas. The first thing we do is apply the
`qr_s`

lemma, which gives us two subgoals, for `q`

and `r`

respectively. We then need to proceed to solve the first goal for
`q`

. In order to isolate the proofs of both goals, we can `focus`

on the current goal making all others temporarily invisible. To prove
`q`

, we then just use the `p_r`

lemma and obtain a subgoal for
`p`

. This one we will just just leave to the SMT solver, hence we
call `smt()`

to move it to the list of SMT goals. We prove `r`

similarly, using `p_r`

.

```
assume val p : prop
assume val q : prop
assume val r : prop
assume val s : prop
assume val p_q : unit -> Lemma (requires p) (ensures q)
assume val p_r : squash p -> Lemma r
assume val qr_s : unit -> Lemma (q ==> r ==> s)
let test () : Lemma (requires p) (ensures s) =
assert s by (
mapply (`qr_s);
focus (fun () ->
mapply (`p_q);
smt());
focus (fun () ->
mapply (`p_r);
smt());
()
)
```

Once this tactic runs, we are left with SMT goals to prove `p`

, which Z3
discharges immediately.

Note that `mapply`

works with lemmas that ensure an implication, or
that have a precondition (`requires`

/`ensures`

), and even those that take a
squashed proof as argument. Internally, `mapply`

is implemented via the
`apply_lemma`

and `apply`

primitives, but ideally you should not need to
use them directly.

Note, also, that the proofs of each part are completely isolated from
each other. It is also possible to prove the `p_gives_s`

lemma by calling
the sublemmas directly, and/or adding SMT patterns. While that style of
proof works, it can quickly become unwieldy.

## Quotations

In the last few examples, you might have noted the backticks, such as
in `(`FStar.Math.Lemmas.pow2_le_compat)`

. This is a *quotation*: it
represents the *syntax* for this lemma instead of the lemma itself. It
is called a quotation since the idea is analogous to the word “sun”
being syntax representing the sun.

A quotation always has type `term`

, an abstract type representing
the AST of F*.

Meta-F* also provides *antiquotations*, which are a convenient way of
modifying an existing term. For instance, if `t`

is a term, we can write
``(1 + `#t)`

to form the syntax of “adding 1” to `t`

. The part inside
the antiquotation (``#`

) can be anything of type `term`

.

Many metaprogramming primitives, however, do take a `term`

as an
argument to use it in proof, like `apply_lemma`

does. In this case,
the primitives will typecheck the term in order to use it in proofs
(to make sure that the syntax actually corresponds to a meaningful
well-typed F* term), though other primitives, such as
`term_to_string`

, won’t typecheck anything.

We will see ahead that quotations are just a convenient way of
constructing syntax, instead of doing it step by step via `pack`

.

## Basic logic

Meta-F* provides some predefined tactics to handle “logical” goals.

For instance, to prove an implication `p ==> q`

, we can “introduce” the
hypothesis via `implies_intro`

to obtain instead a goal for `q`

in a
context that assumes `p`

.

For experts in Coq and other provers, this tactic is simply called
`intro`

and creates a lambda abstraction. In F* this is slightly
more contrived due to squashed types, hence the need for an
`implies_intro`

different from the `intro`

, explained ahead, that
introduces a binder.

Other basic logical tactics include:

`forall_intro`

: for a goal`forall x. p`

, introduce a fresh`x`

into the context and present a goal for`p`

.

`l_intros`

: introduce both implications and foralls as much as possible.

`split`

: split a conjunction (`p /\ q`

) into two goals

`left`

/`right`

: prove a disjunction`p \/ q`

by proving`p`

or`q`

`assumption`

: prove the goal from a hypothesis in the context.

`pose_lemma`

: given a term`t`

representing a lemma call, add its postcondition to the context. If the lemma has a precondition, it is presented as a separate goal.

See the FStar.Tactics.Logic module for more.

## Normalizing and unfolding

We have previously seen `compute()`

, which blasts a goal with F*’s
normalizer to reduce it into a *normal form*. We sometimes need a
bit more control than that, and hence there are several tactics to
normalize goals in different ways. Most of them are implemented via a
few configurable primitives (you can look up their definitions in the
standard library)

`compute()`

: calls the normalizer with almost all steps enabled

`simpl()`

: simplifies logical operations (e.g. reduces`p /\ True`

to`p`

).

`whnf()`

(short for “weak head normal form”): reduces the goal until its “head” is evident.

`unfold_def `t`

: unfolds the definition of the name`t`

in the goal, fully normalizing its body.

`trivial()`

: if the goal is trivial after normalization and simplification, solve it.

The `norm`

primitive provides fine-grained control. Its type is
`list norm_step -> Tac unit`

. The full list of `norm_step`

s can
be found in the `FStar.Pervasives`

module, and it is the same one
available for the `norm`

marker in `Pervasives`

(beware of the
name clash between `Tactics.norm`

and `Pervasives.norm`

!).

## Inspecting and building syntax

As part of automating proofs, we often need to inspect the syntax of
the goal and the hypotheses in the context to decide what to do. For
instance, instead of blindly trying to apply the `split`

tactic (and
recovering if it fails), we could instead look at the *shape* of the
goal and apply `split`

only if the goal has the shape `p1 /\ p2`

.

Note: inspecting syntax is, perhaps obviously, not something we can
just do everywhere. If a function was allowed to inspect the syntax of
its argument, it could behave differently on `1+2`

and `3`

, which
is bad, since `1+2 == 3`

in F*, and functions are expected to map
equal arguments to the same result. So, for the most part, we cannot
simply turn a value of type `a`

into its syntax. Hence, quotations
are *static*, they simply represent the syntax of a term and one
cannot turn values into terms. There is a more powerful mechanism of
*dynamic quotations* that will be explained later, but suffice it to
say for now that this can only be done in the `Tac`

effect.

As an example, the `cur_goal()`

tactic will return a value of type
`typ`

(an alias for `term`

indicating that the term is really the
representation of an F* type) representing the syntax of the current
goal.

The `term`

type is *abstract*: it has no observable structure
itself. Think of it as an opaque “box” containing a term inside. A
priori, all that can be done with a `term`

is pass it to primitives
that expect one, such as `tc`

to type-check it or `norm_term`

to
normalize it. But none of those give us full, programatic access to
the structure of the term.

That’s where the `term_view`

comes in: following a classic idea
introduced by Phil Wadler, there is function
called `inspect`

that turns a `term`

into a `term_view`

. The
`term_view`

type resembles an AST, but crucially it is not
recursive: its subterms have type `term`

rather than `term_view`

.

```
noeq
type term_view =
| Tv_FVar : v:fv -> term_view
| Tv_App : hd:term -> a:argv -> term_view
| Tv_Abs : bv:binder -> body:term -> term_view
| Tv_Arrow : bv:binder -> c:comp -> term_view
...
```

The `inspect`

primitves “peels away” one level of the abstraction
layer, giving access to the top-level shape of the term.

The `Tv_FVar`

node above represents (an ocurrence of) a global name.
The `fv`

type is also abstract, and can be viewed as a `name`

(which
is just `list string`

) via `inspect_fv`

.

For instance, if we were to inspect ``qr_s`

(which we used above)
we would obtain a `Tv_FVar v`

, where `inspect_fv v`

is something
like `["Path"; "To"; "Module"; "qr_s"]`

, that is, an “exploded”
representation of the fully-qualified name `Path.To.Module.qr-s`

.

Every syntactic construct (terms, free variables, bound variables,
binders, computation types, etc) is modeled abstractly like `term`

and
`fv`

, and has a corresponding inspection functions. A list can be found
in `FStar.Reflection.Builtins`

.

If the inspected term is an application, `inspect`

will return a
`Tv_App f a`

node. Here `f`

is a `term`

, so if we want to know its
structure we must recursively call `inspect`

on it. The `a`

part
is an *argument*, consisting of a `term`

and an argument qualifier
(`aqualv`

). The qualifier specifies if the application is implicit or
explicit.

Of course, in the case of a nested application such as `f x y`

, this
is nested as `(f x) y`

, so inspecting it would return a `Tv_App`

node containing `f x`

and `y`

(with a `Q_Explicit`

qualifier).
There are some helper functions defined to make inspecting applications
easier, like `collect_app`

, which decompose a term into its “head” and
all of the arguments the head is applied to.

Now, knowing this, we would then like a function to check if the goal is
a conjunction.
Naively, we need to inspect the goal to check that it is of the shape
`squash ((/\) a1 a2)`

, that is, an application with two arguments
where the head is the symbol for a conjunction, i.e. `(/\)`

. This can
already be done with the `term_view`

, but is quite inconvenient due to
there being *too much* information in it.

Meta-F* therefore provides another type, `formula`

, to represent logical
formulas more directly. Hence it suffices for us to call `term_as_formula`

and match on the result, like so:

```
(* Check if a given term is a conjunction, via term_as_formula. *)
let isconj_t (t:term) : Tac bool =
match term_as_formula t with
| And _ _ -> true
| _ -> false
(* Check if the goal is a conjunction. *)
let isconj () : Tac bool = isconj_t (cur_goal ())
```

The `term_as_formula`

function, and all others that work on syntax,
are defined in “userspace” (that is, as library tactics/metaprograms) by
using `inspect`

.

```
noeq
type formula =
| True_ : formula
| False_ : formula
| And : term -> term -> formula
| Or : term -> term -> formula
| Not : term -> formula
| Implies: term -> term -> formula
| Forall : bv -> term -> formula
...
```

Note

For experts: F* terms are (internally) represented with a
locally-nameless representation, meaning that variables do not have
a name under binders, but a de Bruijn index instead. While this has
many advantages, it is likely to be counterproductive when doing
tactics and metaprogramming, hence `inspect`

*opens* variables when
it traverses a binder, transforming the term into a fully-named
representation. This is why `inspect`

is effectul: it requires
freshness to avoid name clashes. If you prefer to work with a
locally-nameless representation, and avoid the effect label, you can
use `inspect_ln`

instead (which will return `Tv_BVar`

nodes instead
of `Tv_Var`

ones).

Dually, a `term_view`

can be transformed into a `term`

via the
`pack`

primitive, in order to build the syntax of any term. However,
it is usually more comfortable to use antiquotations (see above) for
building terms.

## Usual gotchas

The

`smt`

tactic does*not*immediately call the SMT solver. It merely places the current goal into the “SMT Goal” list, all of which are sent to the solver when the tactic invocation finishes. If any of these fail, there is currently no way to “try again”.If a tactic is natively compiled and loaded as a plugin, editing its source file may not have any effect (it depends on the build system). You should recompile the tactic, just delete its object file, or use the F* option

`--no_plugins`

to run it via the interpreter temporarily,When proving a lemma, we cannot just use

`_ by ...`

since the expected type is just`unit`

. Workaround: assert the postcondition again, or start without any binder.

## Coming soon

Metaprogramming

Meta arguments and typeclasses

Plugins (efficient tactics and metaprograms,

`--codegen Plugin`

and`--load`

)Tweaking the SMT options

Automated coercions inspect/pack

`e <: C by ...`

Tactics can be used as steps of calc proofs.

Solving implicits (Steel)