Structured Proofs

Jean-Baptiste Tristan & K. Rustan M. Leino

Recall

A Dafny proposition is a Boolean-valued expression, not always computable
- Expressiveness similar to that of higher-order logic
- Rich enough for mathematics
A Dafny proof is a sequence of statements (tactics)
- assume
- assert
- call
- Skolemization :|
- assignment :=
- conditional if
- forall
With these statements, one can write proofs in a style similar to informal mathematics

Proofs that convince

There are well-defined rules for what constitutes a valid proof
We can use these rules to construct a detailed proof
If your proof is valid and detailed enough, Dafny will accept it
Dafny's deduction system can simulate:
- The Hilbert-Frege proof system
- Natural deduction
- Sequent calculus

Summary

A model of the proof state
A proof semantics for statements
Structuring proofs
- How to prove
- How to use
Detailed example
- Procedural
- Declarative
Poincare principle

Lemmas and proofs

Recall that a lemma can be understood as a set of propositions
When a proof is not provided, these propositions are axioms
When a proof is provided, the lemma can be understood as a proof challenge

Example:

  lemma Example(x: int) 
    requires x % 2 == 0 
    ensures 2 * (x / 2) == x

Assuming (hypothesis):
- We have some fixed but arbitrary x of type int
- x % 2 == 0 holds
Prove (goal):
- 2 * (x / 2) == x

A notation for lemmas

We can summarize this proof challenge with the following notation:
- x: int, x % 2 == 0 |- 2 * (x / 2) == x
Where:
- The facts left of |- are hypothesis
- The fact right of |- is the goal
- We read |- as “prove”

Proof challenges and automated theorem proving

At a high level, Dafny verifies a lemma by challenging an automated theorem prover (ATP)
Recall that a proof script is a sequence of statements and consider the simplest possible proof: the empty sequence
```
  lemma Example(x: int) 
    requires x % 2 == 0 
    ensures 2 * (x / 2) == x
  {
  }
```
In this case, the proof challenge is simply derived from the lemma itself:
- x: int, x % 2 == 0 |- 2 * (x / 2) == x
It so happens that, in this example, the ATP will meet the challenge

From lemma and proof to challenges

In general, the proof script that follows a lemma affects what challenges will be thrown at the ATP
This raises two questions:
- What proof challenges can the ATP meet?
- How does Dafny generate proof challenges from a lemma and a proof script?

Automated theorem proving

Perhaps surprisingly, we will work under the assumption that the ATP is largely a black box
This is a good assumption to make:
- What challenges an ATP can meet is difficult to characterize
- You may want to use different configurations of an ATP
- You may want to use different ATPs
- ATPs have a discontinuous behavior: small changes to a proof challenge can result in different outcomes
So, what should you know about the ATP?

The trivial challenge

One challenge that any ATP should meet is to prove that something we are assuming holds

  lemma AndIntro<T1, T2, T3, T4>(x1: T1, x2: int, x3: int -> T4, P: bool, Q: T1 -> bool)
    requires Q(x1)
    requires P
    ensures P
  {}

Several important notes:
- Because any proposition/predicate is bool-valued, P, Q, and R could stand for any propositions/predicates
- Could be generalized to any finite number of type parameters (in any order)
- Could be generalize to any finite number of typed parameters (in any order)
- This could be generalized to any finite number of requires (in any order): all we need is that P is assumed

The essence of a challenge

The essence of this challenge can be summarized as:
- If a propostion P is in the list of propositions you assume to hold, then it holds
- Regardless of the rest of the hypotheses
We use a frugal notation to capture the essence of the challenge
```
Γ, P ⊢ P
```
Where:
- Γ (read “gamma”) is a list of type parameters, typed parameters, and propositions
- The order of elements of the list is irrelevant, so we add P to the end for convenience of notation

Basic challenges: conjunction

Proving a conjunction
```
Γ, P, Q ⊢ P && Q
```
Using a conjunction
```
Γ, P && Q ⊢ P
```
```
Γ, P && Q ⊢ Q
```

Basic challenges: disjunction

Proving a disjunction
```
Γ, P ⊢ P || Q
```
```
Γ, Q ⊢ P || Q
```
Using a disjunction
```
Γ, P || Q, P ==> R, Q ==> R ⊢ R
```

Basic challenges: negation

Proving a negation
```
Γ, P ==> false ⊢ !P
```
Using a negation
```
Γ, P, !P ⊢ false
```

Basic challenges: false

If you assume something that is false, anything can be concluded
This is particularly useful to construct proofs incrementally
```
Γ, false ⊢ P
```

Basic challenges: equivalence

Proving an equivalence
```
Γ, P ==> Q, Q ==> P ⊢ P <==> Q
```

Using a equivalence


