From 9971a4fa58bcd4f08343313543d02b198261a0af Mon Sep 17 00:00:00 2001
From: Sandro Stucki <sandro.stucki@gmail.com>
Date: Wed, 19 Aug 2015 09:18:44 +0200
Subject: [PATCH] Adds documentation about theorem proving in Leon and the
proof DSL.
---
doc/purescala.rst | 1 +
doc/verification.rst | 1022 +++++++++++++++++++++++++++++++++++++++++-
2 files changed, 1010 insertions(+), 13 deletions(-)
diff --git a/doc/purescala.rst b/doc/purescala.rst
index 5610bcea7..450abf271 100644
--- a/doc/purescala.rst
+++ b/doc/purescala.rst
@@ -34,6 +34,7 @@ Pure Scala supports two kinds of top-level declarations:
case class Identifier(id: BigInt)
}
+.. _adts:
Algebraic Data Types
--------------------
diff --git a/doc/verification.rst b/doc/verification.rst
index 8778e31d8..e98758d8c 100644
--- a/doc/verification.rst
+++ b/doc/verification.rst
@@ -56,10 +56,10 @@ the following for any number of parameters):
body
} ensuring(r => post)
-where, :math:`\mbox{prec}(x)` is a boolean expression with free variables
-contained in :math:`\{ x \}`, :math:`\mbox{body}(x)` is a boolean expression with
+where, :math:`\mbox{prec}(x)` is a Boolean expression with free variables
+contained in :math:`\{ x \}`, :math:`\mbox{body}(x)` is a Boolean expression with
free variables contained in :math:`\{ x \}` and :math:`\mbox{post}(x, r)` is a
-boolean expression with free variables contained in :math:`\{ x, r \}`. The
+Boolean expression with free variables contained in :math:`\{ x, r \}`. The
types of :math:`x` and :math:`r` are respectively ``A`` and ``B``. We write
:math:`\mbox{expr}(a)` to mean the substitution in :math:`\mbox{expr}` of its
free variable by :math:`a`.
@@ -111,14 +111,14 @@ not checked as part of verifying the function. Given the following definition:
require(prec)
body
}
-
+
For each call site in the whole program (including in ``f`` itself):
.. code-block:: scala
...
- f(e)
+ f(e)
...
where the expression :math:`\mbox{e}(x)` is an expression of type ``A`` with
@@ -130,8 +130,8 @@ when the call site is inside an if expression:
.. code-block:: scala
if(x > 0)
- f(x)
-
+ f(x)
+
The path condition on :math:`x` would include the fact that :math:`x > 0`. This
path condition is then used as a precondition of proving the validity of the
call to :math:`\mbox{f}`. Formally, for each such call site, Leon will attempt
@@ -145,7 +145,7 @@ Leon will generates one such theorem for each static call site of a function wit
a precondition.
.. note::
-
+
Leon only assumes an open program model, where any function could be called from
outside of the given program. In particular, Leon will not derive a precondition
to a function based on known information in the context of the calls, such as
@@ -166,11 +166,11 @@ following program:
(while(cond) {
body
}) invariant(inv)
-
-where the boolean expression :math:`\mbox{cond}(x)` is over the free variable
+
+where the Boolean expression :math:`\mbox{cond}(x)` is over the free variable
:math:`x` and the expression :math:`\mbox{body}(x, x')` relates the value of
:math:`x` when entering the loop to its updated value :math:`x'` on loop exit.
-The expression :math:`\mbox{inv}(x)` is a boolean formula over the free
+The expression :math:`\mbox{inv}(x)` is a Boolean formula over the free
variable :math:`x`.
A loop invariant must hold:
@@ -223,7 +223,1003 @@ As we have seen, verifying the contract of a function is really proving a mathem
theorem. In some sense, Leon can be seen as a (mostly) automated theorem prover. It is
automated in the sense that once the property stated, Leon will proceed with searching
for a proof without any user interaction. In practice however, many theorems will be fairly
-difficult to prove, and it is possible for the user to provide hints to Leon.
-
+difficult to prove, and it is possible for the user to provide hints to Leon.
+
Hints typically take the form of simpler properties that combine in order to prove
more complicated ones.
+
+Neon
+====
+
+.. TODO decide how previous § & what follows should be integrated together (or
+ not)
+
+A practical introduction to proofs
+----------------------------------
+
+When writing logical propositions such as preconditions or
+postconditions in Leon, one is basically writing Boolean
+predicates. They can be as simple as testing whether a list is empty
+or not, to more complex combinations of properties. Lemmas or
+theorems are simply logical tautologies, that is, propositions that
+always hold. They can be expressed using Boolean-valued methods that
+return ``true`` for all their inputs.
+
+To make this more concrete, let's take a simple lemma as an
+example [#example-dir]_. Here we want to prove that the append operation (``++``) on
+lists preserves the content of the two lists being concatenated. This
+proposition is relatively straightforward and Leon is able to verify
+that it always holds.
+
+.. code-block:: scala
+
+ import leon.collection._ // for List
+ import leon.lang._ // for holds
+
+ object Example {
+ def appendContent[A](l1: List[A], l2: List[A]): Boolean = {
+ l1.content ++ l2.content == (l1 ++ l2).content
+ }.holds
+ }
+
+Here we wrote ``.holds`` which is a method implicitly available on ``Boolean``
+that ensure the returned value is ``true``. It is equivalent to writing
+``ensuring { res => res }``.
+
+Now let's look at another example that looks trivial but for which Leon
+actually needs some help with the proof: we want to prove that adding ``Nil``
+at the end of a list has no effect.
+
+.. code-block:: scala
+
+ import leon.collection._ // for List
+ import leon.lang._ // for holds
+
+ object Example {
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ l1 ++ Nil() == l1
+ }.holds
+ }
+
+If you try to verify this last example you'll face a delicate
+situation: Leon runs indeterminately until it is either killed or
+times out. But why does this happen? The proposition doesn't seems
+more complicated than ``appendContent``. Perhaps even more
+surprisingly, Leon *is* able to verify the following:
+
+.. code-block:: scala
+
+ def leftUnitAppend[T](l1: List[T]): Boolean = {
+ Nil() ++ l1 == l1
+ }.holds
+
+How is this possible? The two propositions are completely symmetric!
+The problem is that Leon doesn't know anything about lists, a priori.
+It can only reason about lists thanks to their definition in terms of
+the case classes ``Cons`` and ``Nil`` and associated methods such as
+``++``. In particular, Leon doesn't know that ``Nil`` represents the
+empty list, and hence that appending it to some other list is a no-op.
+What then, is the difference between the two examples above? To
+answer this question, we need to have a look at the definition of the
+``++`` method:
+
+.. code-block:: scala
+
+ def ++(that: List[T]): List[T] = (this match {
+ case Nil() => that
+ case Cons(x, xs) => Cons(x, xs ++ that)
+ }) ensuring { res => /* ... */ }
+
+Note that the implementation of ``++`` is recursive in its first
+argument ``this`` but *not* in its second argument ``that``. This is
+why Leon was able to verify ``leftUnitAppend`` easily: it is true *by
+definition*, i.e. ``Nil() ++ l1`` is actually defined to be ``l1``.
+What about the symmetric case? How is ``l1 ++ Nil()`` defined? Well,
+it depends on whether ``l1`` is the empty list or not. So in order to
+prove ``rightUnitAppend``, we need to proceed by case analysis. The
+resulting proof has a recursive (i.e. inductive) structure reminiscent
+of the definition of ``++``:
+
+.. code-block:: scala
+
+ import leon.collection._ // for List
+ import leon.lang._ // for holds
+ import leon.proof._ // for because
+
+ object Example {
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ (l1 ++ Nil() == l1) because {
+ l1 match {
+ case Nil() => true
+ case Cons(x, xs) => rightUnitAppend(xs)
+ }
+ }
+ }.holds
+ }
+
+With this new implementation of the ``rightUnitAppend`` lemma, Leon is capable
+of verifying that it holds. If you look closely at it, you can distinguish three
+parts:
+
+1. the claim we want to prove ``l1 ++ Nil() == l1``;
+2. ``because``, which is just some syntactic sugar for conjunction -- remember,
+ every proposition is a Boolean formula;
+3. and a recursion on ``l1`` that serves as a hint for Leon to perform
+ induction.
+
+The recursion is based here on pattern matching, which Leon will also check for
+exhaustiveness. It has essentially the same structure as
+the implementation of ``++``: the base case is when ``l1`` is the empty list
+and the inductive case is performed on ``Cons`` objects.
+
+
+Techniques for proving non-trivial propositions
+-----------------------------------------------
+
+In the previous section we saw that "proof hints" can improve the odds
+of Leon successfully verifying a given proposition. In this section
+we will have a closer look at what constitutes such a proof and
+discuss a few techniques for writing them.
+
+As mentioned earlier, propositions are represented by Boolean
+expressions in Leon. But how are proofs represented? They are just
+Boolean expressions as well [#props-not-types]_. The difference
+between propositions and proofs is not their representation, but how
+they are used by Leon. Intuitively, a proof ``p: Boolean`` for a
+proposition ``x: Boolean`` is an expression such that
+
+ 1. Leon is able to verify ``p``, and
+ 2. Leon is able to verify that ``p`` implies ``x``.
+
+This is what we mean when we say that proofs are "hints". Typically,
+a proof ``p`` of a proposition ``x`` is a more complex-looking but
+equivalent version of ``x``, i.e. an expression such that ``p == x``.
+This might seem a bit counter-intuitive: why should it be easier for
+Leon to verify an equivalent but more complex expression? The answer
+is that the more complex version may consist of sub-expressions that
+more closely resemble the definitions of functions used in ``x``. We
+have already seen an example of this principle in the previous
+section: let's have another look at the proof of ``rightUnitAppend``:
+
+.. code-block:: scala
+
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ val x = l1 ++ Nil() == l1
+ val p = l1 match {
+ case Nil() => true
+ case Cons(x, xs) => rightUnitAppend(xs)
+ }
+ x because p
+ }.holds
+
+Here, we have rewritten the example to make the distinction between
+the proposition ``x`` and its proof ``p`` more explicit. It's easy to
+check that indeed ``x == p``, and hence the overall result of
+``rightUnitAppend`` is equivalent to ``x`` (recall that ``because`` is
+just an alias of ``&&``, so ``(x because p) == (x && x) == x``).
+However, the proof term ``p`` closely resembles the definition of
+``++`` and its sub-expressions are easier to verify for Leon than
+``x`` itself. The only non-trivial expression is the recursive call
+to ``rightUnitAppend(xs)``, which serves as the inductive hypothesis.
+We will discuss induction in more detail in Section
+":ref:`induction`".
+
+
+Divide and Conquer
+******************
+
+Before we delve into the details of particular proof techniques, it is
+worth revisiting a guiding principle for writing proofs -- whether it
+be in Leon, by hand, or using some other form of mechanized proof
+checker -- namely to *modularize* proofs, i.e. to split the proofs of
+complex propositions into manageable *sub-goals*. This can be
+achieved in various ways.
+
+ * Use *helper lemmas* -- these are propositions that are lemmas on
+ their own, i.e. they state and prove simple but self-contained
+ propositions that can be reused elsewhere. As such, they play a
+ role akin to helper methods in normal programming, and indeed, are
+ implemented in the same way, except that they carry a ``.holds``
+ suffix.
+
+ * Use *case analysis* to split complex propositions into simpler
+ sub-cases. This is especially helpful in the presence of
+ recursion, where it leads to inductive proofs (see Section
+ ":ref:`induction`").
+
+ * Use *relational reasoning* to split complex relationships into
+ conjunctions of elementary ones. This often requires one to make
+ use of relational properties such as transitivity (e.g. to break a
+ single equation ``a == b`` into a chain of equations ``a == x1 &&
+ x1 == x2 && ... && xN == b``), symmetry (e.g. to use a previously
+ proven inequality ``a <= b`` where ``b >= a`` is expected),
+ anti-symmetry (to unify variables), and so on (see Section
+ ":ref:`rel-reasoning`").
+
+ * Separate specification form implementation. It is sometimes easier
+ to prove the fact that a given function fulfills its specification
+ as a separate lemma (although the proof techniques are roughly the
+ same, see Section ":ref:`post-cond`").
+
+ * Generalize (or specialize) propositions. Sometimes, propositions
+ are more easily proved in a stronger (or weaker) form and
+ subsequently instantiated (or combined with other propositions) to
+ yield a proof of the original proposition.
+
+While it is good practice to factor common propositions into helper
+lemmas, one sometimes wants to verify simple, specific sub-goals in a
+proof without going through the trouble of introducing an additional
+method. This is especially true while one is exploring the branches
+of a case analysis or wants to quickly check whether Leon is able to
+prove a seemingly trivial statement automatically (we will see
+examples of such situations in the coming sections). For such cases,
+one can use the ``check`` function from ``leon.proof``. The ``check``
+function behaves as the identity function on Booleans but additionally
+assumes its argument in its precondition. As a result, Leon will
+check that ``x`` holds while verifying the call to ``check(x)``.
+For example, when verifying the following function:
+
+.. code-block:: scala
+
+ import leon.proof.check
+
+ def foo(x: BigInt): Boolean = {
+ check(x >= 0 || x < 0) && check(x + 0 == 0)
+ }
+
+Leon will check (separately) that ``x >= 0 || x < 0`` and ``x + 0 ==
+0`` hold for all ``x``, even though the function ``foo`` does not
+specify any pre or postconditions, and report a counter example for
+the second case::
+
+ [ Info ] - Now considering 'precond. (call check(x >= 0 || x < 0))' VC for foo @40:5...
+ [ Info ] => VALID
+ [ Info ] - Now considering 'precond. (call check(x + 0 == 0))' VC for foo @40:31...
+ [ Error ] => INVALID
+ [ Error ] Found counter-example:
+ [ Error ] x -> 1
+
+This is especially helpful when "debugging" proofs.
+
+
+.. _induction:
+
+Induction
+*********
+
+The vast majority of functional programs are written as functions over
+:ref:`adts` (ADTs), and consequently, Leon comes with some special
+support for verifying properties of ADTs. Among other things, Leon
+provides an annotation ``@induct``, which can be used to automatically
+prove postconditions of recursive functions defined on ADTs by way of
+*structural induction*. We have already seen an example of such an
+inductive property, namely ``rightUnitAppend``. In fact, using
+``@induct``, Leon is able to prove ``rightUnitAppend`` directly:
+
+.. code-block:: scala
+
+ import leon.annotation._ // for @induct
+
+ @induct
+ def rightUnitAppend[T](l1: List[T]): Boolean = {
+ l1 ++ Nil() == l1
+ }.holds
+
+This is possible because the inductive step follows (more or less)
+directly from the inductive hypothesis and Leon can verify the base
+case automatically. However, Leon may fail to verify more complex
+functions with non-trivial base cases or inductive steps. In such
+cases, one may still try to provide proof hints by performing *manual
+case analysis*. Consider the following lemma about list reversal:
+
+.. code-block:: scala
+
+ import leon.collection._ // for List
+ import leon.lang._ // for holds
+
+ object Example {
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l
+ }.holds
+ }
+
+Leon is unable to verify ``reverseReverse`` even using ``@induct``.
+So let's try and prove the lemma using manual case analysis. We start
+by adding an "unrolled" version of the proposition and inserting calls
+to ``check`` in each branch of the resulting pattern match:
+
+.. code-block:: scala
+
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => check { Nil[T]().reverse.reverse == Nil[T]() }
+ case Cons(x, xs) => check { (x :: xs).reverse.reverse == (x :: xs) }
+ }
+ }
+ }.holds
+
+Clearly, the two versions of the lemma are equivalent: all we did was
+expand the proposition using a pattern match and add some calls to
+``check`` (remember ``check`` acts as the identity function on its
+argument). Let's see what output Leon produces for the expanded
+version::
+
+ [ Info ] - Now considering 'postcondition' VC for reverseReverse @615:5...
+ [Warning ] => UNKNOWN
+ [ Info ] - Now considering 'precond. (call check(List[T]().reverse().reverse() ...)' VC for reverseReverse @617:28...
+ [ Info ] => VALID
+ [ Info ] - Now considering 'precond. (call check({val x$27 = l.h; ...)' VC for reverseReverse @618:28...
+ [Warning ] => UNKNOWN
+ [ Info ] - Now considering 'match exhaustiveness' VC for reverseReverse @616:7...
+ [ Info ] => VALID
+
+As expected, Leon failed to verify the expanded version. However, we
+get some additional information due to the extra pattern match and the
+calls to ``check``. In particular, Leon tells us that the match is
+exhaustive, which means we covered all the cases in our case analysis
+-- that's certainly a good start. Leon was also able to automatically
+verify the base case, so we can either leave the call to ``check`` as
+is, or replace it by ``trivial``. Unfortunately, Leon wasn't able to
+verify the inductive step, something is missing. Let's try to
+manually reduce the inductive case and see where we get.
+
+.. code-block:: scala
+
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => trivial
+ case Cons(x, xs) => check { (xs.reverse :+ x).reverse == (x :: xs) }
+ }
+ }
+ }.holds
+
+And now we're stuck. We can't apply the inductive hypothesis here,
+nor can we reduce the inductive case further, unless we perform
+case analysis on ``xs``, which would grow the term further without
+changing its shape. To make any headway, we need to use an additional
+property of ``reverse``, given by the following lemma (which Leon *is*
+able to prove using ``@induct``):
+
+.. code-block:: scala
+
+ @induct
+ def snocReverse[T](l: List[T], t: T): Boolean = {
+ (l :+ t).reverse == t :: l.reverse
+ }.holds
+
+The lemma states that appending an element ``t`` to a list ``l`` and
+reversing it is equivalent to first reversing ``l`` and then
+prepending ``t``. Using this lemma, we can write the proof of
+``reverseReverse`` as
+
+.. code-block:: scala
+
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => trivial
+ case Cons(x, xs) => check {
+ (xs.reverse :+ x).reverse == x :: xs.reverse.reverse &&
+ x :: xs.reverse.reverse == (x :: xs) because
+ snocReverse(xs.reverse, x) && reverseReverse(xs)
+ }
+ }
+ }
+ }.holds
+
+Leon is able to verify this version of the lemma. Note that Leon
+doesn't actually require us to include the two equations as they are
+equivalent to the applications ``snocReverse(xs.reverse, x)`` and
+``reverseReverse(xs)``. Similarly, the call to ``check`` is somewhat
+redundant now that Leon is able to verify the entire proof. We could
+thus "simplify" the above to
+
+.. code-block:: scala
+
+ def reverseReverse[T](l: List[T]): Boolean = {
+ l.reverse.reverse == l because {
+ l match {
+ case Nil() => trivial
+ case Cons(x, xs) => snocReverse(xs.reverse, x) && reverseReverse(xs)
+ }
+ }
+ }.holds
+
+However, the previous version is arguably more readable for a human
+being, and therefore preferable. In Section ":ref:`rel-reasoning`" we
+will see how readability can be improved even further through the use
+of a DSL for equational reasoning.
+
+So far, we have only considered structurally inductive proofs.
+However, Leon is also able to verify proofs using *natural induction*
+-- the form of induction that is perhaps more familiar to most
+readers. Consider the following definition of the exponential
+function :math:`exp(x, y) = x^y` over integers:
+
+.. code-block:: scala
+
+ def exp(x: BigInt, y: BigInt): BigInt = {
+ require(y >= 0)
+ if (x == 0) 0
+ else if (y == 0) 1
+ else x * exp(x, y - 1)
+ }
+
+The function ``exp`` is again defined recursively, but this time using
+``if`` statements rather than pattern matching. Let's try and prove
+some properties of this function using natural induction. One such
+property is that for any pair of positive numbers :math:`x, y \geq 0`,
+the exponential :math:`x^y` is again a positive number.
+
+.. code-block:: scala
+
+ def positive(x: BigInt, y: BigInt): Boolean = {
+ require(y >= 0 && x >= 0)
+ exp(x, y) >= 0
+ }
+
+Since Leon doesn't know anything about exponentials, it isn't able to
+verify the lemma without hints. As with the previous example, we
+start writing our inductive proof by expanding the top-level ``if``
+statement in the definition of ``exp``.
+
+.. code-block:: scala
+
+ def positive(x: BigInt, y: BigInt): Boolean = {
+ require(y >= 0 && x >= 0)
+ exp(x, y) >= 0 because {
+ if (x == 0) check { exp(x, y) >= 0 } // <-- valid
+ else if (y == 0) check { exp(x, y) >= 0 } // <-- valid
+ else check { exp(x, y) >= 0 } // <-- unknown
+ }
+ }.holds
+
+Leon was able to verify the first two (base) cases, but not the
+inductive step, so let's continue unfolding ``exp`` for that case.
+
+.. code-block:: scala
+
+ def positive(x: BigInt, y: BigInt): Boolean = {
+ require(y >= 0 && x >= 0)
+ exp(x, y) >= 0 because {
+ if (x == 0) trivial
+ else if (y == 0) trivial
+ else check { x * exp(x, y - 1) >= 0 }
+ }
+ }.holds
+
+Although Leon still isn't able to verify the lemma, we now see a way
+to prove the inductive step: ``x`` is positive (by the second
+precondition) and so is ``exp(x, y - 1)`` (by the inductive
+hypothesis). Hence the product ``x * exp(x, y - 1)`` is again
+positive.
+
+.. code-block:: scala
+
+ def positive(x: BigInt, y: BigInt): Boolean = {
+ require(y >= 0 && x >= 0)
+ exp(x, y) >= 0 because {
+ if (x == 0) trivial
+ else if (y == 0) trivial
+ else check {
+ x >= 0 && exp(x, y - 1) >= 0 because positive(x, y - 1)
+ }
+ }
+ }.holds
+
+With these hints, Leon is able to verify the proof. Again, we could
+shorten the proof by omitting inequalities that Leon can infer
+directly, albeit at the expense of readability.
+
+.. code-block:: scala
+
+ def positiveShort(x: BigInt, y: BigInt): Boolean = {
+ require(y >= 0 && x > 0)
+ exp(x, y) >= 0 because {
+ if (x == 0) trivial
+ else if (y == 0) trivial
+ else positiveShort(x, y - 1)
+ }
+ }.holds
+
+We conclude the section with the inductive proof of another, somewhat
+more interesting property of the exponential function, namely that
+:math:`(x y)^z = x^z y^z`.
+
+.. code-block:: scala
+
+ def expMultCommute(x: BigInt, y: BigInt, z: BigInt): Boolean = {
+ require(z >= 0)
+ exp(x * y, z) == exp(x, z) * exp(y, z) because {
+ if (x == 0) trivial
+ else if (y == 0) trivial
+ else if (z == 0) trivial
+ else check {
+ x * y * exp(x * y, z - 1) ==
+ x * exp(x, z - 1) * y * exp(y, z - 1) because
+ expMultCommute(x, y, z - 1)
+ }
+ }
+ }.holds
+
+.. _rel-reasoning:
+
+Relational reasoning
+********************
+
+The majority of the example propositions we have seen so far related
+some expression (e.g. ``l.reverse ++ Nil()`` or ``exp(x, y)``) to some
+other expression (e.g. ``... == l1`` or ``... >= 0``). This is
+certainly a common case among the sorts of propositions about
+functions and data structures one might wish to prove. The proofs of
+such propositions typically involve some form of *relational
+reasoning*, i.e. reasoning involving properties (such as transitivity,
+reflexivity or symmetry) of the relations in question. Leon knows
+about these properties for built-in relations such as ``==`` or orders
+on numbers. For user-defined relations, they first need to be
+established as lemmas. In this section, we discuss how to make
+effective use of built-in relations, but the general principles extend
+to their user-defined counterparts.
+
+When working with simple structural equality, we can rely on the default ``==``
+operator and Leon will happily understand when the reflexivity, symmetry and
+transitivity properties apply and use them to conclude bigger proofs. Similarly,
+when working on ``BigInt``, Leon knows about reflexivity, antisymmetry and
+transitivity over ``>=`` or ``<=``, and also antireflexivity, antisymmetry
+and transitivity of ``>`` and ``<``.
+
+However, even for relatively simple proofs about ADTs, Leon needs
+hints when combining, say equality, with user-defined operations, such
+as ``++`` or ``reverse`` on lists. For example, Leon is not able to
+verify that the following holds for arbitrary pairs of lists ``l1``
+and ``l2``:
+
+.. code-block:: scala
+
+ (l1 ++ l2).reverse == l2.reverse ++ l1.reverse
+
+The hard part of giving hints to Leon is often to find them in the
+first place. Here we can apply a general principle on top of
+structural induction (as discussed in the previous section): we start
+from the left-hand side of an equation and build a chain of
+intermediate equations to the right-hand side. Using ``check``
+statements we can identify where Leon times out and hence potentially
+needs hints.
+
+.. code-block:: scala
+
+ def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
+ ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
+ l1 match {
+ case Nil() =>
+ /* 1 */ check { (Nil() ++ l2).reverse == l2.reverse } &&
+ /* 2 */ check { l2.reverse == l2.reverse ++ Nil() } &&
+ /* 3 */ check { l2.reverse ++ Nil() == l2.reverse ++ Nil().reverse }
+ case Cons(x, xs) =>
+ /* 4 */ check { ((x :: xs) ++ l2).reverse == (x :: (xs ++ l2)).reverse } &&
+ /* 5 */ check { (x :: (xs ++ l2)).reverse == (xs ++ l2).reverse :+ x } &&
+ /* 6 */ check { (xs ++ l2).reverse :+ x == (l2.reverse ++ xs.reverse) :+ x } &&
+ /* 7 */ check { (l2.reverse ++ xs.reverse) :+ x == l2.reverse ++ (xs.reverse :+ x) } &&
+ /* 8 */ check { l2.reverse ++ (xs.reverse :+ x) == l2.reverse ++ (x :: xs).reverse }
+ }
+ }
+ }.holds
+
+If we run the above code with a decent timeout, Leon reports four
+*UNKNOWN* cases: the postcondition of the ``reverseAppend`` function itself and
+checks number 2, 6 and 7.
+
+ * Check #2 fails because, as we saw earlier, Leon is not capable of
+ guessing the ``rightUnitAppend`` lemma by itself. We fix this case
+ by simply instantiating the lemma, i.e. by appending ``&&
+ rightUnitAppend(l2.reverse)`` to the base case.
+
+ * Check #6 fails because, at this point, we need to inject the
+ induction hypothesis on ``xs`` and ``l2`` by adding ``&&
+ reverseAppend(xs, l2)``.
+
+ * Finally, check #7 fails for a similar reason as check #2: we need
+ an additional "associativity" lemma to prove that ``(l1 ++ l2) :+ t
+ == l1 ++ (l2 :+ t)`` holds for any ``l1``, ``l2`` and ``t``. We
+ call this lemma ``snocAfterAppend`` and leave it as an exercise for
+ the reader.
+
+Once we have a valid proof, we can try to optimize it for readability.
+As it stands, the resulting code is rather verbose because both sides
+of most equations are duplicated. One option is to completely remove
+the equations (they are implied by the instantiations of the lemmas)
+and simply write
+
+.. code-block:: scala
+
+ def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
+ ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
+ l1 match {
+ case Nil() =>
+ rightUnitAppend(l2.reverse)
+ case Cons(x, xs) =>
+ reverseAppend(xs, l2) && snocAfterAppend(l2.reverse, xs.reverse, x)
+ }
+ }
+ }.holds
+
+Or we can employ the equational reasoning DSL provided by the
+``leon.proofs`` package to remove the duplicate expressions and
+interleave the equations with their associated proofs. This has the
+advantage of not losing information that is still useful for a human
+being reading the proof later on:
+
+.. code-block:: scala
+
+ def reverseAppend[T](l1: List[T], l2: List[T]): Boolean = {
+ ( (l1 ++ l2).reverse == l2.reverse ++ l1.reverse ) because {
+ l1 match {
+ case Nil() => {
+ (Nil() ++ l2).reverse ==| trivial |
+ l2.reverse ==| rightUnitAppend(l2.reverse) |
+ l2.reverse ++ Nil() ==| trivial |
+ l2.reverse ++ Nil().reverse
+ }.qed
+ case Cons(x, xs) => {
+ ((x :: xs) ++ l2).reverse ==| trivial |
+ (x :: (xs ++ l2)).reverse ==| trivial |
+ (xs ++ l2).reverse :+ x ==| reverseAppend(xs, l2) |
+ (l2.reverse ++ xs.reverse) :+ x ==|
+ snocAfterAppend(l2.reverse, xs.reverse, x) |
+ l2.reverse ++ (xs.reverse :+ x) ==| trivial |
+ l2.reverse ++ (x :: xs).reverse
+ }.qed
+ }
+ }
+ }.holds
+
+The idea is to group statements in a block
+(``{ }``) and call ``qed`` on it. Then, instead of writing ``a == b && b == c
+&& hint1 && hint2`` we write ``a ==| hint1 | b ==| hint2 | c``. And when no
+additional hint is required, we can use ``trivial`` which simply stands for
+``true``.
+
+Additionally, by using this DSL, we get the same feedback granularity from Leon
+as if we had used ``check`` statements. This way we can construct proofs based
+on equality more easily and directly identify where hints are vital.
+
+One shortcoming of the relational reasoning DSL is that it relies on
+Leon's knowledge of the relational properties of the built-in
+relations, and in particular those of equality. Consequently is works
+badly (if at all) with user-defined relations. However, since the DSL
+is defined as a library (in ``library/proof/package.scala``), it can
+in principle be extended and modified to include specific user-defined
+relations on a case-by-case basis.
+
+.. TODO add a word about requirement in ctor (e.g. Rational)
+
+.. TODO Footnote linking to Etienne's answer on SO.
+
+
+Limits of the approach: HOFs, quantifiers and termination
+*********************************************************
+
+While the techniques discussed in this section are useful in general,
+their applicability has of course its limitations in practice. These
+limitations are mostly due to Leon's limited support for certain
+language constructs, such as higher-order functions (HOFs) or
+quantifiers (which in turn is due, mostly, to the limited support of
+the corresponding theories in the underlying SMT solvers).
+
+Still, even using these "experimental" features, one manages to prove
+some interesting propositions. Here is another list example, which
+relates the ``foldLeft``, ``foldRight`` and ``reverse`` operations
+defined on lists and makes crucial use of HOFs:
+
+.. code-block:: scala
+
+ import leon.collection._
+ import leon.lang._
+ import leon.proof._
+
+ def folds[A, B](xs: List[A], z: B, f: (B, A) => B): Boolean = {
+ val f2 = (x: A, z: B) => f(z, x)
+ xs.foldLeft(z)(f) == xs.reverse.foldRight(z)(f2) because {
+ xs match {
+ case Nil() => true
+ case Cons(x, xs) => {
+ (x :: xs).foldLeft(z)(f) ==| trivial |
+ xs.foldLeft(f(z, x))(f) ==| folds(xs, f(z, x), f) |
+ xs.reverse.foldRight(f(z, x))(f2) ==| trivial |
+ xs.reverse.foldRight(f2(x, z))(f2) ==|
+ snocFoldRight(xs.reverse, x, z, f2) |
+ (xs.reverse :+ x).foldRight(z)(f2) ==| trivial |
+ (x :: xs).reverse.foldRight(z)(f2)
+ }.qed
+ }
+ }
+ }.holds
+
+A rather different, more general issue that arises when proving
+propositions using Leon is related to *termination checking*. When
+verifying inductive proofs (and more generally the postconditions of
+recursive methods), Leon assumes that the corresponding proofs are
+*well-founded*, or equivalently, that the corresponding recursive
+methods terminate on all inputs. Yet Leon does not -- by default --
+check that this is the case. It is thus possible -- and indeed rather
+easy -- to write bogus proofs (intentionally or accidentally) which
+Leon recognizes as valid, but which are not well-founded. Consider
+the following lemma, which apparently establishes that all lists are
+empty:
+
+.. code-block:: scala
+
+ import leon.collection._
+ import leon.lang._
+ import leon.proof._
+
+ object NotWellFounded {
+
+ // This proof is not well-founded. Since Leon doesn't run the
+ // termination checker by default, it will accept the proof as
+ // valid.
+ def allListsAreEmpty[T](xs: List[T]): Boolean = {
+ xs.isEmpty because {
+ xs match {
+ case Nil() => trivial
+ case Cons(x, xs) => allListsAreEmpty(x :: xs)
+ }
+ }
+ }.holds
+ }
+
+Leon has (experimental) support for termination checking, which can be
+enabled using the ``--termination`` command line option to minimize
+the risk of accidentally writing bogus proofs such as the one above.
+
+.. TODO example: folds + future work (alt. version of folds)
+
+.. _post-cond:
+
+Techniques for proving non-trivial postconditions
+-------------------------------------------------
+
+When proving a mathematical lemma, the return type of the
+corresponding function is most of
+the time, if not always, ``Boolean``. For those proofs it is rather easy to
+write a postcondition: using ``holds`` is generally enough.
+
+But when it comes to writing postconditions for more general functions, such as
+the addition on rational numbers, we are no longer dealing with ``Boolean`` so
+we need a strategy to properly write ``ensuring`` statements.
+
+
+Rationals: a simple example
+***************************
+
+Let's take rational numbers as an example: we define them as a case class with
+two attributes, `n` for the numerator and `d` for the denominator. We also
+define three simple properties on them: ``isRational``, ``isNonZero`` and
+``isPositive``.
+
+.. code-block:: scala
+
+ case class Rational(n: BigInt, d: BigInt) {
+ def isRational = d != 0
+ def isPositive = isRational && (n * d >= 0)
+ def isNonZero = isRational && (n != 0)
+
+ // ...
+ }
+
+And on top of that we want to support addition on ``Rational`` in a way that
+the rationality and positiveness properties are correctly preserved:
+
+.. code-block:: scala
+
+ def +(that: Rational): Rational = {
+ require(isRational && that.isRational)
+ Rational(n * that.d + that.n * d, d * that.d)
+ } ensuring { res =>
+ res.isRational &&
+ (this.isPositive == that.isPositive ==> res.isPositive == this.isPositive)
+ }
+
+In this simple case, things work nicely and we can write the
+multiplication in a similar fashion:
+
+.. code-block:: scala
+
+ def *(that: Rational): Rational = {
+ require(isRational && that.isRational)
+ Rational(n * that.n, d * that.d)
+ } ensuring { res =>
+ res.isRational &&
+ (res.isNonZero == (this.isNonZero && that.isNonZero)) &&
+ (res.isPositive == (!res.isNonZero || this.isPositive == that.isPositive))
+ }
+
+
+Measures: a slightly more complex example
+*****************************************
+
+Now let's look at a slightly more complex example: measures on
+discrete probability spaces. We represent such measures using a
+``List``-like recursive data structure: a generic abstract class
+``Meas[A]`` that has two subclasses, ``Empty[A]`` and ``Cons[A]``.
+The constructor of the class ``Empty[A]`` takes no arguments; it
+represents an "empty" measure that evaluates to 0 when applied to any
+set of values of type ``A``. The constructor of ``Cons[A]``, on the
+other hand, takes three parameters: a value ``x``, its associated
+weight ``w`` expressed as a ``Rational`` (since Leon doesn't quite yet
+support real numbers out of the box), and another measure ``m`` on
+``A``. The value ``Cons(x, w, m)`` represents the measure obtained by
+adding to ``m`` the "single-point" measure that evaluates to ``w`` at
+``x`` and to 0 everywhere else. We also define an ``isMeasure``
+property -- similar to the ``isRational`` property presented above --
+which recursively checks that all the weights in a measure are
+positive rationals (note that all our measures have finite support).
+
+.. code-block:: scala
+
+ /** Measures on discrete probability spaces. */
+ sealed abstract class Meas[A] {
+
+ /** All weights must be positive. */
+ def isMeasure: Boolean = this match {
+ case Empty() => true
+ case Cons(x, w, m) => w.isPositive && m.isMeasure
+ }
+
+ // ...
+ }
+
+ /** The empty measure maps every subset of the space A to 0. */
+ case class Empty[A]() extends Meas[A]
+
+ /**
+ * The 'Cons' measure adjoins an additional element 'x' of type 'A'
+ * to an existing measure 'm' over 'A'. Note that 'x' might already
+ * be present in 'm'.
+ */
+ case class Cons[A](x: A, w: Rational, m: Meas[A]) extends Meas[A]
+
+
+The defining operation on a measure ``m`` is its evaluation ``m(xs)``
+(or equivalently ``m.apply(xs)``) on some set ``xs: Set[A]``, i.e. on a
+subset of the "space" ``A``. The value of ``m`` should be a positive
+rational for any such set ``xs``, provided ``m.isMeasure`` holds.
+This suggests ``_.isPositive`` as the postcondition for ``apply``,
+but simply claiming that the result is positive is not enough for Leon
+to verify this postcondition.
+
+We can provide the necessary hint to Leon by performing structural
+induction on ``this`` inside the postcondition as follows:
+
+.. code-block:: scala
+
+ /** Compute the value of this measure on a subset of the space 'A'. */
+ def apply(xs: Set[A]): Rational = {
+ require (isMeasure)
+ this match {
+ case Empty() => Rational(0, 1)
+ case Cons(x, w, m) => if (xs contains x) w + m(xs) else m(xs)
+ }
+ } ensuring { res =>
+ res.isPositive because {
+ this match {
+ case Empty() => trivial
+ case Cons(x, w, m) => m(xs).isPositive
+ }
+ }
+ }
+
+Notice the similarity between the pattern match in the body of the
+``apply`` function and that in the postcondition. With this hint,
+Leon is able to verify the postcondition.
+
+
+A complex example: additivity of measures
+-----------------------------------------
+
+Using the principles and techniques discussed so far, one can prove
+quite advanced propositions using Leon. Returning to the
+measure-theoretic example from the previous section, we would like to
+prove that our implementation of measures is properly *additive*.
+Formally, a measure :math:`\mu \colon A \to \mathbb{R}` on a countable
+set :math:`A` must fulfill the following additivity property
+[#dicrete-meas]_:
+
+.. math::
+
+ \forall A_1, A_2 \subseteq A . A_1 \cap A_2 = \emptyset \Rightarrow
+ \mu(A_1 \cup A_2) = \mu(A_1) + \mu(A_2)
+
+which we can express in Leon as
+
+.. code-block:: scala
+
+ def additivity[A](m: Meas[A], xs: Set[A], ys: Set[A]): Boolean = {
+ require(m.isMeasure && (xs & ys).isEmpty)
+ m(xs ++ ys) == m(xs) + m(ys)
+ }.holds
+
+We can prove this property using structural induction on the parameter
+``m``, case analysis on the parameters ``xs`` and ``ys``, equational
+reasoning, and properties of rational numbers (in the form of
+user-defined lemmas) as well as sets (using Leon's built-in support).
+
+.. code-block:: scala
+
+ def additivity[A](m: Meas[A], xs: Set[A], ys: Set[A]): Boolean = {
+ require(m.isMeasure && (xs & ys).isEmpty)
+ m(xs ++ ys) == m(xs) + m(ys) because {
+ m match {
+ case Empty() => trivial
+ case Cons(x, w, n) => if (xs contains x) {
+ w + n(xs ++ ys) ==| additivity(n, xs, ys) |
+ w + (n(xs) + n(ys)) ==| plusAssoc(w, n(xs), n(ys)) |
+ (w + n(xs)) + n(ys) ==| !(ys contains x) |
+ m(xs) + m(ys)
+ }.qed else if (ys contains x) {
+ w + n(xs ++ ys) ==| additivity(n, xs, ys) |
+ w + (n(xs) + n(ys)) ==| plusComm(w, (n(xs) + n(ys))) |
+ (n(xs) + n(ys)) + w ==| plusAssoc(n(xs), n(ys), w) |
+ n(xs) + (n(ys) + w) ==| plusComm(n(ys), w) |
+ n(xs) + (w + n(ys)) ==| !(xs contains x) |
+ m(xs) + m(ys)
+ }.qed else {
+ n(xs ++ ys) ==| additivity(n, xs, ys) |
+ n(xs) + n(ys)
+ }.qed
+ }
+ }
+ }.holds
+
+The full proof (including the proofs of all helper lemmas) as well as
+its generalization to *sub-additivity* can be found in the
+``testcases/verification/proof/measure/`` directory of the Leon
+distribution [#example-dir]_.
+
+
+Quick Recap
+-----------
+
+Let's summarize what we've learned here. To write proofs efficiently,
+it's good to keep the following in mind:
+
+1. Always use a proper timeout and ask Leon for more information about
+ what he tries to verify, e.g. ``--timeout=5 --debug=verification``.
+
+2. Use ``@induct`` when working on structurally inductive proofs to
+ get a more precise feedback from Leon: this will decompose the
+ proof into a base case and an inductive case for the first argument
+ of the function under consideration.
+
+ If Leon isn't able to verify the proof using ``@induct``, try
+ performing manual case analysis.
+
+3. Modularize your proofs and verify *sub-goals*!
+
+ - use plenty of helper lemmas;
+ - use ``check`` abundantly;
+ - if possible use the relational reasoning DSL presented above.
+
+ This is especially handy when you can connect the two sides of a relational
+ claim with sub-statements.
+
+
+.. rubric:: Footnotes
+
+.. [#example-dir] The source code of this example and all other in
+ this chapter are included in the Leon distribution. Examples about
+ lists can be found in ``library/collection/List.scala``, the other
+ examples are located in the ``testcases/verification/proof/``
+ directory.
+
+.. [#props-not-types] Perhaps surprisingly, propositions and proofs
+ live in the same universe in Leon. This is contrary to
+ e.g. type-theoretic proof assistants where propositions are
+ represented by types and proofs are terms inhabiting such types.
+
+.. [#dicrete-meas] To be precise, we are assuming here the underlying
+ measurable space :math:`(A, \mathcal{P}(A))`, where :math:`A` is
+ countable and :math:`\mathcal{P}(A)` denotes its discrete σ-algebra
+ (i.e. the power set of :math:`A`).
--
GitLab