# Existential Quantification

A very common specification style in Pulse involves the use of the existential quantifier. Before we can start to write interesting examples, let’s take a brief look at how existential quantification works.

As mentioned in the introduction to Pulse, one of the connectives of Pulse’s separation logic is the existential quantifier. Its syntax is similar to F*’s existential quantifier, except it is written `exists*` instead of just `exists`, and its body is a `vprop`, as in the examples shown below.

```exists* (v:nat). pts_to x v

exists* v. pts_to x v

exists* v1 v2. pts_to x v1 ** pts_to y v2

...
```

## Some simple examples

Looking back to the `assign` example from the previous chapter (shown below), you may have wondered why we bothered to bind a logical variable `'v` in precondition of the specification, since it is never actually used in any other predicate.

```fn assign (#a:Type) (r:ref a) (v:a)
requires pts_to r 'v
ensures pts_to r v
{
r := v;
}
```

And indeed, another way to write the specification of `assign`, without the logical variable argument, is shown below.

```fn assign #a (x:ref a) (v:a)
requires
exists* w. pts_to x w
ensures
pts_to x v
{
x := v
}
```

This time, in the precondition, we use an existential quantifier to say that `assign` is callable in a context where `x` points to any value `w`.

Usually, however, the postcondition of a function relates the initial state prior to the call to the state after the call and existential variables are only in scope as far to the right as possible of the enclosing `vprop`. So, existential quantifiers in the precondition of a function are not so common.

To illustrate, the following attempted specification of `incr` does not work, since the existentially bound `w0` is not in scope for the postcondition.

```[@@expect_failure]
```pulse
fn incr #a (x:ref int)
requires
exists* w0. pts_to x w
ensures
pts_to x (w0 + 1) //w0 is not in scope here
{
let w = !x
x := w + 1
}
```
```

However, existential quantification often appears in postconditions, e.g., in order to abstract the behavior of function by underspecifying it. To illustrate, consider the function `make_even` below. It’s type states that it sets the contents of `x` to some even number `w1`, without specifying `w1` exactly. It also uses an existential quantification in its precondition, since its postcondition does not depend on the initial value of `x`.

```fn make_even (x:ref int)
requires
exists* w0. pts_to x w0
ensures
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
{
let v = !x;
x := v + v;
}
```

## Manipulating existentials

In a previous chapter on handling classical connectives, we saw how F* provides various constructs for introducing and eliminating logical connectives, including the existential quantifier. Pulse also provides constructs for working explicitly with existential quantifiers, though, usually, Pulse automation takes care of introducing and eliminating existentials behind the scenes. However, the explicit operations are sometimes useful, and we show a first example of how they work below

```fn make_even_explicit (x:ref int)
requires
exists* w0. pts_to x w0
ensures
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
{
with w0. assert (pts_to x w0);
let v = !x; // v:int; _:squash(v==w0); Ctxt=pts_to x v
x := v + v; //                          ... pts_to x (v + v)
introduce
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
with (v + v);
}
```

### Eliminating existentials

The form `with w0...wn. assert p; rest` is often used as an eliminator for an existential. When the context contains ```exists* x0...xn. p```, the `with` construct binds `w0 ... wn` to the existentially bound variables in the remainder of the scope `rest`.

A `show_proof_state` immediately after the ```with w0. assert (pts_to x w0)``` prints the following:

```- Current context:
pts_to x (reveal w0) **
emp
- In typing environment:
[w0#2 : erased int,
x#1 : ref int]
```

That is, we have `w0:erased int` in scope, and ```pts_to x (reveal w0)``` in context.

Here is another example usage of `with`, this time with multiple binders.

```fn make_even_explicit_alt (x y:ref int)
requires
exists* wx wy. pts_to x wx ** pts_to y wy ** pure (wx % 2 == wy % 2)
ensures
exists* wx' wy'. pts_to x wx' ** pts_to y wy' ** pure (wx' % 2 == 0)
{
with wx wy. _;
let vx = !x;
let vy = !y;
x := vx + vy;
introduce exists* wx' wy'. pts_to x wx' ** pts_to y wy' ** pure (wx' % 2 == 0)
with (vx + vy) vy;
}
```

When there is a single existential formula in the context, one can write `with x1..xn. _` to “open” the formula, binding its witnesses in scope. A `show_proof_state` after the first line prints:

```- Current context:
pts_to x (reveal wx) **
pts_to y (reveal wy) **
pure (eq2 (op_Modulus (reveal wx) 2) (op_Modulus (reveal wy) 2)) **
emp
- In typing environment:
[_#5 : squash (eq2 (op_Modulus (reveal wx) 2) (op_Modulus (reveal wy) 2)),
wy#4 : erased int,
wx#3 : erased int,
y#2 : ref int,
x#1 : ref int]
```

### Introducing existentials

The Pulse checker will automatically introduce existential formulas by introduces new unification variables for each existentially bound variable, and then trying to find solutions for those variables by matching `vprops` in the goal with those in the context.

However, one can also introduce existential formulas explicitly, using the `introduce exists*` syntax, as seen in the two examples above. In general, one can write

```introduce exists* x1 .. xn. p
with w1...wn
```

explicitly providing witnesses `w1..wn` for each of the existentially bound variables `x1..xn`.