# IVy as a theorem prover

In the development of systems, we sometimes have to reason about mathematical functions and relations in ways that automated theorem provers can’t handle reliably. For these cases, IVy provides a facility that allows the user to supply the necessary proofs. IVy’s approach to theorem proving is designed to make maximal use of automated provers. We do this by localizing the proof into “isolates”. Our verification conditions in each isolate are confined to a logical fragment or theory that an automated prover can handle reliably.

## Primitive judgments

A logical development in IVy is a succession of statements or
*judgments*. Each judgment must be justified by a primitive axiom or
inference rule.

# Type declarations

On such primitive is a type declaration, like this:

```
type t
```

This judgment can be read as “let `t`

be a type”. It is admissible
provided `t`

is new symbol that has not been used up to this point
in the development.

# Functions and individuals

We can introduce a constant like this:

```
individual n : t
```

where `n`

is new. This judgment can be read as “let `n`

be a term of type
`t`

” and is admissible if symbol `n`

has not been used up to this point
in the development.

Similarly, we can introduce new function and relation symbols:

```
function f(X:t) : t
relation r(X:t,Y:t)
```

The first judgment can be read as “for any term *X* of type *t*, let
*f*(*X*) be a term of type *t*”. The second says “for any terms
*X,Y* of type *t*, let *r*(*X*,*Y*) be a proposition” (a term of
type `bool`

).

# Axioms

An *axiom* is a proposition whose truth is admitted by fiat. For
example:

```
axiom [symmety_r] r(X,Y) -> r(Y,X)
```

The free variables *X*,*Y* in the formula are taken as universally
quantified. The text `symmetry_r`

between brackets is a name for the
axiom and is optional. The axiom is simply admitted in the current
context without proof. Axioms are dangerous, since they can
introduce inconsistencies. You should use axioms only if you are
developing a foundational theory and you know what you are doing, or
to make a temporary assumption that will later be removed.

# Properties

A *property* is a proposition that can be admitted as true only if
it follows logically from judgments in the current context. For
example:

```
property [myprop] r(n,X) -> r(X,n)
```

A property requires a proof (see below). If a proof is not supplied,
IVy applies its default proof tactic `auto`

. This calls the
automated prover Z3 to attempt to prove the property from the
previously admitted judgments in the current context.

The `auto`

tactic works by generating a *verification condition* to
be checked by Z3. This is a formula whose validity implies that the
property is true in the current context. In this case, the
verification condition is:

```
# (forall X,Y. r(X,Y) -> r(Y,X)) -> (r(n,X) -> r(X,n))
```

That is, it states that axiom `symmetry_r`

implies property `myprop`

.
IVy checks that this formula is within a logical fragment that Z3 can
decide, then passes the formula to Z3. If Z3 finds that the formula is
valid, the property is admitted.

# Definitions

A definition is a special form of axiom that cannot introduce an inconsistency. As an example:

```
function g(X:t) : t
definition g(X) = f(X) + 1
```

This can be read as “for all *X*, let *g*(*X*) equal *f*(*X*) + 1”. The
definition is admissible if the symbol *g* is “fresh”, meaning it
does not occur in any existing properties or definitions in the
current context. Further *g* must not occur on the right-hand side
of the equality (that is, a recursive definition is not admissible
without proof – see “Recursion” below).

# Theory instantiations

IVy has built-in theories that can be instantated with a specific type
as their carrier. For example, the theory of integer arithmetic is
called `int`

. It has the signature `{+,-,*,/,<}`

, plus the integer
numerals, and provides the axioms of Peano arithmetic. To instantiate
the theory `int`

using type *u* for the integers, we write:

```
type u
interpret u -> int
```

This declaration requires that type `u`

is not previously interpreted
and that the symbols `{+,-,*,/,<}`

in the signature of `int`

are
fresh. Notice, though, that the symbols `{+,-,*,/,<}`

are
overloaded. This means that `+`

over distinct types is considered to
be a distinct symbol. Thus, we can we can instantiate the `int`

