Passing lemma to SMT in local scope of extrinsic proof (using)

[catalin-hritcu]

Chantal suggested that we could have a construct that feeds a given lemma (or set of lemmas?) to the SMT solver in the local scope. I can imagine syntaxes like using typable_empty_closed, or using typable_empty_closed [VPat (appears_free_in x e)] or using [typable_empty_closed [VPat (appears_free_in x e)], sometime_other_lemma [some_other_pattern]] or using list_lemmas where list lemmas is a "lemma database" for lists containing lemma-pattern pairs.

[catalin-hritcu]

As it become clearer in the discussion to #91, the simple fact that using would be explicitly converting lemmas from "functional programming" to logical form would be highly valuable, irrespective of the automation aspect.

[catalin-hritcu]

Started working on this with Guido Martínez, a potential new intern, and the simplest variant using lemma is already there (99df8c0).

For the using lemma pattern variant we have some issues though. Where should the variables in the patterns be bound? The current option we're considering is making pattern be a lambda re-binding all the variables of the lemma and then returning a pattern over them.

Here is a concrete example from lambda_omega. We proved this lemma

val esubst_extensional: s1:esub -> s2:esub{FEq s1 s2} -> e:exp ->
                        Lemma (requires True) (ensures (esubst s1 e = esubst s2 e))

but adding a global pattern to it would slow things down. So we want to add these patterns after the fact, in a local context. For instance, this could look as follows:

let esub_lam_hoist t e s =
  using esubst_extensional
    (fun s1 s2 e -> [SMTPat (esubst s1 e);  SMTPat (esubst s2 e)])

Note that under this implementation I need to rebind the 3 arguments of esubst_extensional using a lambda, and I could potentially give them different names. In the implementation I would need to replace the formals with the actuals before locally adding the pattern to the lemma. Is there code that already does this kind of replacement and which we could reuse?

A more invasive alternative would be to make using a special syntactic construct that introduces the variables from esubst_extensional in scope for the pattern. I would like to avoid this if possible though.

@nikswamy WDYT?

[nikswamy]

Sorry, missed this one. Would be good to revive discussion about this feature. Discussing it here with @jkzinzindohoue also

[catalin-hritcu]

Let me know if I can contribute more than just reiterating that this would be a great feature to have :)

[nikswamy]

After more than a year, it just occurred to me that we already have reasonable programmable support for the functionality requested here.

module M

type lemma =  //define some tags for the lemmas we want to export and control
  | A | B | C
let enable_lemma (l:lemma) = True //define a logically trivial trigger 
let using (l:lemma) : Lemma (enable_lemma l) = () //and a convenience to introduce the trigger

//Now, prove your lemmas A, B, and C and decorate them with the SMTPats 
val lemma_A: x1:t1 -> x2:t2 -> Lemma
    (requires P x1 x2)
    (ensures Q x1 x2)
    [SMTPat (R x1 x2); //with some pattern mentioning the bound variables, as usual 
     SMTPatT (enable_lemma A)] //but also the trigger pattern for A
let lemma_A x1 x2 = ...

//likewise for the other lemmas
val lemma_B:...

val lemma_C:...

Elsewhere:

let f  = 
 using M.A; //if you want to use M.lemma_A here to prove e, just say so
 e

[catalin-hritcu]

This is a cool trick, but I think there are a couple of things we could do better:

1. generate the type lemma automatically
2. maybe even generate the SMTPatT (enable_lemma A) automatically?
3. what I had in mind was specifying the SMTPat (R x1 x2) when using a lemma, not when defining it. Given 3, I'm still not convinced we should be using global SMTPats for this, but it's at least a workaround.

[nikswamy]

Don't agree with your first two points. Auto generating stuff is brittle, implicit and sometimes magical. It will accommodate some pattern that we find useful today but will not anticipate new patterns that occur to us randomly a year from now. The mechanism I proposed is simple and explicit...if you understand patterns there's no mystery here.

The third point is interesting: do you have a concrete example in mind where specifying a pattern at a use is easier than just applying the lemma to some x1,x2? In any case, you can always just reprove the same lemma trivially (using the first one) and bind a different pattern to it this time.

[catalin-hritcu]

do you have a concrete example in mind where specifying a pattern at a use is easier than just applying the lemma to some x1,x2

I think that almost any example where global SMTPats are too expensive should fit this category, since you almost never want to have to write explicit proofs. See for instance: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/LambdaOmega.fst#L96

Personally I would prefer if a simple and easy using construct would be the default for everyone who's not a super expert and just wants to tap into automation locally without big risk. That's what I would like to use for instance. SMTPat is a huge gun that can blow off in your hand. Don't think that giving this gun to everyone and showing people one trick that happens to be quite safe will be beneficial for their long term safety.

[nikswamy]

Of course, we all agree that adding SMTPat's globally is risky.

I don't see how this is an example of the pattern you requested: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/LambdaOmega.fst#L96

But, in the example you provided, there seems to be one very particular pattern to apply to orient the equality from left to right. I was looking for an example where the pattern you want to use cannot be selected reasonably at definition time and choice needed to be delayed until use, and in particular, where the use really needs the flexibility of the pattern, rather than applying esub_lam_hoist to some explicit arguments.

As for packaging up this pattern in some compiler-provided syntax: I'm just not sure it's really worth it. As a library writer, I pay a small upfront cost for adding my definition-specific 'using' combinator. For library users, there is no difference whether the compiler provided special support for it, or whether the library author coded it up.

In any case, since the required functionality is expressible currently and we're only arguing about convenience, this is falling down my long list of priorities. I wouldn't be opposed to a pull request that packages this up in some easier to use manner.

[catalin-hritcu]

Reopening this for the "package this up in some easier to use manner" part.

[nikswamy]

No example?

[nikswamy]

We also have

module FStar.Classical 
...

val forall_intro_with_pat (#a:Type) (#c: (x:a -> Type)) (#p:(x:a -> GTot Type0))
  ($pat: (x:a -> Tot (c x)))
  ($_: (x:a -> Lemma (p x)))
  :Lemma (forall (x:a).{:pattern (pat x)} p x)

We also have lemmas with SMT patterns now available in all scopes, not just top-level.