Bluish Coder

My last post that covered using proofs in ATS implemented a stack. In this post I step back a bit and go through some smaller examples using dataprop with proofs using prfun. The examples I work through here are based on the Propositions and Evidence section of Software Foundations. That book covers the Coq Proof Assistant and I've been working through some of the exercises in ATS.

The Propositions and Evidence chapter starts off with introducing a property of natural numbers. Numbers with this property are considered 'beautiful'. A natural number is 'beautiful' if it is 0, 3, 5 or the sum of two beautiful numbers. This is defined in four rules:

• Rule b_0: The number 0 is beautiful.
• Rule b_3: The number 3 is beautiful.
• Rule b_5: The number 5 is beautiful.
• Rule b_sum: If n and m are beautiful, then so is their sum.

This can be expressed in ATS using dataprop:

dataprop BEAUTIFUL (n:int) =
| B_0 (0)
| B_3 (3)
| B_5 (5)
| {m,n:nat} B_SUM (n+m) of (BEAUTIFUL m, BEAUTIFUL n)

A dataprop is similar to a datatype but exists for the proof system. Like other proof elements (prfun, etc) they are erased at compile time and have no runtime overhead. A dataprop is used to encode a relation or proposition. The BEAUTIFUL dataprop uses dependent types - it has a natural number, n, as a type index, making BEAUTIFUL a property of numbers. Each line implements the rules outlined earlier.

In the B_SUM line the section in curly brackets, {m,n:nat}, declares two universal variables. This line should be read as "For all m and and n, which are natural numbers that are beautiful, the sum of those numbers are also beautiful".

Now that we have the proposition we can start assembling proofs. The first proof we look at is proving the second rule - that the number 3 is beautiful. We need to implement this proof function:

prfun three_is_beautiful ():<> BEAUTIFUL 3

A proof function, introduced with prfun or prfn is used to implement proofs that are checked by ATS to ensure programs are correct. prfn is used for non-recursive functions whereas prfun can be recursive. If it is recursive it must be able to prove it can terminate. How this is done will be explained later. This function returns an instance of BEAUTIFUL 3. The :<> section of the definition means that this function is a pure function. It can perform no side effects. All proof functions must be pure and terminating.

The implementation for this proof is simple:

prfn three_is_beautiful ():<> BEAUTIFUL 3 = B_3

The body just returns the B_3 rule. Typechecking this succeeds:

$ atscc -tc proof.dats
The file [proof.dats] is successfully typechecked!

It is possible to declare proof functions but not implement them. This is a way of saying to the compiler that "the proof is self evident". It can be used in cases where proofs are time consuming to implement but nevertheless obvious. In this case, three_is_beautiful is obvious from the rules so we could just declare it without an implementation:

praxi three_is_beautiful ():<> BEAUTIFUL 3

Note here I use praxi instead of prfun. The former is often used for fundamental axioms that don't need to be proved. They are not expected to be implemented. Although the ATS compiler doesn't currently warn if a prfun is unimplemented it may do in the future so it's good practice to use praxi for proofs that aren't intended to be implemented.

The next step up would be to prove some aspect using B_SUM. Let's prove that eight is a beautiful number:

prfn eight_is_beautiful ():<> BEAUTIFUL 8 = B_SUM (B_3, B_5)

The implementation for this constructs a B_SUM of two other BEAUTIFUL rules, B_3 and B_5. Typechecking this confirms that this is enough to prove the rule.

Proof functions can be used to prove (or disprove) claims. For example, someone claims that adding three to any beautiful number will produce a beautiful number. Expressed as a proof function:

prfn b_plus3 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (3+n)

The implementation is trivial and successful typechecking by the ATS compiler proves that any beautiful number, with three added, does indeed produce a new beautiful number:

prfn b_plus3 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (3+n) =
  B_SUM (B_3, b)

Another claim to prove is that any beautiful number multiplied by two produces a beautiful number. The claim, implemented as a proof is:

prfn b_times2 {n:nat} (b: BEAUTIFUL n):<> BEAUTIFUL (2*n) =
  B_SUM (b, b)

A more complicated proof is that any beautiful number multiplied by any natural number is a beautiful number:

prfun b_timesm {m,n:nat} .<m>. (b: BEAUTIFUL n):<>
       [p:nat] (MUL (m,n,p), BEAUTIFUL p) =

This is the first proof function we've looked at that needs recursion. Recursive proof functions must show they can terminate. This is done by adding a termination clause (the bit between .< and >.). The termination clause must contain a static type variable that is used in each recursive call and can be proven to decrement on each call. In this case it is m.

