Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
262 lines (198 sloc) 7.33 KB

Theorem Proving

TODO: review and update with correct error messages (after the Hole update). Also talk about log(x).

TODO: this article is outdated since there isn't an equality primitive anymore. It must be updated to use Data.Equal instead.

Simple proofs

Let's prove a theorem about the boolean not:

import Base@0

main : {b : Bool} -> Equal(Bool, %not(not(b)), %b)
  ?a

Evaluate it using fm -t <file>/main and the type checker complains:

Found hole: 'a'.
- With goal... Equal(Bool, not(not(b)), b)
- Couldn't solve it.
- With context:
- b : Bool

Unsolved holes.

Let's pattern-match on b.

import Base@0

main : {b : Bool} -> Equal(Bool, %not(not(b)), %b)
  case/Bool b
  | true  => ?t
  | false => ?f
  : Equal(Bool, %not(not(b)), %b)

Not helpful:

Found hole: 't'.
- With goal... Equal(Bool, not(not(true)), true)
- Couldn't solve it.
- With context:
- b : Bool

Found hole: 'f'.
- With goal... Equal(Bool, not(not(false)), false)
- Couldn't solve it.
- With context:
- b : Bool

Unsolved holes.

If we reduce both sides, we get the same expression: {true, false} => true. In this case, we can use refl:

import Base@0

main : {b : Bool} -> Equal(Bool, %not(not(b)), %b)
  case/Bool b
  | true  => refl(~Bool, ~%true)
  | false => ?f
  : Equal(Bool, %not(not(b)), %b)

Progress, compiler now complains about the false branch:

Found hole: 'f'.
- With goal... Equal(Bool, not(not(false)), false)
- Couldn't solve it.
- With context:
- b : Bool

Unsolved holes.

We can do the same:

import Base@0

main : {b : Bool} -> Equal(Bool, %not(not(b)), %b)
  case/Bool b
  | true  => refl(~Bool, ~%true)
  | false => refl(~Bool, ~%false)
  : Equal(Bool, %not(not(b)), %b)

No type error. Our proof is complete! If we used case'd args, the proof becomes just:

import Base@0

main : {case b : Bool} -> Equal(Bool, %not(not(b)), %b)
| true  => refl(~Bool, ~%true)
| false => refl(~Bool, ~%false)

Inductive proofs

Let's prove a similar theorem, but for negation on arbitrary-length bit-strings instead of plain booleans:

import Base@0

// {-  From Bits@0
// T Bits
// | b0 {pred : Bits}
// | b1 {pred : Bits}
// | be-}

#bnot*n : !{case halt bits : Bits} -> Bits
| b0 => b1(bnot(bits.pred))
| b1 => b0(bnot(bits.pred))
| be => be

Start with the theorem we want to prove:

#main*n : !{bits : Bits} -> Equal(Bits, %($bnot(n))(($bnot(n))(bits)), %bits)
  ?a
  halt: ?b

Remember that halt: is mandatory on recursive definition to provide the base-case. TODO: explain why the -#s on the type.

The type checker complains:

Found hole: 'a'.
- With goal... Equal(Bits, $bnot(step(n))($bnot(step(n))(bits)), bits)
- Couldn't solve it.
- With context:
- n    : Ind
- n    : -Ind
- main : {bits : Bits} -> Equal(Bits, $bnot(n)($bnot(n)(bits)), bits)
- bits : Bits

Found hole: 'b'.
- With goal... Equal(Bits, $bnot(base)($bnot(base)(bits)), bits)
- Couldn't solve it.
- With context:
- n    : Ind
- bits : Bits

Unsolved holes.

Notice that:

  1. It asks for P(step(n)) instead of P(n).

  2. We have, on context, main, which gives us P(n).

That's because the body of a recursive function is actually the step case of inductive proof, so all we need to do is, assuming P(n), prove P(step(n))!

Let's match against bits:

