Propositions

Jean-Baptiste Tristan & K. Rustan M. Leino

Dafny as a proof assistant

Dafny is a genuine programming language
- Implemented using a compiler (including type checking) to write and execute programs
It is also a proof assistant
- You can state and prove mathematical propositions
- More generally, you can formalize mathematical theories
  - Arithmetic, set theory, group theory, measure theory, etc…
Our ultimate goal (and Dafny's purpose) is to verify programs, not mathematics
- Yet, an expert Dafny user must have a solid understanding of how to prove theorem in Dafny

Theories

In Dafny, you define theories with
- Symbols
  - Types
  - Functions
  - Constants
  - Predicates
- Propositions

Type symbols

Dafny is a type theory:
- A proposition (mathematical statement) has a type: bool
- Any term that constitutes a proposition has a type
You can declare the existence of types and give them definitions
A type can be empty
Types can have type characteristics
- 00 says the type is nonempty
- Note that auto-init (0) implies nonempty (00)
NaturalNumber stands for a fixed but arbitrary, nonempty type
```
  type NaturalNumber(00)
```
A type can be parameterized by other types (a so-called type operator)
```
  type NaturalNumber(00)
```

Constant symbols

You can declare the existence of constants
They must have a type
```
  ghost const zero: NaturalNumber
```
zero stands for a fixed but arbitrary constant of type NaturalNumber
Since we are stating zero's existence, we need to know that NaturalNumber is nonempty
For now, think of the keyword ghost as telling us that this constant is a mathematical object, not a programming one

Function symbols

A constant with a function type is called a function

A function symbol can be declared by function

  ghost function Successor(n: NaturalNumber): NaturalNumber

Functions can have
- Type parameters
- Typed parameters
Functions have a return type

Predicate symbols

A function with return type bool is called a predicate

A predicate symbol can be declared by predicate

  ghost predicate Less(n: NaturalNumber, m: NaturalNumber)

Note that the “: bool” is implicit for a predicate

Lemmas

A functional (“executable”) expression of type bool represents a mathematical formula that can be false or true
They are sometimes called propositions

Propositions can be named using a lemma

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

A lemma has a name (here, Proposition)
The proposition stated by a lemma is given after the ensures keyword
- We call it the ensures clause of the lemma

Lemma schema

More generally, a lemma names a family of formulas

In the simplest case, the formula is unique

  lemma Prop() 
    ensures forall x: int :: x % 2 == 0 ==> (x / 2) * 2 == x

Schemas with parameters

The lemma can have type parameters and typed parameters
There is one formula for each possible instantiation of these parameters
```
  lemma Prop<T>(x: T) 
    ensures x == x
```

Schemas with preconditions

A lemma can have a requires clause, which is a precondition

It restricts the set of formulas to those whose parameterizations satisfy the precondition

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

Type test

We will now introduce the language of propositions (and terms/expressions)
Every expression has a type
There is an expression to test if an expression is of a certain type
It uses the keyword is
It evaluates to a Boolean value
We will use that expression to introduce the syntax and types of expressions in Dafny
```
  predicate IntPlus3IsInt(n: int) { (n + 3) is int }
```

Basic expressions

  predicate ConditionalExpression<T>(bexpr: bool, expr1: T, expr2: T)  { 
    (if bexpr then expr1 else expr2) is T
  }

  predicate LetBinding<U, V>(expr1: U, expr2: V) { (var x := expr1; expr2) is V }

  predicate Tuple<T, U, V>(t: T, u: U, v: V) { (t, u, v) is (T, U, V) }

  predicate TupleAccess0<T, U, V>(tup: (T, U, V)) { tup.0 is T }

  predicate TupleAccess1<T, U, V>(tup: (T, U, V)) { tup.1 is U }

  predicate TupleAccess2<T, U, V>(tup: (T, U, V)) { tup.2 is V }

In the let expression var x := expr1; expr2
- x is just a name for the value of expr1
- You can replace x by expr1 in expr2 without changing the value of the expression
- x cannot be updated, despite the fact that let expressions use the keyword var

Anonymous functions and application

  predicate LambdaAbstraction<U, V>(expr: V) { ((x: U) => expr) is U -> V }

  predicate Application<U, V>(fun: U -> V, arg: U) { fun(arg) is V }

Propositions != expressions

All functional expressions of type bool are valid propositions
Other RHS expressions are not valid propositions
Some propositions are not valid functional expressions

Propositional logic

Type: bool

  // Constants
  lemma False()
    ensures false 
  lemma True()
    ensures true 

  // Predicates
  lemma Conjunction(a: bool, b: bool)
    ensures a && b 
  lemma Disjunction(a: bool, b: bool)
    ensures a || b 
  lemma Implication(a: bool, b: bool)
    ensures a ==> b 
  lemma Explication(a: bool, b: bool)
    ensures a <== b 
  lemma Equivalence(a: bool, b: bool)
    ensures a <==> b 
  lemma Negation(a: bool)
    ensures !a

First-order logic

The language of propositions includes quantifiers that are not functional expressions

  type T
  
  ghost predicate P(x: T)

  lemma PredicateLogicConnectives()
    ensures (forall x: T :: P(x)) is bool
    ensures (exists x: T :: P(x)) is bool

Note: propositions need not be computable and they cannot always be compiled

Second-order logic

You can quantify over predicates and state properties from second order logic

  lemma SecondOrder()
    ensures forall P: int -> bool :: forall x: int :: P(x) || !P(x)

Higher-order logic

In fact, you can quantify over any value and Dafny is a higher-order logic

  lemma ThirdOrder()
    ensures forall P2: (int -> bool) -> bool :: forall P1: int -> bool :: P2(P1) || !P2(P1)

Impredicativity of propositions

Dafny is impredicative: a predicate can be defined by quantifying over all predicates

  lemma Impredicative()
    ensures forall x: T :: forall P: T -> bool :: P(x)

Predicativity of polymorphism

Dafny's polymorphism is predicative: type parameters always appear before typed parameters

Note, Dafny performs a syntactic rewrite called type-parameter completion on signatures¹

This ensures that all type arguments are filled in
This should not be confused for first-class higher-order type operators

  type List<X>

  function F<T>(x: T): T {
    x
  }

  function G(): List -> List {  // expands to:  function G<_T0>(): List<_T0> -> List<_T0>
    F<List>                     // expands to:  F<List<_T0>>
  }

Partiality

Dafny is a partial logic: some propositions, while syntactically correct, are rejected
In this example, Dafny rejects this proposition because 1/x is not defined for x == 0
```
  lemma Partial() 
    ensures forall x: int :: x * 1/x == x 
```
Note for experts:
- Dafny only pretends to be a partial logic
- In reality, it ensures that nothing can be proved about an undefined term
- The existing implementation requires propositions to be proved to be defined
- An implementation could also ensure that nothing can be proved about an undefined term

Partiality and proofs

Dafny therefore needs to verify whether a proposition is acceptable
To do so, it actually proves that the proposition is defined

In this example, Dafny can prove that x will not be equal to 0

  lemma Partial() 
    ensures forall x: int :: x != 0 ==> x / x == 1

Conclusion: in Dafny, the language of propositions depends on provability
And vice versa

Description

You can use Hilbert's Epsilon operator to choose a value satisfying some property

  predicate P(x: int)

  lemma HilbertEpsilon() 
    requires forall x: int :: P(x)
    ensures var x: int :| P(x); true

Referential transparency

Dafny is not referentially transparent²

The following proposition is false in Dafny:

  lemma NotReferentiallyTransparent()
    ensures (var x: int :| true; x) == (var x: int :| true; x)

Subtypes

You can combine a type and a proposition to define a subset type

  type T

  predicate P(x: T) 

  type U = x: T | P(x)
    witness *

Elements of type U are elements of type T that satisfy predicate P
A subset type is empty if the predicate never holds
The witness clause allows you to provide a witness if you want to guarantee that the type is inhabited
The witness * clause says that the type may be empty

Empty subset types

Example of nonempty subset type with a witness

  type T(00)

  ghost const k: T

  type U = x: T | true
    ghost witness k

Subtyping

If type U is defined as a subset type of T then U is a subtype of T

Consider the following types

  type T 

  predicate P1(x: T)

  type U = x: T | P1(x) witness *

  predicate P2(x: U)

  type V = x: U | P2(x) witness *

U is a subtype of T
- the inhabitants of U are those T inhabitants x for which P1(x) holds
V is a subtype of U
- the inhabitants of V are those U inhabitants x for which P2(x) holds
- the inhabitants of V are those T inhabitants x for which P1(x) && P2(x) holds

Subtyping for functions

Function type A -> B is a subtype of C -> D if

C is a subtype of A
B is a subtype of D

  lemma Subtyping(h: (V -> T) -> bool, f: U -> U)
    ensures h(f)

Covariant subtyping for type parameters

If a type operator S is covariant in its parameter (declared with +) then
- if U is a subtype of V, then S<U> is a subtype of S<V>
```
  type S<+X> 

  lemma Subtyping(f: S<U> -> bool, y: S<V>)
    ensures f(y) 
```

Contravariant subtyping for type parameters

If a type operator S is contravariant in its parameter (declared with -) then
- if U is a subtype of V, then S<V> is a subtype of S<U>
```
  type S<-X> 

  lemma Subtyping(f: S<U> -> bool, y: S<T>)
    ensures f(y)
```

Restrictions on type synonyms

To ensure that it remains consistent, Dafny sometimes rejects the definition of a type operator
```
  type S<!X> = X -> bool
```
In this example, because of how the type parameter X is used, Dafny asks for the parameter to be marked as !
This limits the how it can be instantiated
A covariant type parameter that needs to be restricted is declared as * instead of +

Logic expressiveness

Dafny's language of proposition is rich enough to be a foundation for mathematics
For example, you can axiomatize set theory

Theory: integers

Type: int

Mathematical integers: no max, no min

  // Constants
  lemma DecimalLiteral() ensures 38 is int
  lemma HexadecimalLiteral() ensures 0xBadDecaf is int
  lemma ReadableLiteral() ensures 4_345_765 is int
  // Functions
  lemma Negation(n: int) ensures -n is int 
  lemma Addition(n: int, m: int) ensures (n + m) is int
  lemma Substraction(n: int, m: int) ensures (n - m) is int
  lemma Multiplication(n: int, m: int) ensures (n * m) is int
  lemma Division(n: int, m: int)
    requires m != 0
    ensures (n / m) is int
  lemma Remainder(n: int, m: int)
    requires m != 0
    ensures (n % m) is int
  // Predicates
  lemma Equality(n: int, m: int) ensures n == m 
  lemma Disequality(n: int, m: int) ensures n != m
  lemma LessOrEqual(n: int, m: int) ensures n <= m
  lemma LessThan(n: int, m: int) ensures n < m
  lemma GreaterOrEqual(n: int, m: int) ensures n >= m
  lemma GreaterThan(n: int, m: int) ensures n > m

Theory: reals

Type: real

Complete ordered field (cannot construct non-rationals but safe to assume existence)

  // Constants
  lemma DecimalLiteral() ensures 38.98 is real 
  lemma ReadableLiteral() ensures 4_345_765.999_987 is real
  // Functions
  lemma Negation(n: real) ensures -n is real
  lemma Addition(n: real, m: real) ensures (n + m) is real
  lemma Substraction(n: real, m: real) ensures (n - m) is real
  lemma Multiplication(n: real, m: real) ensures (n * m) is real
  lemma Division(n: real, m: real)
    requires m != 0.0
    ensures (n / m) is real
  lemma IntegerToReal(k: int) ensures (k as real) is real
  lemma Floor(n: real) ensures n.Floor is int 
  // Predicates
  lemma Equality(n: real, m: real) ensures n == m
  lemma Disequality(n: real, m: real) ensures n != m
  lemma LessOrEqual(n: real, m: real) ensures n <= m
  lemma LessThan(n: real, m: real) ensures n < m
  lemma GreaterOrEqual(n: real, m: real) ensures n >= m
  lemma GreaterThan(n: real, m: real) ensures n > m

Theory: finite sets

Type: set<T>

  // Constants
  lemma EmptySet<T>() ensures {} is set<T> 

  // Functions
  lemma Cardinality<T>(A: set<T>) ensures |A| is int 
  lemma Union<T>(A: set<T>, B: set<T>) ensures (A + B) is set<T>
  lemma Intersection<T>(A: set<T>, B: set<T>) ensures (A * B) is set<T>
  lemma AsymmetricDifference<T>(A: set<T>, B: set<T>) ensures (A - B) is set<T>

  // Predicates
  lemma Equality<T>(A: set<T>, B: set<T>) ensures A == B
  lemma Disequality<T>(A: set<T>, B: set<T>) ensures A != B
  lemma Subset<T>(A: set<T>, B: set<T>) ensures A <= B
  lemma StrictSubset<T>(A: set<T>, B: set<T>) ensures A < B
  lemma Superset<T>(A: set<T>, B: set<T>) ensures A >= B
  lemma StrictSuperset<T>(A: set<T>, B: set<T>) ensures A > B
  lemma Disjoint<T>(A: set<T>, B: set<T>) ensures A !! B
  lemma Membership<T>(e: T, A: set<T>) ensures e in A
  lemma Absence<T>(e: T, A: set<T>) ensures e !in A

Theory: sets

Type: iset<T>

Set may or may not be finite

  // Functions
  lemma Union<T>(A: iset<T>, B: iset<T>) ensures (A + B) is iset<T>
  lemma Intersection<T>(A: iset<T>, B: iset<T>) ensures (A * B) is iset<T>
  lemma AsymmetricDifference<T>(A: iset<T>, B: iset<T>) ensures (A - B) is iset<T>

  // Predicates
  lemma Equality<T>(A: iset<T>, B: iset<T>) ensures A == B
  lemma Disequality<T>(A: iset<T>, B: iset<T>) ensures A != B
  lemma Subset<T>(A: iset<T>, B: iset<T>) ensures A <= B
  lemma StrictSubset<T>(A: iset<T>, B: iset<T>) ensures A < B
  lemma Superset<T>(A: iset<T>, B: iset<T>) ensures A >= B
  lemma StrictSuperset<T>(A: iset<T>, B: iset<T>) ensures A > B
  lemma Disjoint<T>(A: iset<T>, B: iset<T>) ensures A !! B
  lemma In<T>(e: T, A: iset<T>) ensures e in A
  lemma NotIn<T>(e: T, A: iset<T>) ensures e !in A

Set comprehension

Finite and infinite sets can be created by comprehension

  predicate P(x: int)

  lemma SetOfPValues() 
    ensures (iset x: int | P(x)) is iset

^1.Dafny Power User: Type-Parameter Completion ↩

^2.Compiling Hilbert’s epsilon operator ↩