Quantifiers
===========

.. contents::
   :depth: 1
   :local:

Quantifying over infinite sets
------------------------------

| |backendloss_full|
| |backendverification_part| (:ref:`⤴ <verifying-quantifier-limitations>`)
| |backendagda_full|
| |backendrocq_full|
| |backendimandra_full|
| |backendisabelle_full|

One of the main advantages of Vehicle compared to a testing framework is
that it can be used to state and prove specifications that describe the
network's behaviour over an infinite set of values.

Suppose you have the following network which produces two outputs:

.. code-block:: agda

   @network
   f : Tensor Real [10, 10] -> Tensor Real [2]

and would like to specify that *for any input the network's first
output is always positive*.
This can be achieved by using the ``forall`` quantifier as follows:

.. code-block:: agda

   forall x . f x ! 0 > 0

which brings a new variable ``x`` of type ``Tensor Real [10, 10]`` into
scope. The variable ``x`` has no assigned value and therefore represents
an arbitrary input.

Similarly, if trying to specify that *there exists at least one input for which
the network's first output is positive*, the ``exists`` quantifier can be
used as follows:

.. code-block:: agda

   exists x . f x ! 0 > 0

As with lambda functions, the quantified variables can be annotated with
their types:

.. code-block:: agda

   exists (x : Tensor Real [10, 10]) . f x ! 0 > 0

and multiple variables can be quantified over at once:

.. code-block:: agda

   exists x i . f x ! i > 0

In many cases you don't want the property to hold over *all* the
values in the set, but only a (still infinite) subset of them.
For example, network inputs are frequently normalised to lie
within the range ``[0, 1]``. If the quantified variable's domain is not
also restricted to this range, then Vehicle will produce spurious
counter-examples to the specification.

In general such restrictions can be achieved by combining a quantifier
with an implication as follows:

.. code-block:: agda

   forall x. (forall i j . 0 <= x ! i ! j <= 1) => f x ! 0 > 0

Quantifying over finite sets
----------------------------

|backendall_full|

While most specifications will quantify over at least one variable
with an infinite domain, sometimes one might also want to quantify
over a finite set of values. There are multiple ways of doing this:

Quantifying over an ``Index``
+++++++++++++++++++++++++++++

The first approach is to quantify over a variable with the ``Index``
type. For example:

.. code-block:: agda

   pointwiseLess : Vector Real 3 -> Vector Real 3 -> Bool
   pointwiseLess x y = forall (i : Index 3) . x ! i < y ! i

is semantically equivalent to:

.. code-block:: agda

   pointwiseLess : Vector Real 3 -> Vector Real 3 -> Bool
   pointwiseLess x y = x ! 0 < y ! 0 and x ! 1 < y ! 1 and x ! 2 < y ! 2

The type annotation ``Index 3`` on the quantified variable ``i`` is
included for clarity but are not need in practice as it can be inferred
by the compiler.

Quantifying over a collection
+++++++++++++++++++++++++++++

Alternatively quantifiers can be modified with the ``in`` keyword to
quantify over all the values contained within a ``List``, ``Vector`` or ``Tensor``:

.. code-block:: agda

   myList : List Real
   myList = [0.4, 1.1, 0.2]

   myListInRange : Bool
   myListInRange = forall x in myList . 0 <= f x <= 1

During compilation Vehicle will automatically expand this out
to a sequence of conjunctions as follows:

.. code-block:: agda

   myListInRange : Bool
   myListInRange = 0 <= f 0.4 <= 1 and 0 <= f 1.1 <= 1 and 0 <= f 0.2 <= 1