# Implication and Universal Quantification

In this chapter, we’ll learn about two more separation logic
connectives, `@==>`

and `forall*`

. We show a few very simple
examples using them, though these will be almost trivial. In the next
chapter, on linked lists, we’ll see more significant uses of these
connectives.

## Trades, or Separating Ghost Implication

The library `module I = Pulse.Lib.Stick.Util`

defines the operator
*trade* `(@==>)`

and utilities for using it. In the literature, the
operator `p --* q`

is pronounced “p magic-wand q”; `p @==> q`

is
similar, though there are some important technical differences, as
we’ll see. We’ll just pronounce it `p for q`

, or `p trades for q`

.
Here’s an informal description of what `p @==> q`

means:

`p @==> q`

says that if you have`p`

then you cantradeit for`q`

. In other words, from`p ** (p @==> q)`

, you can derive`q`

. This step of reasoning is performed using a ghost function`I.elim`

with the signature below:ghost fn I.elim (p q:vprop) requires p ** (p @==> q) ensures q

Importantly, if you think of `p`

as describing permission on a
resource, the `I.elim`

makes you *give up* the permission `p`

and
get `q`

as a result. Note, during this step, you also lose
permission on the implication, i.e., `p @==> q`

lets you trade `p`

for `q`

just once.

But, how do you create a `p @==> q`

in the first place? That’s its
introduction form, shown below:

ghost fn I.intro (p q r:vprop) (elim: unit -> stt_ghost unit emp_inames (r ** p) (fun _ -> q)) requires r ensures p @==> q

That is, to introduce `p @==> q`

, one has to show hold permission
`r`

, such that a ghost function can transform `r ** p`

into
`q`

.

## Universal Quantification

Let’s look at our `regain_half`

predicate again:

```
let regain_half #a (x:GR.ref a) (v:a) =
pts_to x #one_half v @==> pts_to x v
```

This predicate is not as general as it could be: to eliminate it, it
requires the caller to prove that they holds `pts_to x #one_half v`

,
for the same `v`

as was used when the trade was introduced.

One could try to generalize `regain_half`

a bit by changing it to:

```
let regain_half #a (x:GR.ref a) (v:a) =
(exists* u. pts_to x #one_half u) @==> pts_to x v
```

This is an improvement, but it still is not general enough, since it
does not relate `v`

to the existentially bound `u`

. What we really
need is a universal quantifier.

Here’s the right version of `regain_half`

:

```
let regain_half_q #a (x:GR.ref a) =
forall* u. pts_to x #one_half u @==> pts_to x u
```

This says that no matter what `pts_to x #one_half u`

the context
has, they can recover full permission to it, *with the same witness*
`u`

.

The `forall*`

quantifier and utilities to manipulate it are defined
in `Pulse.Lib.Forall.Util`

. The introduction and elimination forms
have a similar shape to what we saw earlier for `@==>`

:

ghost fn FA.elim (#a:Type) (#p:a->vprop) (v:a) requires (forall* x. p x) ensures p v

The eliminator allows a *single* instantiation of the universally
bound `x`

to `v`

.

ghost fn FA.intro (#a:Type) (#p:a->vprop) (v:vprop) (f_elim : (x:a -> stt_ghost unit emp_inames v (fun _ -> p x))) requires v ensures (forall* x. p x)

The introduction form requires proving that one holds `v`

, and that
with `v`

a ghost function can produce `p x`

, for any `x`

.

Note, it’s very common to have universal quantifiers and trades together, so the library also provides the following combined forms:

ghost fn elim_forall_imp (#a:Type0) (p q: a -> vprop) (x:a) requires (forall* x. p x @==> q x) ** p x ensures q x

and

ghost fn intro_forall_imp (#a:Type0) (p q: a -> vprop) (r:vprop) (elim: (u:a -> stt_ghost unit emp_inames (r ** p u) (fun _ -> q u))) requires r ensures forall* x. p x @==> q x

## Trades and Ghost Steps

As a final example in this section, we show that one can use package
any ghost computation into a trade, including steps that may modify
the ghost state. In full generality, this makes `@==>`

behave more
like a view shift (in Iris terminology) than a wand.

Here’s a predicate `can_update`

which says that one can trade a half
permission to `pts_to x #one_half u`

for a full permission to a
*different value* `pts_to x v`

.

```
let can_update (x:GR.ref int) =
forall* u v. pts_to x #one_half u @==>
pts_to x v
```

In `make_can_update`

, we package a ghost-state update function into
a binary quantifier `forall* u v. ...`

.

```
ghost
fn make_can_update (x:GR.ref int)
requires pts_to x w
ensures pts_to x #one_half w ** can_update x
{
ghost
fn aux (u:int)
requires pts_to x #one_half w
ensures forall* v. pts_to x #one_half u @==> pts_to x v
{
ghost
fn aux (v:int)
requires pts_to x #one_half w ** pts_to x #one_half u
ensures pts_to x v
{
gather x;
x := v;
};
FA.intro_forall_imp _ _ _ aux;
};
share x;
FA.intro _ aux;
fold (can_update x);
}
```

And in `update`

, below, we instantiate it to update the reference
`x`

from `'u`

to `k`

, and also return back a `can_update`

predicate to the caller, for further use.

```
ghost
fn update (x:GR.ref int) (k:int)
requires pts_to x #one_half 'u ** can_update x
ensures pts_to x #one_half k ** can_update x
{
unfold can_update;
FA.elim #_ #(fun u -> forall* v. pts_to x #one_half u @==> pts_to x v) 'u;
FA.elim #_ #(fun v -> pts_to x #one_half 'u @==> pts_to x v) k;
I.elim _ _;
make_can_update x;
}
```