Intuitive Proofs

Jean-Baptiste Tristan & K. Rustan M. Leino

Dafny: a proof assistant

In Dafny, you can state and prove mathematical propositions

  lemma Proposition()
    ensures forall m: int, n: int :: m > 0 && n > m ==> m + n > 0

A proposition and its proof are packaged as a lemma
- The proposition is a Boolean expression (functional expression + quantifiers)
- The proof script comes in curly braces following the lemma
If a lemma comes with a proof script, then the Dafny verifier checks that the proof is valid and establishes the proposition
We will now introduce the languages of proofs

Dafny: an auto-active proof assistant

Dafny builds on automated theorem proving
- You need not provide painfully detailed proof scripts

In many cases, Dafny can find a proof on its own

  lemma AutoActive()
    ensures forall m: int, n: int :: m + n == n + m
  {
  }

In this example, Dafny finds a complete proof on its own
Therefore, we know that the ensures clause is true
Dafny is somewhere in between an automated and an interactive theorem prover
- You can interact with the prover by writing a proof script
- You do not interactively build a proof tree

Writing proofs

What is a proof anyway?

A proof plays two roles.

(i) A proof convinces the reader that the statement is correct.
(ii) A proof explains why the statement is correct.

The first point consists of the administrative (‘bookkeeper’) activities of verifying the correctness of the small reasoning steps and see if they constitute a correct proof. One doesn’t have to look at the broad picture, but one just has to verify step by step whether every step is correct. The second point deals with giving the intuition of the theorem: Why is it so natural that this property holds? How did we come to the idea of proving it in this way?

— Herman Geuvers

Proofs that explain

Many of us have learned to write proofs in a course on Euclidean geometry
In this context, a proof is a succession of assertions and appeal to known lemmas
A proof is valid if it explains why the property holds
A proof is mostly unstructured
This approach relies primarily on intuition: no formal appeal to what constitutes a proof

Proving by explaining

The principal way by which you write proofs in Dafny is by explaining
You do so by asserting intuitive properties that guide Dafny

Consider the following exercise

  ghost predicate Even(n: nat)

  ghost predicate Odd(n: nat)

  lemma EvenP()
    ensures forall n: nat :: Even(n) == exists m: nat :: n == 2 * m

  lemma OddP()
    ensures forall n: nat :: Odd(n) == !Even(n)

  lemma SuccOddIsEven()
    ensures forall n: nat :: Odd(n) ==> Even(n + 1)

This is probably obvious to you, but not to Dafny
The reason it is not so obvious is because of the quantifiers

What does dafny know?

When you write a pencil-and-paper proof, you adapt to your audience
For example, you may not need to remind the reader that real addition is associative because that's part of the folklore knowledge
What is Dafny's folklore knowledge?
This question is hard to answer
- We will answer it partly in later lectures
- In practice, you form a mental model of what it can do by experience

Proof statements

A proof is a sequence of statements that guides the proof verification
Each statement affects what Dafny knows

Asserting and calling propositions

The most important proof statements are:
Assertions
- The assert keyword is followed by a proposition
- If the proposition is verified, then it is known for the rest of the proof
Reminders
- Call a lemma to remind Dafny about our axioms

  lemma SuccOddIsEven()
    ensures forall n: nat :: Odd(n) ==> Even(n + 1)
  {

    EvenP();
    OddP();

    assert forall n: nat :: n % 2 == 0 ==> n == 2 * (n / 2);
    assert forall n: nat :: n == 2 * (n / 2) ==> Even(n);
    assert forall n: nat :: Odd(n) ==> n % 2 == 1;
    assert forall n: nat :: n % 2 == 1 ==> (n + 1) % 2 == 0;

  }

Fixing arbitrary values

We would not write a proof like that on paper
Instead, we would work around all the quantification by considering a fixed but arbitrary value of n for the proof

  lemma SuccOddIsEven(n: nat)
    ensures Odd(n) ==> Even(n + 1)
  {

    EvenP();
    OddP();

    assert forall n: nat :: n % 2 == 0 ==> n == 2 * (n / 2);
    assert forall n: nat :: n == 2 * (n / 2) ==> Even(n);
    assert Odd(n) ==> n % 2 == 1;
    assert Odd(n) ==> (n + 1) % 2 == 0;

  }

Fixing assumptions

We would not write a proof like that on paper

Instead, we would work around all the implications by stating what assumptions we are making in the proof

  lemma SuccOddIsEven(n: nat)
    requires Odd(n)
    ensures Even(n + 1)
  {

    EvenP();
    OddP();
    
    assert forall n: nat :: n % 2 == 0 ==> n == 2 * (n / 2);
    assert forall n: nat :: n == 2 * (n / 2) ==> Even(n);
    assert n % 2 == 1;
    assert (n + 1) % 2 == 0;
  
  }

