Table of Contents

1. Introduction(top)

This section will explain how to prove your programs in PML ... But, you must first understand that PML has no specific language for proofs: proofs are just programs. However, they are some syntactic sugars that can help to make proofs more readable.

2. The scissors(top)

The first ingredient that we use in PML is 8< which means that this position in the code is not accessible. Here is a trivial but enlightening example:

Correct pml code
val test b = if b then (if b then A[] else 8<) else (if b then 8< else B[]) 

PML checks that scissors are inaccessible using equational reasoning (in an equational theory which contains the evaluation rules of PML). At the first scissors, PML knows that b == true (we will explain == in the next section, for the time being, just consider that this is equality) because we are in the then branch of the outer if and it knows that b == false because we are in the else branch of the inner if. Therefore there is a contradiction at this point and the scissors are legal. The second scissors is similar.

If we write something wrong we get an error message:

Incorrect pml code (with error message)
val test b = if b then 8< else (if b then 8< else B[]) 
Pml output
Wrong indication of impossible case at: /tmp/tmpcqGPlR.pml: line 1 column 23 to column 25

Here as another example with exceptions:

Correct pml code
val rec pred n = match n with
  Zero[] -> raise Undef[]
| Succ[n'] -> n'
val two = try pred Succ[Succ[Succ[Zero[]]]] with _ -> 8<

At the scissors, PML assumes that pred Succ[Succ[Succ[Zero[]]]] == raise Undef[] but the evaluation rules of PML implies that pred Succ[Succ[Succ[Zero[]]]] == Succ[Succ[Zero[]]] and hence do not raise any exception. Again, there is a contradiction and PML detects it.

3. Specifications(top)

In records, we can add specifications. Specifications are properties that we prove to be true. A property is just a program of type bool. The syntax is val id x1 ... xn |- A proof P and it means that the property A named id is true for all values of x1 ... xn. P is the proof of A. But what is a proof ? In fact, it is a piece of program which has the empty type ([]), raise no exception and trigger no errors. The only object of such a type is the scissors. This means that all the branches of P must end with 8<. This is possible because PML checks the validity of P under the hypothesis A == false.

Here is a first example:

Correct pml code
open bool
val excluded_middle x |- x || not x
  proof if x then 8< else 8<

At the beginning of the proof PML assumes (x || not x) == false. Then, in each branch of the if, knowing that x == true or x == false implies (x || not x) == true.

Two remarks:

4. Restriction of specification(top)

Specifications are stored in the signature (that is the type of a record). Due to restriction in the type-checking algorithm, this implies that a specification should be only local, that is only mention the other field of the record.

In fact, the above example does not respect this rule, because the disjunction and negation are defined in the bool module and therefore not in the same record as excluded_middle.

In fact there are two exceptions to the above rule:

Incorrect pml code (with error message)
open list
open unary_nat

val (A) do_work = fun l0:(list A)  ->
  let n = $length l0 in
  { l0 as l with val prop |- $length l == n proof 8< }

val (A) do_not_work = fun l0:(list A) ->
  (do_work l0).prop
Pml output
Using non local specification (_val0) in prop at: /tmp/tmpcqGPlR.pml: line 9 column 2 to column 19

The problem here is that the specification prop uses the variable n and it escapes its scope in the last line. Still, the first part of the example is valid.

5. Recursive proofs and termination checker(top)

We can also prove specification by induction. Here is an exemple

Correct pml code
open bool
open list

val (A) for_all f:(A => bool) l:(list A) = fold_right (fun x a -> and (f x) a) l true

val rec (A) for_all_and f:(A => bool) g:(A => bool) l:(list A)
  |- (for_all f l && for_all g l) <=> for_all (fun x -> f x && g x) l
  proof
    match l with
      [] -> 8<
    | x::l' ->
        deduce (for_all f l' && for_all g l') <=> for_all (fun x -> f x && g x) l' by
          let hyprec = for_all_and f g l' in 8< in 
	if f x then 
	  if g x then 
            8< 
          else 
	    if for_all f l then 
              8< 
            else 8<
	else 8<
    endmatch

It is very important to know that the proof of a result must be a terminating program. This means that all functions in the proof and the proof itself must terminates and should not trigger exceptions nor errors.

The termination checker (written by Pierre Hyvernat) is only able to establish the termination of mutually recursive functions that do recursive call on arguments which are structurally smaller than the input. Here it works because the recursive call is on l' which is a sub-list of the input l

One also notice the syntactic sugar deduce whose translation will be given in the next section.

This proof is not easy to understand, because the case analysis at the end is needed to unblock the evaluation of conjunction which is done by looking at the first argument. Fortunately, one can ask PML to try case analysis suggested by blocked evaluations (and nothing more) using #set proof_depth = N when N is the number of imbricated cases allowed (this suggests N = 3 here). Moreover, case analysis where all cases but one are not counted but still require N > 0. In fact, N = 1 is enough for the above example.

This gives the following minimal proof:

Correct pml code
open bool
open list

val (A) for_all f:(A => bool) l:(list A) = fold_right (fun x a -> and (f x) a) l true

val rec (A) for_all_and f:(A => bool) g:(A => bool) l:(list A)
  |- (for_all f l && for_all g l) <=> for_all (fun x -> f x && g x) l
  proof
    match l with
      [] -> 8<
    | x::l' ->
        let hyprec = for_all_and f g l' in 
	#set proof_depth = 1 in 8<
    endmatch

6. Syntactic sugar for proofs(top)

Here are some syntactic sugar usable in proofs. More will be added and they might be modified. The design goal here is to allow for a readable style of proofs ...

7. Leibniz equality(top)

There is a predefined equality in PML written u == v. The intended meaning is Leibniz extensional equality, meaning that u can replace v in any context without changing the outcome.

This equality enjoys the following properties:

All these properties are automatic in PML (meaning that you do not need to say anything to use them).

8. Subtypes and specification in signatures(top)

9. Controlling errors(top)

10. Field values stored in signature(top)

11. Field values usable only in proofs(top)

TODO:: this is not implemented yet