theory over different types (and also instantiate other theories that
have these symbols in their signature).

## Schemata

A *schema* is a compound judgment that takes a collection of judgments
as input (the premises) and produces a judgment as output (the
conclusion). If the schema is valid, then we can provide any
type-correct values for the premises and the conclusion will follow.

Here is a simple example of a schema taken as an axiom:

```
axiom [congruence] {
type d
type r
function f(X:d) : r
#--------------------------
property X = Y -> f(X) = f(Y)
}
```

The schema is contained in curly brackets and gives a list of premises
following a conclusion. In this case, it says that, given types *d* and *r* and a function *f* from
*d* to *r* and any values *X*,*Y* of type *d*, we can infer that *X*=*Y* implies
*f*(*X*) = *f*(*Y*). The dashes separating the premises from the conclusion are
just a comment. The conclusion is always the last judgement in the schema.
Also, notice the declaration of function *f* contains a variable *X*. The scope of this
variable is only the function declaration. It has no relation to the variable *X* in the conclusion.

The keyword `axiom`

tells IVy that this schema should be taken as valid
without proof. However, as we will see, the default `auto`

tactic treats a schema differently from a simple proposition. That is,
a schema is never used by default, but instead must be explicitly
instantiated. This allows is to express and use facts that, if they
occurred in a verification condition, would take us outside the
decidable fragment.

Any judgment that has been admitted in the current context can be
*applied* in a proof. When we apply a schema, we supply values for its
premises to infer its conclusion.

```
property [prop_n] Z = n -> Z + 1 = n + 1
proof
apply congruence
```

The `proof`

declaration tells IVy to apply the axiom schema `congruence`

to prove the property.
IVy tries to match the proof goal `prop_n`

to the schema’s conclusion by picking particular
values for premises, that is, the types *d*,*r* and function *f*. It also chooses terms for the
the free variables *X*,*Y* occurring in the schema. In this case, it
discovers the following assignment:

```
# d = t
# r = t
# X = Z
# Y = n
# f(N) = N + 1
```

After plugging in this assignment, the conclusion of the rule exactly matches the property to be proved, so the property is admitted.

The problem of finding an assignment such as the one above is one of “second order matching”. It is a hard problem, and the answer is not unique. In case IVy did not succeed in finding the above match, we could also have written the proof more explicitly, like this:

```
property [prop_n_2] Z = n -> Z + 1 = n + 1
proof
apply congruence with X=Z, Y=n, f(X) = X:t + 1
```

Each of the above equations acts as a constraint on the
assignment. That is, it must convert *X* to
*Z*, *Y* to *n* and *f*(*X*) to *X* + 1. Notice that we had to
explicitly type *X* on the right-hand side of the last equation,
since its type couldn’t be inferred (and in fact it’s not the same
as the type of *X* on the left-hand side, which is *d*).

It’s also possible to write constraints that do not allow for any assignment. In this case, Ivy complains that the provided match is inconsistent.

# Proof chaining

A premise of a schema can itself be a property. When applying the
schema, we are not required to provide values for the premises that
are properties. An unsupplied premise becomes a *subgoal* which we
must then prove.

For example, consider the following axiom schema:

```
relation man(X:t)
relation mortal(X:t)
axiom [mortality_of_man] {
property [prem] man(X)
#---------------
property mortal(X)
}
```

The scope of free variables such as *X* occurring in properties is
the entire schema. Thus, this schema says that, for any term *X* of
type `t`

, if we can prove that `man(X)`

is true, we can prove that
`mortal(X)`

is true.

We take as a given that Socrates is a man, and prove he is mortal:

```
individual socrates : t
axiom [soc_man] man(socrates)
property mortal(socrates)
proof
apply mortality_of_man
```

The axiom `mortality _of_man`

, requires us supply the premise
`man(socrates)`

. Since this premise isn’t present in our theorem,
IVy sets it up as a proof subgoal. We didn’t supply a proof of this
subgoal, so IVy uses its default tactic `auto`

, which in this case
can easily prove that the axiom `man(socrates)`

