2013-07-01

## Constructing Proofs with dataprop in ATS

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.