Convincing and Explaining

In classes 9 and 10 we will explore how Dafny automatically constructs proofs of logical expressions — we’ll discuss negation, conjunction and disjunction, implication, and universal and existential quantification — and how we can structure our proofs to assist both Dafny and human readers.

What does Dafny know?

We have seen examples where Dafny “knows” potentially surprising facts without any outside explanation:

function TriangleNumber(n: nat): nat
{ if n == 0 then 0 else TriangleNumber(n - 1) + n }

lemma Gauss(n: nat)
  ensures TriangleNumber(n) == n * (n + 1) / 2
{ /* no further explanation required */ }

… and other examples where it seems to have potentially surprising blind spots?

lemma Hello?() {
  var hi := [ "👋" ];
  assert exists idx: nat :: idx < |hi| && hi[idx] == "👋";
}

Explaining all the built-in rules that Dafny can apply is not straightforward, and this list anyway is always subject to change and improvement. Instead: in the first part of this reading we establish a notation for proof rules, so that we can explain the steps of Dafny’s reasoning; and in the second part we step back and look at how to structure our proofs so that instead of thinking about low-level rules, we are first and foremost concerned with providing clear explanations.

Proof challenges

Suppose we write the following lemma about positive even numbers:

lemma ZeroMod2_Implies_Even(n: int)
  requires n > 0
  ensures (n % 2 == 0) ==>
    (exists m: int :: m > 0 && n == 2 * m)
{
}

What are we asking Dafny to prove? We would like the system to take a collection of assumed facts about the world of our program and derive a new fact. For lemma ZeroMod2_Implies_Even, the assumed facts are:

• there is some n of type int, and
• n > 0.

We can read those assumptions off from the lemma’s definition and precondition. The new fact we hope to derive given these hypotheses, our goal, is:

• n % 2 == 0 ==> exists m: int :: m > 0 && n == 2 * m.

Our notation for this proof challenge uses the turnstile symbol ⊢ which you should read as “proves:”

n: int, n > 0  ⊢  n % 2 == 0 ==> exists m: int :: m > 0 && n == 2 * m

On the left of the turnstile are our hypotheses, an unordered set of facts. On the right is our goal. And the question is: do the hypotheses prove the goal?

lemma ZeroMod2_Implies_Even(n: int)
  requires n > 0
  ensures (n % 2 == 0) ==> (exists m: int :: m > 0 && n == 2 * m)
{
  // if n % 2 == 0, then n equals...
  assert n % 2 == 0 ==> n == ???;
}

What is happening when we use assert in order to complete the proof? Let’s give some names to the propositions we have:

• P(n) is the precondition, n > 0.
• Q(n) is the postcondition, n % 2 == 0 ==> exists m: int :: m > 0 && n == 2 * m.
• R(n) is our asserted n % 2 == 0 ==> n == ... (see the exercise answer).

lemma ZeroMod2_Implies_Even(n: int)
  requires P(n)
  ensures Q(n)
{
  // the overall proof challenge:
  n: int, P(n) ⊢ Q(n)

  assert R(n) by {
    // set Q aside, are our hypotheses sufficient to prove R?
    n: int, P(n) ⊢ R(n)
  }

  // if so, the conclusion of the assert is now an
  //   assumption we can use to try and prove Q:
  n: int, P(n), R(n) ⊢ Q(n)
}

The challenge of assert

We can generalize this schematic to summarize the challenge of assert. Supposing any number of parameters x, y, etc. of arbitrary types T1, T2, etc.:

• how can we prove an assert?
• and then how can we use it?

lemma UsingAssert<T1, T2, ...>(x: T1, y: T2, ...)
  requires P(x, y, ...)
  ensures Q(x, y, ...)
{
  // overall proof challenge:
  T1, T2, x: T1, y: T2, ..., P(x, y, ...) ⊢ Q(x, y, ...)

  assert R(x, y, ...) by {
    // how do we prove an assert?
    T1, T2, x: T1, y: T2, ..., P(x, y, ...) ⊢ R(x, y, ...)
  }

  // and how do we use an assert?
  T1, T2, x: T1, y: T2, ..., P(x, y, ...), R(x, y, ...) ⊢ Q(x, y, ...)
}

Let’s look at some simpler cases. By convention, we use capital Greek letter gamma Γ on the left side of the turnstile to stand for “all of our hypotheses,” and then after the Γ we pick out particular hypotheses that are relevant to the challenge at hand.