implies
`man(socrates)`

.

If we wanted to prove this manually, however, we could continue our proof by
applying the axiom `soc_man`

, like this:

```
property mortal(socrates)
proof
apply mortality_of_man;
apply soc_man
```

The prover maintains a list of proof goals, to be proved in order
from first to last. Applying a rule, if it succeeds, removes the
first goal from the list, possibly replacing it with subgoals. At
the end of the proof, the prover applies its default tactic `auto`

to the remaining goals.

In the above proof, we start with this goal:

```
# property mortal(socrates)
```

Applying axiom `mortality_of_man`

we are left with the following subgoal:

```
# property man(socrates)
```

Applying axiom `soc_man`

then leaves us with no subgoals.

Notice that the proof works backward from conclusions to premises.

A note on matching: There may be many ways to match a given proof goal to the conclusion of a schema. Different matches can result in different sub-goals, which may affect whether a proof succeeds. IVy doesn’t attempt to verify that the match it finds is unique. For this reason, when it isn’t obvious there there is a single match, it may be a good idea to give the match explicitly (though we didn’t above, as in this case there is only one possible match).

When chaining proof rules, it is helpful to be able to see the
intermediate subgoals. This can be done with the `showgoals`

tactic,
like this:

```
property mortal(socrates)
proof
apply mortality_of_man;
showgoals;
apply soc_man
```

When checking the proof, the `showgoals`

tactic has the effect of
printing the current list of proof goals, leaving the goals unchanged.
A good way to develop a proof is to start with just the tactic `showgoals`

, and to add tactics
before it. Running the Ivy proof checker in an Emacs compilation buffer
is a convenient way to do this.

# Theorems

Thus far, we have seen schemata used only as axioms. However, we can also
prove the validity of a schema as a *theorem*. For example, here is a theorem
expressing the transitivity of equality:

```
theorem [trans] {
type t
property X:t = Y
property Y:t = Z
#--------------------------------
property X:t = Z
}
```

We don’t need a proof for this, since the `auto`

tactic can handle
it. The verification condition that ivy generates is:

```
# X = Y & Y = Z -> X = Z
```

Here is a theorem that lets us eliminate universal quantifiers:

```
theorem [elimA] {
type t
function p(X:t) : bool
property forall Y. p(Y)
#--------------------------------
property p(X)
}
```

It says, for any predicate *p*, if `p(Y)`

holds for all *Y*, then
`p(X)`

holds for a particular *X*. Again, the `auto`

tactic can
prove this easily. Now let’s derive a consequence of these facts. A
function *f* is *idempotent* if applying it twice gives the same
result as applying it once. This theorem says that, if *f* is
idempotent, then applying *f* three times is the same as applying it
once:

```
theorem [idem2] {
type t
function f(X:t) : t
property forall X. f(f(X)) = f(X)
#--------------------------------
property f(f(f(X))) = f(X)
}
```

The auto tactic can’t prove this because the premise contains a function cycle with a universally quantified variable. Here’s the error message it gives:

```
# error: The verification condition is not in the fragment FAU.
#
# The following terms may generate an infinite sequence of instantiations:
# proving.ivy: line 331: f(f(X_h))
```

This means we’ll need to apply some other tactic. Here is one possible proof:

```
proof
apply trans with Y = f(f(X));
apply elimA with X = f(X);
apply elimA with X = X
```

We think this theorem holds because `f(f(f(X)))`

is equal to `f(f(X))`

(by idempotence of *f*) which in turn is equal to `f(X)`

(again, by
idempotence of *f*). This means we want to apply the transitivy rule, where
the intermediate term *Y* is `f(f(x))`

. Notice we have to give the value of *Y*
explicitly. Ivy isn’t clever enough to guess this intermediate term for us.
This gives us the following two proof subgoals:

```
# theorem [prop2] {
# type t
# function f(V0:t) : t
# property [prop5] forall X. f(f(X)) = f(X)
# #----------------------------------------
# property f(f(f(X))) = f(f(X))
# }
# theorem [prop3] {
# type t
# function f(V0:t) : t
# property [prop5] forall X. f(f(X)) = f(X)
# #----------------------------------------
# property f(f(X)) = f(X)
# }
```