Γ, P <==> Q ⊢ P ==> Q


Γ, P <==> Q ⊢ Q ==> P

Basic challenges: existential quantifier

Proving an existential quantifier


Γ, T, k: T, P(k) ⊢ exists c: T :: P(c)

Using an existential quantifier


Γ, T, c: T, P(c), (exists x: T :: P(x)) ==> Q ⊢ Q

Basic challenges: universal quantifier


  Γ, T, forall x: T :: P(x), c: T ⊢ P(c)

From proofs to challenges

How does Dafny generate proof challenges from a lemma and a proof script?
This question could be answered precisely, but we will not!
- Understanding how Dafny uses your proof is not the best way to come up with it
Instead, we would like to capture the idea that writing a proof is a linear process
As a first approximation, you can think of a statement as something that modifies the proof challenge

Then, the goal of the proof script is:

  lemma Example<T>(x: T) 
    requires P(x) 
    ensures Q(x) 
  { 
    // T, x: T, P(x) |- Q(x)

    // ...

    // T, x: T, P(x), Q(x) |- Q(x)
  }

Proof semantics: assert

  lemma Example<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    assert R(x) by {
      // T, x: T, P(x) |- R(x)
    } 
    // T, x: T, P(x), R(x) |- Q(x)
  }

Proof semantics: assume

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    assume R(x);
    // T, x: T, P(x), R(x) |- Q(x)
  }

Proof semantics: lemma call – 1

  lemma Premise<T>(x: T)
    requires P(x)
    ensures R(x)

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    Premise<T>(x); // T, x: T, P(x) |- P(x)
    // T, x: T, P(x), R(x) |- Q(x)
  }

Proof semantics: lemma call – 2

  lemma Premise<T>(x: T)
    ensures P(x) ==> R(x)

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    Premise<T>(x);
    // T, x: T, P(x), P(x) ==> R(x) |- Q(x)
  }

Proof semantics: lemma call – 3

  lemma Premise<T>()
    ensures forall x: T :: P(x) ==> R(x)

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    Premise<T>();
    // T, x: T, P(x), forall x: T :: P(x) ==> R(x) |- Q(x)
  }

Proof semantics: conditional statement – 1

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    if R(x) {
      // T, x: T, P(x), R(x) |- S(x)
    }
    // T, x: T, P(x), R(x) ==> S(x) |- Q(x)
  }

Proof semantics: conditional statement – 2

  lemma Premise<T>(x: T)
    requires P(x)
    ensures R(x)

  lemma Conclusion<T>(x: T)
    ensures P(x) ==> Q(x)
  {
    // T , x: T |- P(x) ==> Q(x)
    if P(x) {
      Premise(x); // T, x: T, P(x) |- P(x)
      // T, x: T, P(x) |- Q(x)
    }
    // T, x: T, P(x) ==> R(x) |- P(x) ==> Q(x)
  }

Proof semantics: forall statement

  lemma Conclusion<T>(x: T)
    requires P(x)
    ensures Q(x)
  {
    // T, x: T, P(x) |- Q(x)
    forall x: T
      ensures R(x)
    {
      // T , x: T, P(x) |- R(x)
    }
    // T, x: T, P(x), forall x: T :: R(x) |- Q(x)
  }

Proof semantics: variable choice

  lemma Conclusion<T>()
    requires exists y: T :: P(y)
    ensures A
  {
    // T, exists x: T :: P(x) |- A
    var y: T :| P(y); 
    // T, y: T, P(y) |- A
  }

Proof semantics: variable assigment

  lemma Conclusion<T>(x: T)
    ensures A
  {
    // T, x: T |- A
    var y: T := x; 
    // T, x: T, y: T, y == x |- A
  }

Example

  lemma Premise<T>(x: T)
    requires P(x)
    ensures Q(x)

  lemma Conclusion<T>()
    ensures forall x: T :: P(x) ==> Q(x)
  {
    // T |- forall x: T :: P(x) ==> Q(x)
    forall x: T
      ensures P(x) ==> Q(x)
    {
      // T , x: T |- P(x) ==> Q(x)
      if P(x) {
        Premise(x); // T, x: T, P(x) |- P(x)
        // T, x: T, P(x) |- Q(x)
      }
      // T, x: T, P(x) ==> Q(x) |- P(x) ==> Q(x)
    }
    // T , forall x: T :: P(x) ==> Q(x) |- forall x: T :: P(x) ==> Q(x)
  }

Structuring a proof

Two sets of rules
Going backward from the goal
- How to prove
- Follow the structure of the goal
Going forward from the premises
- How to use
- Use existing facts or generalize

Incrementally writing a proof with assume

A proof is not done until you have removed all uses of assume statements
In the end, you do not want any assume to appear in your proof
However, assume is a fantastic tool to grow a proof and make sure that it is going in the right direction

