Computation holes for Meta-F*?

[nikswamy]

I was talking with @jaylorch after @mtzguido guido's seminar on tactics and metaprograms.

Say you want to metaprogram the proof of a lemma using something like this:

let f x1 ... xn : Lemma (requires p) (ensures q) = _ by some_tactic

This doesn't work today, because holes in Meta-F* just have value types. In this case, the tactic just sees that the goal is unit, and further, the tactic engine does not allow solving goals with terms that have non-trivial computation types.

To make this concrete, I'll use a simple example:

Say, I have this in scope:

module Lem
open FStar.Tactics

assume
val p (x:ℤ) : prop

assume
val prove_p (x:ℤ) : Lemma (requires x > 1) (ensures p x)

And now I want to metaprogram a proof of the following lemma:

let test (x:ℤ) : Lemma (requires x > 2) (ensures p x) = _ by (exact (quote (prove_p x)))

This fails for several related reasons:

1. The hole just has type unit

2. When checking the quoted term in exact, we check it just as a unit in the current environment, excluding the precondition of the lemma. So, this produces a proof obligation x > 1 which is not provable.

3. For the postcondition, what we do simply to check that any solution of the hole, i.e., any unit-typed term, is well-typed as the body of the lemma. In this case, that also produces a proof obligation of x > 2 ==> p x, which again is not provable (without the call to prove_p)

That brings me to the title of this post:

Can we introduce a new kind of "computation hole" in Meta-F*: i.e., a hole with a computation type? This would address the three problems above:

1. In this case, the hole would have type Lemma (requires x > 2) (ensures p x)

2. We could introduce a new primitive, e.g., exact_computation, which when typechecking a term for solving a computation hole, would typecheck it in a context where we expect it to have a computation type

3. We would use the computation type of the hole when building the VC for the context that includes it, not just the value type.

There are some subtleties though:

• Can other terms be dependent on computation holes? The simple answer is no. But, maybe there are some cases in which we would like to allow it, but that would bring up effect elaboration etc.

• Is it possible to solve a computation hole by anything other than by building some syntax and calling exact_computation? This also seems hard, since the behavior of a computation type is determined by the user-defined effect system. So, incrementally filling a computation hole by transforming one computation hole into another would require applying some effect combinator.

Despite these limitations, I think a facility to solve computation holes just by building some syntax t and solving using exact_computation t could be useful in metaprogramming things like lemmas that would be too painful to type out by hand.

WDYT @mtzguido @aseemr @jaylorch and others?

[jaylorch]

The reason I asked @nikswamy for something like this is that I'm used to writing proofs in F*, not Coq. That is, I write a proof by stringing together a series of hints: asserting relevant facts, triggering quantifiers, invoking useful lemmas with appropriate parameters, introducing and eliminating terms, etc. I work forward from the preconditions, establishing new facts along the way, but not being very thorough about it because I know Z3 will fill in simple gaps in the reasoning process. I don't write proofs like a Coq person would, i.e., carefully working backward from a goal to hypotheses, specifying the justification for every step in this process.

So, when I heard about there being tactics in F*, this is what I thought they'd be like. I thought I could program a tactic algorithm that would take as input some terms to reflect on, and would generate as output the various things I think of as being a proof: assertions, triggering terms, lemma invocations, etc. This would be very useful to me, since I have a lot of lemmas that I write that are tedious to write because they're just applying a basic algorithm.

For instance, I often have to generate proofs that predicates P1, P2, ..., P20 all preserve some invariant. Those predicates have a bunch of subterms, a few of which are hard to reason about. So I write a lemma for each complex subterm showing a key property about it with respect to the invariant. Then, for every top-level predicate, I write the proof by manually unfolding the predicate's definition, and, everywhere there's an invocation of a complex subterm, invoking the corresponding lemma. I'd like to be able to metaprogram this simple algorithm.

I know this is a different way of thinking than tactics are designed for. They're designed for programming a Coq-like backwards proof. But, given that this is a tactic language embedded in F*, I'm guessing there are a lot more users used to writing proofs in the forward-hinting style than the backwards-thorough style. So I may not be the only one who would appreciate a means to use F* tactics that way.

[mtzguido]

Hi Nik, Jay.

Indeed this is a usual problem when proving lemmas, due to having value types in most places. For Lemma and Pure, I think we can already do all that's needed, at the cost of some verbosity.

---