Now we see that the conclusion in both cases is an instance of the
idempotence assumption, for a particular value of *X*. This means
we can apply the `elimA`

rule that we proved above. In the first case,
the value of `X`

for which we are claiming idempotence is `f(X)`

.
With this assignment, IVy can match `p(X)`

in theorem `elimA`

to `f(f(f(X))) = f(X)`

.
This substituion produces a new subgoal as follows:

```
# theorem [prop2] {
# type t
# function f(V0:t) : t
# property [prop5] forall X. f(f(f(X))) = f(f(X))
# #----------------------------------------
# property forall Y. f(f(f(Y))) = f(f(Y))
# }
```

This goal is trivial, since the conclusion is exactly the same as one
of the premises, except for the names of bound variables. Ivy proves
this goal automatically and drops it from the list. This leaves the
second subgoal `prop3`

above. We can also prove this using `elimA`

. In
this case `X`

in the `elimA`

rule corresponds to `X`

in our goal.
Thus, we write `apply elimA with X = X`

. This might seem a little
strange, but keep in mind that the `X`

on the left refers to `X`

in
the `elimA`

rule, while `X`

on the right refers to `X`

in our goal. It
just happens that we chose the same name for both variables.

Once again, the subgoal we obtain is trivial and Ivy drops it. Since there are no more subgoals, the proof is now complete.

#### The deduction library

Facts like `trans`

and `elimA`

above are included in the library
`deduction`

. This library contains a complete set of rules of a system
natural deduction
for first-order logic with equality.

# Recursion

Recursive definitions are permitted in IVy by instantiating a
*definitional schema*. As an example, consider the following axiom schema:

```
# axiom [rec[u]] {
# type q
# function base(X:u) : q
# function step(X:q,Y:u) : q
# fresh function fun(X:u) : q
# #---------------------------------------------------------
# definition fun(X:u) = base(X) if X <= 0 else step(fun(X-1),X)
# }
```

This axiom was provided as part of the integer theory when we
interpreted type *u* as `int`

. It gives a way to construct a fresh
function `fun`

from two functions:

`base`

gives the value of the function for inputs less than or equal to zero.`step`

gives the value for positive*X*in terms of*X*and the value for*X*-1

A definition schema such as this requires that the defined function
symbol be fresh. With this schema, we can define a recursive function that
adds the non-negative numbers less than or equal to *X* like this:

```
function sum(X:u) : u
definition [defsum] {
sum(X:u) = 0 if X <= 0 else (X + sum(X-1))
}
proof
apply rec[u]
```

Notice that we wrote the definition in curly brackets. This causes Ivy to
treat it as an axioms schema, as opposed to a simple axiom.
We did this because the definition has a universally quantified variable
`X`

under arithmetic operators, which puts it outside the decidable
fragment. Because this definition is a schema, when we want to use it,
we’ll have to apply it explicitly,

In order to admit this definition, we applied the definition
schema `rec[u]`

. Ivy infers the following assignment:

```
# q=t, base(X) = 0, step(X,Y) = Y + X, fun(X) = sum(X)
```

This allows the recursive definition to be admitted, providing that
`sum`

is fresh in the current context (i.e., we have not previously refered to
`sum`

except to declare its type).

### Extended matching

Suppose we want to define a recursive function that takes an additional
parameter. For example, before summing, we want to divide all the
numbers by *N*. We can define such a function like this:

```
function sumdiv(N:u,X:u) : u
definition
sumdiv(N,X) = 0 if X <= 0 else (X/N + sumdiv(N,X-1))
proof
apply rec[u]
```

In matching the recursion schema `rec[u]`

, IVy will extend the
function symbols in the premises of `rec[u]`

with an extra parameter *N* so that
schema becomes:

```
# axiom [rec[u]] = {
# type q
# function base(N:u,X:u) : q
# function step(N:u,X:q,Y:u) : q
# fresh function fun(N:u,X:u) : q
# #---------------------------------------------------------
# definition fun(N:u,X:u) = base(N,X) if X <= 0 else step(N,fun(N,X-1),X)
# }
```

The extended schema matches the definition, with the following assignment:

```
# q=t, base(N,X)=0, step(N,X,Y)=Y/N+X, fun(N,X) = sum2(N,X)
```

This is somewhat as if the functions were “curried”, in which case the
free symbol `fun`

would match the partially applied term `sumdiv N`

.
Since Ivy’s logic doesn’t allow for partial application of functions,
extended matching provides an alternative. Notice that,
to match the recursion schema, a function definition must be
recursive in its *last* parameter.

# Induction

The `auto`

tactic can’t generally prove properties by induction. For
that IVy needs manual help. To prove a property by induction, we define
an invariant and prove it by instantiating an induction schema. Here is
an example of such a schema, that works for the non-negative integers:

```
axiom [ind[u]] {
relation p(X:u)
{
individual x:u
property x <= 0 -> p(x)
}
{
individual x:u
property p(x) -> p(x+1)
}
#--------------------------
property p(X)
}
```

Like the recursion schema `rec[u]`

, the induction schema `ind[u]`

is
part of the integer theory, and becomes available when we interpret
type `u`

as `int`

.

Suppose we want to prove that `sum(Y)`

is always greater than or equal
to *Y*, that is:

```
property sum(Y) >= Y
```

We can prove this by applying our induction schema:

```
proof
apply ind[u] with X = Y;
assume sum with X = x;
defergoal;
assume sum with X = x + 1
```

Applying `ind[u]`

produces two sub-goals, a base case and an induction step:

```
# property x <= 0 -> sum(x) <= x
# property sum(x) <= x -> sum(x+1) <= x + 1
```

The `auto`

tactic can’t prove these goals because the definition of
`sum`

is a schema that must explicitly instantiated. Fortunately, it
suffices to instantiate this schema just for the specific arguments
of `sum`

in our subgoals. For the base case, we need to instantiate
the definition for `X`

, while for the induction step, we need
`X+1`

. Notice that we referred to the definiton of `sum`

by the name
`sum`

. Alternatively, we can name the definition itself and refer
to it by this name.

After instantiating the definition of `sum`

, our two subgoals look like this:

```
# theorem [prop5] {
# property [def2] sum(Y + 1) = (0 if Y + 1 <= 0 else Y + 1 + sum(Y + 1 - 1))
# property sum(Y) >= Y -> sum(Y + 1) >= Y + 1
# }
# theorem [prop4] {
# property [def2] sum(Y) = (0 if Y <= 0 else Y + sum(Y - 1))
# property Y:u <= 0 -> sum(Y) >= Y
# }
```

Because these goals are quantifier-free the `auto`

tactic can easily
handle them, so our proof is complete.

# Naming

If we can prove that something exists, we can give it a name. For
example, suppose that we can prove that, for every *X*, there exists a
*Y* such that `succ(X,Y)`

. Then there exists a function that, given an
*X*, produces such a *Y*. We can define such a function called `next`

in the following way:

```
relation succ(X:t,Y:t)
axiom exists Y. succ(X,Y)
property exists Y. succ(X,Y) named next(X)
```

Provided we can prove the property, and that `next`

is fresh, we can
infer that, for all *X*, `succ(X,next(X))`

holds. Defining a function
in this way, (that is, as a Skolem function) can be quite useful in
constructing a proof. However, since proofs in Ivy are not generally
constructive, we have no way to *compute* the function `next`

, so we
can’t use it in extracted code.

## Hierarchical proof development

As the proof context gets larger, it becomes increasingly difficult
for the automated prover to handle all of the judgements we have
admitted. This is especially true as combining facts or theories may
take us outside the automated prover’s decidable fragment. For this
reason, we need some way to break the proof into manageable parts.
For this purpose, IVy provides a mechanism to structure the proof into
a collection of localized proofs called *isolates*.

# Isolates