One by one, you will need to replace an assume, and this can be done in one of two ways

  lemma Example() 
  {
    // ...
    assume A; // TODO
    // ...
  }

Removing an assumption: assert

  lemma Example() 
  {
    // ...
    assert A by {
      assume false; // TODO
    }
    // ...
  }

Removing an assumption: lemma call

  lemma Prior() 
    ensures A

  lemma Example() 
  {
    // ...
    Prior();
    // ...
  }

How to prove: conjunction – procedural

Procedural approach: add to the hypothesis toward an easy challenge

  lemma Example()
    ensures A && B
  {
    // |- A && B
    assume A; 
    // A |- A && B
    assume B; 
    // A , B |- A && B
  }

How to prove: conjunction – procedural to declarative

You can always assume what you want to prove
This allows you to refine the proof using a more declarative style

  lemma Example()
    ensures A && B
  {
    // |- A && B
    assume A && B;
    // A && B |- A && B
  }

How to prove: conjunction – declarative

    assume A && B;

$\Rightarrow$

    assert A && B by {
      assume A;
      assume B;
    }

How to prove: disjunction, procedural – 1

  lemma Example()
    ensures A || B
  {
    // |- A || B
    assume A; 
    // A |- A || B
  }

How to prove: disjunction, procedural – 2

  lemma Example()
    ensures A || B
  {
    // |- A || B
    assume B; 
    // B |- A || B
  }

How to prove: disjunction, declarative – 1

    assume A || B;

$\Rightarrow$

    assert A || B by {
      assume A;
    }

How to prove: disjunction, declarative – 2

    assume A || B;

$\Rightarrow$

    assert A || B by {
      assume B;
    }

How to prove: disjunction, declarative – 3

    assume A || B;

$\Rightarrow$

    assert A || B by {
      if !A {
        assume B;
      }
    }

How to prove: disjunction, declarative – 4

    assume A || B;

$\Rightarrow$

    assert A || B by {
      if !B {
        assume A;
      }
    }

How to prove: implication, procedural

  lemma Example()
    ensures A ==> B
  {
    // |- A ==> B
    if A {
      assume B;
    }
    // A ==> B |- A ==> B
  }

How to prove: implication, declarative – 1

    assume A ==> B;

$\Rightarrow$

    assert A ==> B by {
      if A {
        assume B;
      }
    }

How to prove: implication, declarative – 2

    assume A ==> B;

$\Rightarrow$

    assert A ==> B by {
      if !B {
        assume !A;
      }
    }

How to prove: negation procedural

  lemma Example()
    ensures !A
  {
    // |- !A
    if A {
      assume false;
    }
    // A ==> false |- !A
  }

How to prove: negation, declarative

    assume !A;

$\Rightarrow$

    assert !A by {
      if A {
        assume false;
      }
    }

How to prove: universal quantification, procedural

  lemma Exampl<T>()
    ensures forall x: T :: P(x)
  {
    // |- forall x: T :: P(x)
    forall x: T
      ensures P(x)
    {
      assume P(x);
    }
    // forall x: T :: P(x) |- forall x: T :: P(x)
  }

How to prove: universal quantification, declarative

    assume forall x: nat :: P(x);

$\Rightarrow$

    assert forall x: nat :: P(x) by {
      forall x: nat
        ensures P(x)
      {
        assume P(x);
      }
    }

How to prove: existential quantification, procedural

  lemma Example<T>(c: T)
    ensures exists x: T :: P(x)
  {
    // |- exists x: T :: P(x)
    assume P(c);
    // exists x: T :: P(x) |- exists x: T :: P(x)
  }

How to prove: existential quantification, declarative

    assume exists x: nat :: P(x);

$\Rightarrow$

    assert exists x: nat :: P(x) by {
      assume P(c);
    }

How to use: implication

  lemma Example()
    requires A ==> B
    ensures B
  {
    // A ==> B |- B
    assume A;
    // A ==> B, A |- B
  }

How to use: disjunction

  lemma Example() 
    requires A || B 
    ensures C
  {
    // A || B |- C
    if A {
      assume C;
    }
    // A || B, A ==> C |- C 
    if B {
      assume C;
    }
    // A || B, A ==> C, B ==> C |- C
  }

How to use: negation

  lemma Example() 
    requires !A
    ensures false 
    {
      // !A |- false 
      assume A; 
      // !A, A |- false
    }

How to use: existential

  lemma Example<T>() 
    requires exists c: T :: P(c)
    ensures C 
  {
    // exists c: T :: P(c) |- C 
    assume forall x: T :: P(x) ==> C;
    // exists c: T :: P(c), forall x: T :: P(x) ==> C |- C 
    var c: T :| P(c);
    // exists c: T :: P(c), c:T, P(c), forall x: T :: P(x) ==> C |- C 
  }