lemma Intro<T1, T2, ...>(x: T1, y: T2, ...)
  requires P(x, y, ...)
  requires Q(...)
  ensures Q(...)
{
}

P && Q

Every logical operator has associated rules for:

1. proving a statement that has the operator, like the answer to (1) above, and

2. using a proved statement to prove something else, like the answer (and its companion) to (2).

We will discuss the rules for more operators in class 10, so that we can understand what proof challenges we are posing to Dafny and how it will try to meet them.

What about zero-mod-2 implies even?

We introduced the “proves” relation ⊢ so that we could formalize our goal of proving:

lemma ZeroMod2_Implies_Even(n: int)
  requires n > 0
  ensures n % 2 == 0  ==>  exists m: int :: m > 0 && n == 2 * m

… as:

n: int, n > 0  ⊢  n % 2 == 0 ==> exists m: int :: m > 0 && n == 2 * m

… which Dafny could not immediately prove. However, we saw in the first exercise above that Dafny is able to prove our assertion:

n: int, n > 0  ⊢  n % 2 == 0 ==> n == 2 * (n/2)

It succeeded because the automated proof system has built-in knowledge about integers and their operations. Following the rule for using an assert, our goal is now:

n: int, n > 0, n % 2 == 0 ==> n == 2 * (n/2)
  ⊢ n % 2 == 0 ==> exists m: int :: m > 0 && n == 2 * m

And this Dafny can prove. We will complete a proof of a similar lemma in class 10, where you will want to pay attention to:

• how we prove an implication ==> and then how we make use of that knowledge;
• how we prove an existential quantification and how we make use of it.

With those pieces in hand, you will be able to understand all the steps Dafny is taking.

But for the rest of this reading we step back from the low-level rules to the bigger picture of writing proofs that explain.

Organizing a proof

Knowing exactly the rules that Dafny uses to complete a proof is not the best way to come up with the proof, nor is it necessarily going to help us write a proof that other readers can understand.

The Dafny introduction slides linked in the margin quote Herman Geuvers to answer the question, 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?

The proof rules above are about convincing, but our starting point should be explaining — and an objective of Dafny is to permit us to focus on explaining, with the hope that by explaining our reasoning in Dafny’s terms, a great many details of the convincing can be generated and proved automatically by the system.

For example, we could have started off ZeroMod2_Implies_Even differently:

lemma ZeroMod2_Implies_Even_of_n(n: int) // the original version
  requires n > 0
  ensures (n % 2 == 0) ==> (exists m: int :: m > 0 && n == 2 * m)
{
  assert n % 2 == 0 ==> n == 2 * (n/2);
}

lemma ZeroMod2_Implies_Even_forall() // remove argument n, use forall
  ensures forall n: int :: (n > 0) ==> (n % 2 == 0) ==> (exists m: int :: m > 0 && n == 2 * m)
{
  assert forall n: int :: n % 2 == 0 ==> n == 2 * (n/2);
}

Instead of “given integer n where n > 0, then …” this new lemma has the form “for all integers n, if n > 0, then …”. These statements are identical. But the first option, choosing an arbitrary fixed value of n for the proof, makes it easier to read the precondition, easier to read the postcondition, and easier to state the argument we needed to convince Dafny (and perhaps the reader).

lemma ZeroMod2_Implies_Even(n: int) 
  requires ???
  ensures exists m: int :: m > 0 && n == 2 * m
{
  assert n == 2 * (n/2);
}

lemma Example() {
  ZeroMod2_Implies_Even(42);
  assert exists m: int :: 42 == 2 * m;
}

These two strategies of:

• fixing arbitrary values so we don’t need to state a universal quantification, and

• fixing assumptions so we don’t need to state an implication

… are two of the approaches we will use in class 9 as we talk about writing proofs that explain our reasoning and convince Dafny.

In class we will also meet the Skolemization operation :| which is considerably more exciting than its emoji interpretation suggests! :P

Summary

Dafny may have seemed like an irritable magic genie so far, arbitrarily deciding to prove true facts for us or not. In fact, there are plenty of heuristics underlying any practical automated theorem prover for a logical language as expressive as Dafny’s. However, it helps to understand the fundamental rules of logic that those heuristics might apply. If the logical rules don’t permit a deduction, Dafny certainly won’t find it! Our framing in terms of proof challenges helps us state those rules concisely, and we introduced the rules for a few of the simpler features of familiar logic. More to come in class!