An isolate is a restricted proof context. An isolate can make parts of its proof context available to other isolates and keep other parts hidden. Moreover, isolates can contain isolates, allowing us to structure a proof development hierarchically.

Suppose, for example, that we want to define a function *f*, but keep
the exact definition hidden, exposing only certain properties of the
function. We could write something like this:

```
isolate t_theory = {
implementation {
interpret t -> int
definition f(X) = X + 1
}
theorem [expanding] {
property f(X) > X
}
property [transitivity] X:t < Y & Y < Z -> X < Z
}
```

Any names declared within the isolate belong to its namespace. For
example, the names of the two properties above are
`t_theory.expanding`

and `t_theory.transitivity`

.

The isolate contains four declarations. The first, says the type `t`

is to be interpreted as the integers. This instantiates the theory
of the integers for type `t`

, giving the usual meaning to operators
like `+`

and `<`

. The second defines *f* to be the integer successor
function. These two declarations are contained an *implementation*
section. This means that the `auto`

tactic will use them only within
the isolate and not outside.

The remaining two statements are properties about *t* and *f* to
be proved. These properties are proved using only the context of the
isolate, without any judgments admitted outside.

Now suppose we want to prove an extra property using `t_theory`

:

```
isolate extra = {
theorem [prop] {
property Y < Z -> Y < f(Z)
}
proof
assume t_theory.expanding with X = Z
}
with t_theory
```

The ‘with’ clause says that the properties in `t_theory`

should be
used by the `auto`

tactic within the isolate. In this case, the `transitivy`

property will be used by default. This pattern is particularly useful when
we have a collection of properties of an abstract datatype that we wish to
use widely without explicitly instantiating them.

Notice that `auto`

will not use the interpretation of *t* as the
integers and the definiton of *f* as the successor function, since
these are in the implementation section of isolate `t_theory`

and are therefore
hidden from other isolates. Similarly, theorem `expanding`

is not used by default
because it is a schema. This is as intended, since including any of these facts would
put the verification condition outside the decidable fragment.

We used two typical techniques here to keep the verification
conditions decidable. First, we hid the integer theory and the
definition of *f* inside an isolate, replacing them with some
abstract properties. Second, we eliminated a potential cycle in the
function graph by instantiating the quantifier implicit in theorem
`expanding`

, resulting in a stratified proof goal.

# Hierarchies of isolates

An isolate can in turn contain isolates. This allows us to structure a proof hierarchically. For example, the above proof could have been structured like this:

```
isolate extra2 = {
function f(X:t) : t
isolate t_theory = {
implementation {
interpret t -> int
definition f(X) = X + 1
}
theorem [expanding] {
property f(X) > X
}
property [transitivity] X:t < Y & Y < Z -> X < Z
}
theorem [prop] {
property Y < Z -> Y < f(Z)
}
proof
assume t_theory.expanding with X = Z
}
```

The parent isolate `extra2`

uses only the visible parts of the child isolate `t_theory`

.

# Proof ordering and refinement

Thus far, proof developments have been presented in order. That is, judgements occur in the file in the order in which they are admitted to the proof context.

In practice, this strict ordering can be inconvenient. For example,
from the point of view of clear presentation, it may often be better
to state a theorem, and *then* develop a sequence of auxiliary
definitions and lemmas needed to prove it. Moreover, when developing
an isolate, we would like to first state the visible judgments, then
give the hidden implementation.

To achieve this, we can use a *specification* section. The
declarations in this section are admitted logically *after* the other
declarations in the isolate.

As an example, we can rewrite the above proof development so that the visible properties of the isolates occur textually at the beginning:

```
isolate extra3 = {
function f(X:t) : t
specification {
theorem [prop] {
property Y < Z -> Y < f(Z)
}
proof
assume t_theory.expanding with X = Z
}
isolate t_theory = {
specification {
theorem [expanding] {
property f(X) > X
}
property [transitivity] X:t < Y & Y < Z -> X < Z
}
implementation {
interpret t -> int
definition f(X) = X + 1
}
}
}
```