How to use: congruence of propositions

    assume A;

$\Rightarrow$

    assert A by {
      assume A == B;
      assume B;
    }

How to use: congruence of terms

    assume P(c);

$\Rightarrow$

    assert P(c) by {
      assume c == d;
      assume P(d);
    }

Detailed example

We have seen the basics of formalizing proofs
Rules of deduction
How they can be encoded in Dafny
Let's formalize the proof of the following lemma

Lemma 1.

$\forall x: nat \cdot\; x \% 2 = 0 \Rightarrow \exists y: nat \cdot\; x = 2 \times y$

In english

Lemma 2.

\forall x: nat \cdot\; x \% 2 = 0 \Rightarrow \exists y: nat \cdot\; x = 2 \times y

Proof.
Let $$x$$ be some fixed but arbitrary natural number.
We assume that $x\%2 = 0$ .
Since the remainder of the division of $$x$$ by $$2$$ is $$0$$ , then by definition, $$x$$ is divisible by $$2$$ and has a unique divisor.
Let's call this divisor $$y$$ , we have that $x =2 \times y$ .

Procedural – 1

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y

Procedural – 2

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    assume false; // TODO












    
    // false |- GOAL
  }

Procedural – 3

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    assume forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y; // TODO













    // GOAL |- GOAL
  }

Procedural – 4

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
      assume false; // TODO









      // x: nat, false |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    }
    // GOAL |- GOAL
  }

Procedural – 5

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
      assume x % 2 == 0 ==> exists y: nat :: x == 2 * y; // TODO








      // x: nat, x % 2 == 0 ==> exists y: nat :: x == 2 * y 
      //                  |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    }
    // GOAL |- GOAL
  }

Procedural – 6

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
      if x % 2 == 0 {
        // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
        assume false; // TODO




        // x: nat, x % 2 == 0, false |- exists y: nat :: x == 2 * y
      }
      // x: nat, x % 2 == 0 ==> exists y: nat :: x == 2 * y 
      //                  |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    }
    // GOAL |- GOAL
  }

Procedural – 7

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
      if x % 2 == 0 {
        // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
        assert exists y: nat :: x == 2 * y by {
          // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
          assume false; // TODO
          // x: nat, x % 2 == 0, false |- exists y: nat :: x == 2 * y
        }
        // x: nat, x % 2 == 0, exists y: nat :: x == 2 * y |- exists y: nat :: x == 2 * y
      }
      // x: nat, x % 2 == 0 ==> exists y: nat :: x == 2 * y 
      //                  |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    }
    // GOAL |- GOAL
  }

Procedural – 8

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    // |- GOAL
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      // x: nat |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
      if x % 2 == 0 {
        // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
        assert exists y: nat :: x == 2 * y by {
          // x: nat, x % 2 == 0 |- exists y: nat :: x == 2 * y
          assert x == 2 * (x / 2);
          // x: nat, x % 2 == 0, exists y: nat :: x == 2 * y |- exists y: nat :: x == 2 * y
        }
        // x: nat, x % 2 == 0, exists y: nat :: x == 2 * y |- exists y: nat :: x == 2 * y
      }
      // x: nat, x % 2 == 0 ==> exists y: nat :: x == 2 * y 
      //                  |- x % 2 == 0 ==> exists y: nat :: x == 2 * y
    }
    // GOAL |- GOAL
  }

Declarative – 1

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y

Declarative – 2

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    assume false; // TODO
  }

Declarative – 3

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      assume false; // TODO
    }
  }

Declarative – 4

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      if x % 2 == 0 {
        assume false; // TODO
      }
    }
  }

Declarative – 5

  lemma s1()
    ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
  {
    forall x: nat
      ensures x % 2 == 0 ==> exists y: nat :: x == 2 * y
    {
      if x % 2 == 0 {
        assert x == 2 * (x / 2);
      }
    }
  }

Proofs that calculate

An important class of propositions are of the form $\exists x \cdot P(x)$
One way to prove that a value satisfying a predicate exist is to explicitely compute one
Example:
- Prove that for any rational number, there exists another in normal form that has the same value
- One intuitive way to prove this is to show how to cancel out common factors

Back-of-the-envelope calculations

Instead of:

  lemma OddFactor(n: nat)
    requires n % 2 == 1
    ensures exists m: nat :: n == m * 2 + 1
  {
    assert n == n/2 * 2 + 1;
  }

In the same way that you would prove $$2 + 2 = 4$$ by doing the math:

  lemma OffFactorComputed(n: nat) returns (m: nat)
    requires n % 2 == 1
    ensures n == m * 2 + 1
  {
    m := n/2;
  }