#main*n : !{bits : Bits} -> Equal(Bits, %($bnot(n))(($bnot(n))(bits)), %bits)
  case/Bits bits
  | b0 => ?b0
  | b1 => ?b1
  | be => ?be
  : Equal(Bits, %($bnot(n))(($bnot(n))(bits)), %bits)
  halt: ?b

Now the complaint becomes:

Type mismatch.
- Found type... Hole
- Instead of... bnot(step(n), bnot(step(n), b0(pred))) == b0(pred)
- When checking ?
- On expression {bits} => ?
- With the following context:
- n    : Ind
- n    : Ind
- main : {bits : Bits} -> bnot(n, bnot(n, bits)) == bits
- bits : Bits
- pred : Bits

This is better because now it expects b0(pred) instead of just bits . This allows the left-side of the equation to be reduced to:

b0(bnot(n, bnot(n, pred))) == b0(pred)

This is perfect because we can use the inductive hypothesis to get this same equation, without the b0s. As in, we need to go...

from :    bnot(n, bnot(n, bs))  == b0(bs)
to   : b0(bnot(n, bnot(n, bs))) ==    bs

All we need is to add b0 on both sides. We can do it with cong, from the base libraries (Base@0):

#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
  case/Bits bits
  | b0 => cong(~Bits, ~Bits, ~(<bnot(n)>)((<bnot(n)>)(pred)), ~pred, ~b0, ~main(pred))
  | b1 => ?
  | be => ?
  : <bnot(step(n))>(<bnot(step(n))>(self)) == self
  halt: ?

TODO: should we have a built-in syntax to simplify cong?

Now the checker complains about the b1 case:

Type mismatch.
- Found type... Hole
- Instead of... bnot(step(n), bnot(step(n), b1(pred))) == b1(pred)
- When checking ?
- On expression {pred} => ?
- With the following context:
- n    : Ind
- n    : Ind
- main : {bits : Bits} -> bnot(n, bnot(n, bits)) == bits
- bits : Bits
- pred : Bits

We can easily complete this proof now:

#main*n : !{bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
  case/Bits bits
  | b0 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(pred)), ~pred, ~b0, ~main(pred))
  | b1 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(pred)), ~pred, ~b1, ~main(pred))
  | be => refl(~be)
  : <bnot(step(n))>(<bnot(step(n))>(self)) == self
  halt: refl(~bits)

As usual, it could be simplified with case'd arguments:

#main*n : !{case bits : Bits} -> <bnot(n)>(<bnot(n)>(bits)) == bits
| b0 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(bits.pred)), ~bits.pred, ~b0, ~main(bits.pred))
| b1 => cong(~Bits, ~Bits, ~<bnot(n)>(<bnot(n)>(bits.pred)), ~bits.pred, ~b1, ~main(bits.pred))
| be => refl(~be)
halt: refl(~bits)

Note that the big difference here, with relation to Agda/Coq proofs, is that, in their cases, since recursive functions are defined by structural recursion, inductive proofs are also defined by recursion on the structure. For example, if we wanted to prove this theorem in Agda, we'd just match the bit-string, prove the base case by reflexivity, and prove the recursive case by calling main recursively on pred.

In Formality, it looks like the proof is the same, but there is a subtle, yet important, difference: under the hoods, we're not actually recursing on the Bits structure. Instead, we're folding over n : Ind, a datatype capturing the inductive hypothesis on natural numbers. As such, in order to prove that bnot(n, bnot(n, bits)) == bits hold for any n, we first must prove that it is true for n == 0, i.e., when bits has a maximum recursion depth of 0 (i.e., is "out-of-gas"), which is true by reflexivity since the function returns bits itself. We then prove that assuming this is true for a maximum recursion depth of n, then it is also true for bits(step(n)). This is the step case, which coincides with Agda's proof.

Proving that kind of inductive theorem on Formality is a little more verbose than in Agda, since you have to wrap the whole proof inside Ind, and always tell the compiler what to do when the function "runs out of gas". In exchange, since termination is guaranteed by EAL, there is no "structural recursion" checker, so you're allowed to be more flexible in your recursive definitions.

You can’t perform that action at this time.