Calculational proofs

2 minute pitch

Calculational proofs look like this:

let lem1 (a : pos) : Lemma (2 * a > a) = ()

let calc0 (a : pos) : Lemma (a + a > a) =
  calc (>) {
    a + a;
    == {}
    2 * a;
    > { lem1 a }
    a;
  }

They are a way to structure a proof into "steps" that are checked individually, and which then compose to provide a final result. In this case, we are proving that a + a is greater than a, by first proving that a + a == 2 * a (with an empty justification {}) and then that 2 * a > a by calling lem1 in the justification (just for illustration purposes, as the SMT can of course handle this). F* also checks that if a == b > c, then a > c, rejecting the proof otherwise.

How to use them

A calculational proof is a sequence of expressions (of some type t) related by a sequence of steps plus some top-level relation (i.e. a term of type t -> t -> Type0). Each step is composed of a relation and a justification (proving that the expressions next to it are indeed related). Relations can be either symbols or any parenthesized term. Note that every expression is terminated by a ;.

For instance, the proof of a + a > a above succeeds since:

• a) a + a == 2 * a with proof () ({} is equivalent to {()})
• b) 2 * a > a with proof lem1 a 2
• c) for all x,y,z, if x == y > z, then x > z.

This last condition is currently sent to the SMT solver.

How they work

Calc proofs have no special semantics, they are a simply a desugaring artifact. As such, no extra trust is needed. The real magic occurs in the FStar.Calc module in the standard library. For instance, the proof above is actually sugar for:

let calc0_desugared (a : pos) : Lemma (a + a > a) =
  calc_finish (fun x y -> (>) x y <: Type) (fun () ->
    calc_step (fun x y -> (>) x y <: Type) a (fun () ->
      calc_step (fun x y -> (==) x y <: Type) (2 * a) (fun () ->
        calc_init (a + a)
      ) (fun () -> ())
    ) (fun () -> lem1 a)
  )

Internals

Internally, all justifications are thunked by the desugarer. This helps to not make them visible to each other in the SMT contexts, and allows to admit() single steps while having all others be properly checked.

All relations r are expanded to fun x y -> r x y <: Type0 in order to accept boolean operations like (>) : int -> int -> bool and properly obtain the b2t coercion where needed.

Justifications and steps are not in "logical scope" of each other: admitting a step should not affect others. However, everything is encoded in a single VC for now. We might want to split some parts of it out.