The return result of this proof function includes an existential variable, p and returns a tuple of a MUL proof object and the beautiful number. MUL is part of the ATS prelude. It encodes the relation that for any numbers m and n the number p is m*n. The p here is also included as the type index of the beautiful number returned. The proof then reads as "For all m which are natural numbers, and for all n which are beautiful numbers, there exists a beautiful number p that is m*n".

The implementation of this proof looks like:

sif m == 0 then
  (MULbas, B_0)
else let
  prval (pf, b') = b_timesm {m-1,n} (b)
in
  (MULind pf, B_SUM(b, b'))
end

The first thing you may note is we use sif instead of if. The former is for the static type system which is what the variables m and n belong to. In the case of 0 (multiplying a beautiful number by zero) we return the B_0 rule and the base case for the MUL prop.

In the case of non-zero multiplication we recursively call b_timesm, reducing m on each call. As m and n are universal variables in the static type system they are passed using the {...} syntax. The result of this is summed. We are implementing multiplication via recursive addition basically. More on the use of MUL can be read in the encoding relations as dataprops section of the ATS documentation.

Once we've proven what we want to prove with regards to beautiful numbers, how are they used in actual programs? Imagine a program that needs to add beautiful numbers and display the result. Without any checking it could look like:

fun add_beautiful (n1: int, n2: int): int =
  n1 + n2

fun do_beautiful () = let
  val n1 = 3
  val n2 = 8
  val n3 = add_beautiful (n1, n2)
in
  printf("%d\n", @(n3))
end

This relies on inspection to ensure that numbers are in fact beautiful numbers. Or it could use runtime asserts to that effect. The same program using the proofs we've defined would be:

fun add_beautiful {n1,n2:nat}
         (pf1: BEAUTIFUL n1, pf2: BEAUTIFUL n2
          | n1: int, n2: int): [n3:nat] (BEAUTIFUL n3 | int) =
  (B_SUM (pf1,pf2) | n1 + n2)

fun do_beautiful () = let
  prval pf1 = three_is_beautiful ()
  prval pf2 = eight_is_beautiful ()
  val n1 = 3
  val n2 = 8
  val (pf3 | n3) = add_beautiful (pf1, pf2 | n1, n2)
in
  printf("%d\n", @(n3))
end

This program will not compile if non-beautiful numbers are passed to add_beautiful. We've constructed proofs that the two numbers we are using are beautiful and pass those proofs to the add_beautiful function. It returns the sum of the two numbers and a proof that the resulting number is also a beautiful number.

An exercise for the reader might be to implement an 'assert_beautiful' function that checks if a given integer is a beautiful number using proofs to verify the implementation is correct. The function to implement would allow:

extern fun assert_beautiful (n: int): [n:nat] (BEAUTIFUL n | int n)

fun do_beautiful2 (a:int, b:int): void = let
  val (pf1 | n1) = assert_beautiful (a)
  val (pf2 | n2) = assert_beautiful (b)
  val (pf3 | n3) = add_beautiful (pf1, pf2 | n1, n2)
in
  printf("%d\n", @(n3))
end

As noted in Software Foundations, besides constructing evidence that numbers are beautiful, we can also reason about them using the proof system. The only way to build evidence that numbers are beautiful are via the constructors in the dataprop. In the following example we create a new property of numbers, gorgeous numbers, and prove some relationships with beautiful numbers.

dataprop GORGEOUS (n:int) =
| G_0 (0)
| {n:nat} G_plus3 (3+n) of GORGEOUS (n)
| {n:nat} G_plus5 (5+n) of GORGEOUS (n)

I'll leave as a reader exercise to write some proofs about gorgeous numbers in a similar way we did with beautiful numbers. Try proving that the sum of two gorgeous numbers results in a gorgeous number.

One proof I'll demonstrate here is proving that all gorgeous numbers are also beautiful numbers. Looking at the definition gives an intuitive idea that this is the case. A proof function to prove it looks like:

prfun gorgeous__beautiful {n:nat} (g: GORGEOUS n): BEAUTIFUL n

The implementation uses case+ to dispatch on the possible constructors of GORGEOUS and produce BEAUTIFUL equivalents:

prfun gorgeous__beautiful {n:nat} .<n>. (g: GORGEOUS n): BEAUTIFUL n = 
  case+ g of 
  | G_0 () => B_0
  | G_plus3 g => B_SUM (B_3, gorgeous__beautiful (g))
  | G_plus5 g => B_SUM (B_5, gorgeous__beautiful (g))

This will fail to type check if gorgeous numbers are not also beautiful numbers. It does pass typechecking so we know that this is the case.