(I'll write a bit of recap here.)

As you notice, using _ by with a lemma does not help. The inferred type for an _ by in the place of the definition of a Lemma is just unit, and then we're pretty much lost. The usual workaround for this is asserting the postcondition again, as in:

val test0 : (x:ℤ) -> Lemma (requires x > 2) (ensures p x)
let test0 x = assert (p x) by (apply_lemma (`prove_p))

(Though admittedly that becomes a bit annoying when it is a complex formula.)

As noted, exact won't work, since that involves passing prove_p x via a value type, and that's just unit, so this fails to solve the goal squash (p x). However we do have the (slightly mangled) precondition in this variant, see this proofstate just before the apply_lemma:

Goal 1/1
x: int
p: pure_post unit
uu___: x > 2 /\ (forall (pure_result: unit). p x ==> p pure_result)
--------------------------------------------------------------------------------
squash (p x)
(*?u52*) _

This comes "for free" from the way we extract tactic-marked assertions from the VCs. Hence this is only the case for an assert ... by, and not an _ by.

---

Another alternative is to write a tactic to turn a goal of shape a -> b -> ... -> Lemma pre post (a value type!) into a goal for squash post in a proper context. This can already be done, using an auxiliary lemma (which should probably go into the library). See:

assume
val p (x:ℤ) : prop

assume
val prove_p (x:ℤ) : Lemma (requires x > 1) (ensures p x)

private
val __intro_pure :
  a:Type ->
  b:Type ->
  pre : (a -> pure_pre)  ->
  post : (x:a -> pure_post' b (pre x)) ->
  (x:a -> squash (pre x) -> y:b{post x y}) ->
  (x:a -> Pure b (requires (pre x)) (ensures (post x)))
private
let __intro_pure a b pre post f x = f x ()

let intro_pure () : Tac (binder * binder) =
  apply (`__intro_pure);
  let x = intro () in
  let pre = intro () in
  (x, pre)

val test : (x:ℤ) -> Lemma (requires x > 2) (ensures p x)
let test =
  _ by (let _ = intro_pure() in
        apply_lemma (`prove_p))

val test2 : (z:ℤ) -> (y:int) -> Lemma (requires z > y /\ y > 2) (ensures p z)
let test2 =
  _ by (let _ = intro () in
        let _ = intro_pure() in
        apply_lemma (`prove_p))

The __intro_pure function does not do anything very interesting. Its type is just complicated due to the thunking of the postcondition, but a simpler variant would still work here.

In the first example, this intro_pure () gives:

 Goal 1/1
x: int
uu___: squash (x > 2)
--------------------------------------------------------------------------------
y: unit{p x}
(*?u135*) _

which is really just squash (p x) unfolded, as expected.

---

Now, this is still not very satisfactory. A user would justifiably just want to write _ by ... and start proving. But, I'm wary about adding computation holes... that would bring many subtleties such as the ones you mention. Plus goals would stop being simply uvars (unless uvars can take computation types..?)

So if we could make this work via some encoding like the above that would be much better IMO. At least for proving...

[aseemr]

There may be a middle-ground between adding computation holes and exact_computation in full-force vs allowing proof of lemmas with syntax building and exact.

In the thread, there are already several subtle implementation details for adding computation holes. Another one that comes to mind is that, the typechecker today takes the expected (value) type of the hole from Env.expected_typ (unless explicitly annotated), but we don't have any notion of expected effect or even expected pre- and post. May be computation holes are always annotated, and desugaring helps by identifying certain common cases like the examples in the thread, but still need to think about it.

A middle ground may be that synth hook always returns a PURE or GHOST computation type, instead of forcing the synthesized term to be Tot or GTot. This computation type can then be folded into the rest of the VC as with any other term. This is how the usual typechecker works anyway, the environment may have expected type, but the typechecker compute the computation types and folds them in the VC.

So in this example, the programmer will write _ by (exact (quote (prove_p x))), typechecker will compute the computation type of this term to be Pure unit (requires x > 1) (ensures p x) (roughly). And then subcomp will kick in as usual to prove that Pure unit (requires x > 1) (ensures p x) <: Pure unit (requires x > 2) (ensures p x), which will succeed.

In terms of code, tc_synth today does this:

// run the tactic to get the term t, whose type the tactic has forced to be Tot tau
let t = env.synth_hook env typ ({ tau with pos = rng }) in
t, TcComm.lcomp_of_comp <| mk_Total typ, Env.trivial_guard

Instead it would be:

// run the tactic to get the term t, and a pure/ghost computation type c (c.t = tau)
let t, c = env.synth_hook env typ ({ tau with pos = rng }) in
t, c |> lcomp_comp, Env.trivial_guard

And the exact t tactic implementation instead of saying tc_tot_or_gtot_term t, would use, tc_pure_or_ghost_term t.

One unknown here is, how are these pre- and post (or wps) tracked in the proof state and exposed to the synth hook.