Structuring a proof in lemmas

We would not write a proof like that on paper

Instead, we would organize our proof by first defining a proving a lemma

  lemma DivBy2IsEven()
    ensures forall n: nat :: n % 2 == 0 ==> Even(n)
  {
    EvenP(); OddP();
    assert forall n: nat :: n % 2 == 0 ==> n == 2 * (n / 2);
  }

  lemma SuccOddIsEven(n: nat)
    requires Odd(n)
    ensures Even(n + 1)
  {
    OddP();
    DivBy2IsEven();
    
    assert n % 2 == 1;
    assert (n + 1) % 2 == 0;
  }

Reasoning incrementally

It is hard to come up with a proof at once

To make and validate incremental progress, one can assume a result

This should be proved later

  lemma Prop()
    ensures forall n: nat :: Even(n) ==> Even(n + 2)
  {
    assume false; // TODO
  }

Universal introduction

A forall statement proves a universal property by fixing an arbitary name

  lemma Prop()
    ensures forall n: nat :: Even(n) ==> Even(n + 2)
  {
    forall n: nat
      ensures Even(n) ==> Even(n + 2)
    {
      assume false; // TODO
    }
  }

Implication introduction

An if statement proves a conditional property by assuming a property

  lemma Prop()
    ensures forall n: nat :: Even(n) ==> Even(n + 2)
  {
    forall n: nat
      ensures Even(n) ==> Even(n + 2)
    {
      if Even(n) {
        assume false; // TODO
      }
    }
  }

Skolemization

A Skolemization fixes a witness for a known existential property

  lemma Prop()
    ensures forall n: nat :: Even(n) ==> Even(n + 2)
  {
    forall n: nat
      ensures Even(n) ==> Even(n + 2)
    {
      if Even(n) {
        var a: nat :| n == 2 * a;
        assume false; // TODO
      }
    }
  }

Providing a witness

A variable definition names an expression and creates a witness

  lemma Prop()
    ensures forall n: nat :: Even(n) ==> Even(n + 2)
  {
    forall n: nat
      ensures Even(n) ==> Even(n + 2)
    {
      if Even(n) {
        var a: nat :| n == 2 * a;
        var b: nat := 2 * (a + 1);
      }
    }
  }

Proof methods

Other important proof methods include
- Proof by contradiction
- Proof by case analysis
- Proof by induction

Proof by contradiction

Assume the contrary to your goal and prove false

  lemma ProofByContradiction(n: nat)
    requires Even(n)
    ensures !exists m: nat :: n == 2 * m + 1
  {

    var m1: nat :| n == 2 * m1;

    if exists m: nat :: n == 2 * m + 1 {

      var m2: nat :| n == 2 * m2 + 1;
      assert false;

    }

  }

Proof by case analysis

In math, we sometimes enumerate different possibilities

In Dafny, one way to do this uses conditional statements

  lemma ProofByCaseAnalysis(n: nat)
    ensures Even(n) || Odd(n)
  {

    if n % 2 == 0 { assert n == 2 * (n / 2); }

    if n % 2 == 1 { assert n == (2 * (n / 2)) + 1; }

  }

Proof by induction

To prove a property that holds for all natural numbers, you can sometimes do it by induction
If you can prove $$P(0)$$
And $\forall \; n \cdot P(n) \Rightarrow P(n+1)$
Then, you can conclude $\forall \; n \cdot P(n)$

Pencil and paper proof by induction

Lemma 1.
$\forall n \cdot \sum_{i=0}^n i = \frac{n(n+1)}{2}$

Proof.

Base case: $\sum_{i=0}^0 i = 0 = \frac{0 \times 1}{2}$
Inductive case:
- We assume that $\sum_{i=0}^n i = \frac{n(n+1)}{2}$
- Autopilot:
  - $\sum_{i=0}^{n+1} i$
    $= \sum_{i=0}^{n} i + (n + 1) \;\;\;\; \text{By definition}$
    $= \frac{n(n+1)}{2} + (n + 1) \;\;\;\; \text{By induction hypothesis}$
    $= \frac{(n+1)(n+2)}{2} \;\;\;\; \text{By algebra autopilot}$
Conclusion: $\forall n \cdot \sum_{i=0}^n i = \frac{n(n+1)}{2}$

Dafny proof by induction

In Dafny, a proof by induction amounts to a recursive call with a smaller argument

  lemma ProofByInduction(n: nat)
    requires n % 2 == 0
    ensures Even(n)
  {

    if n == 0 {

      assert n == 2 * 0;

    } else {

      assert (n - 2) % 2 == 0;
      ProofByInduction(n - 2);
      var m: nat :| n - 2 == 2 * m;
      assert n == 2 * m + 2;
      assert n == 2 * (m + 1);

    }
  }