"intro" combinator for universal quantifiers

[Lysxia]

To prove a postcondition with a universal quantifier #[ensures(forall<x: _> _)], it would be nice to be able to have a way to put x in scope (like the intro tactic in Coq, or forall in Dafny).

---

I know of a currently working hacky solution which is to create an auxiliary lemma where the quantified variable becomes a function parameter:

#[ensures(forall<x: _> P(x))]
fn theorem() {
   proof_assert! { forall<x: _> lemma(x) == () }; // Hack to make theorem depend on lemma, so lemma is in the context of theorem in the Coma output
}

#[ensures(P(x))]
fn lemma(x: _) {
   ... // proof with x in scope
}

It's not pretty, but it seems to work, so this issue is more about a "nice to have" feature IMO.

---

What is missing is a new binder, call it intro:

#[ensures(forall<x: _> P(x))]
fn theorem() {
  pearlite! {
    intro<x: _> ... // Proof of P(x)
  }
}

The challenge is to figure out what the VCgen is supposed to do with this binder.

@jhjourdan proposes this WP (assuming that the expressions don't return a result so Q is just a proposition):

wp (intro<x> F(x)) (Q) = exists<x> wp (F(x)) (Q)

Which is logically correct because all types are inhabited. The question is whether SMT will be able to prove propositions of that form in practice.

We want that WP to be provable if Q is a quantified proposition Q = forall<y> P(y), and F(x) proves P(x).
Indeed, in that case wp (F(x)) (Q) is supposed to look like P(x) -> forall<y> P(y), and the WP wraps it in exists:

wp (intro<x> F(x)) (forall<y> P(y)) = exists<x> (P(x) -> forall<y> P(y))

That's a tautology also known as the drinker's paradox.

SMT solvers will be asked to refute it, i.e., they will be given the negation:

forall<x> (P(x) && exists<y> ~P(y))

and the desired outcome is that they find that to be unsatisfiable, by deriving a contradiction from that statement as a hypothesis, call it H.

That is possible by applying H twice: first we apply H to an arbitrary x0 to get access to the existential y such that P(y), and use that y to apply H a second time. The hope is that SMT solvers will be able to do that even if P has a complex shape.

[jhjourdan]

Thanks, @Lysxia, for writting all this down!

[xldenis]

This is really good. how would this combine with proof assertions? I think like all: in dafny it would be good if we can place assertions under the binder to guide the proof.

[jhjourdan]

I don't see why this could not work out-of-the-box with assertions.