- 1. Introduction
- 2. The scissors
- 3. Specifications
- 4. Restriction of specification
- 5. Recursive proofs and termination checker
- 6. Syntactic sugar for proofs
- 7. Leibniz equality
- 8. Subtypes and specification in signatures
- 9. Controlling errors
- 10. Field values stored in signature
- 11. Field values usable only in proofs

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.

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

valtest b =ifbthen(ifbthenA[]else8<)else(ifbthen8<elseB[])

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)

Pml outputvaltest b =ifbthen8<else(ifbthen8<elseB[])

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

valrecpred n =matchnwithZero[] ->raiseUndef[] | Succ[n'] -> n'valtwo =trypred 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.

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

openboolvalexcluded_middle x |- x || not xproofifxthen8<else8<

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:

- PML's logic is classical ... you can not restrict PML to intuitionistic logic.
- Specification are in fact not primitive and are just a syntactic sugar using values in signature and controled errors that are explained later.

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:

- Value stored in other files are allowed. That is values that have a global meaning which is always the same, basically because they have an absolute name from the default path. This is the case for the example above where || and not mean in fact bool.or and bool.not.
- a specification not respecting the above restriction can still be used as long as the use of the specification (its projection) is in the scope of the variables which are not fields of the record. Here are examples of what is legal and what is not:

Incorrect pml code (with error message)

Pml outputopenlistopenunary_natval(A) do_work =funl0:(list A) ->letn =$lengthl0in{ l0aslwithvalprop |-$lengthl == nproof8< }val(A) do_not_work =funl0:(list A) -> (do_work l0).prop

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.

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

Correct pml code

openboolopenlistval(A) for_all f:(A => bool) l:(list A) = fold_right (funx a ->and(f x) a) ltruevalrec(A) for_all_and f:(A => bool) g:(A => bool) l:(list A) |- (for_all f l && for_all g l)<=>for_all (funx -> f x && g x) lproofmatchlwith[] -> 8< | x::l' ->deduce(for_all f l' && for_all g l')<=>for_all (funx -> f x && g x) l'bylethyprec = for_all_and f g l'in8<iniff xthenifg xthen8<elseiffor_all f lthen8<else8<else8<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

openboolopenlistval(A) for_all f:(A => bool) l:(list A) = fold_right (funx a ->and(f x) a) ltruevalrec(A) for_all_and f:(A => bool) g:(A => bool) l:(list A) |- (for_all f l && for_all g l)<=>for_all (funx -> f x && g x) lproofmatchlwith[] -> 8< | x::l' ->lethyprec = for_all_and f g l'in#set proof_depth= 1in8<endmatch

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 ...

- assume A in P means if A then P else 8<
- assume A by Q in P means if A then P else Q
- deduce A in P means if A then P else 8<
- deduce A by Q in P means if A then P else Q
- show A in P means if A then 8< else P
- show A by Q in P means if A then Q else P

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:

- It is reflexive: u == u is true.
- It is symmetric: u == v implies v == u
- It is transitive: u == v and v == w imply u == w
- It is a congruence: u == v implies P u == P v for any program P.

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

**TODO:**:
this is not implemented yet