CYP: Colour Your Proof

What is a proof for CYP?

CYP is a simple program to help checking proofs. The idea is to translate the usual pen and paper proofs into formal proofs. To do so, the user has to indicate the different components of the proof by colouring them. Once the proof is coloured, it can be sent to the theorem prover to be checked.

An early paper presenting CYP can be found here.

What is a proof for CYP?

A proof is any text file. Of course for the translation to work, there is some pre-requisite. CYP has his own predefined syntax for the objects manipulated by the proof. This syntax has been directly taken from the WHY tool. It corresponds to a strongly typed first-order language. It contains for the terms:

the base types: int, real, ...
the usual arithmetic operations: +, -, *, /, %, ^
the function call: functionName(arg₁, ..., arg_n).

It contains for the propositions:

the proposition type: prop,
the usual arithmetic predicates < &le, >, ≥ that can be extended to interval. So x < y ≤ x + y is a valid predicate,
the generic predicate: predicateName(term₁, ..., term_n),
the usual connectors: conjunction and, disjunction or, implication ->, negation not. For example, not(x and y) -> (not x) or (not y) represents the formula ¬(x ∧ y) → ¬x ∨ ¬y ,
the usual universal and existential quantifiers: forall variables: type. body, exists variables: type. body. For example
forall x, y: int. exists z: int. x = y + z is a valid proposition. Types of quantified variables can be omitted.

Why does the proof need to be coloured?

The colouring process is simply a way to indicate the structure. Once the structure known, it is easy to translate the proof into the theorem prover. Of course a proof has to be coloured in a specific way. The semantic of the proof gives its structure. As finding the structure automatically is far from being easy, we just propose the colouring process as a light alternative.

Colouring is just a graphical way to indicate the structure of the proof. Internally CYP uses tag. When displaying its internal structure, it simply associates a colour to each tag. A tag indicates a region of the proof text and has a specific colour. The core structure has five different tags:

p for proofs,
c for conclusions,
h for hypothesis
v for variables,
n for names.

To illustrate how tags are used, we consider the following proof:

Property exp_pos:
Let x and y be two integers, if 0 < x, to prove 0 < x^y, we have three cases:
      If 0 < y  then x^1 <= x^y
      If 0 = y  then x^y = 1 
      If y < 0  then x^y = 1/(x^(-y))

Note that we have been using indentation only for legibility. The system does not impose any formatting style.

Proof

A proof is indicated by the tag p. Proofs can be nested. In our example, we have a proof that has three subproofs. Its tagged version is then

Property exp_pos:
<p>Let x and y be two integers, if 0 < x, to prove 0 < x^y, we have three cases:
      <p> If 0 < y then x^1 <= x^y  </p>
      <p> If 0 = y then x^y = 1  </p>
      <p> If y < 0 then  x^y = 1/(x^(-y))</p>
<p>

Conclusion

x Each proof has a conclusion. This is the goal of the proof. The conclusion can be anywhere in the proof and is indicated by the tag c. Adding conclusions to our examples gives:

Property exp_pos:
<p>Let x and y be two integers, if 0 < x, to prove <c> 0 < x^y</c>, we have three cases:
      <p> If 0 < y  then <c>x^1 <= x^y</c></p>
      <p> If 0 = y  then <c>x^y = 1</c></p>
      <p> If y < 0  then <c>x^y = 1/(x^(-y))</c></p>
<p>

Hypothesis

Each proof can have an arbitrary number of hypothesis. These assumptions are indicated by the tag h. Refining furthermore our examples we have:

Property exp_pos:
<p> Let x and y be two integers, if <h>0 < x</h>, to prove <c>0 < x^y </c>, we have three cases:
      <p> If <h>0 < y</h>  then <c>x^1 <= x^y</c></p>
      <p> If <h>0 = y</h>  then <c>x^y = 1</c></p>
      <p> If <h>y < 0</h>  then <c>x^1 = 1/(x^(-y))</c></p>
<p>

Variables

Each proofs can also introduce new variables. Variables are indicated with the tag v. The text is either of the form name: type or of the form name. When the type is not given, it is the system that tries to infer the type.

Property exp_pos:
<p> Let <v>x</v> and <v>y</v> be two integers, if <h>0 < x</h>, to prove <c>0 < x^y</c>, we have three cases:
      <p> If <h>0 < y</h>  then <c>x^1 <= x^y</c></p>
      <p> If <h>0 = y</h>  then <c>x^y = 1</c></p>
      <p> If <h>y < 0</h>  then <c>x^y = 1/(x^(-y))</c></p> 
<p>

Names

Finally it is possible to associate a name to a proof with the tag n.

Property <n>exp_pos</n>:
<p> Let <v>x</v> and <v>y</v> be two integers, if <h>0 < x</h>, to prove <c>0 < x^y</c>, we have three cases:
      <p> If <h>0 < y</h>  then <c>x^1 <= x^y</c></p>
      <p> If <h>0 = y</h>  then <c>x^y = 1</c></p>
      <p> If <h>y < 0</h>  then <c>x^y = 1/(x^(-y))</c></p> 
<p>

Removing all the tags, we get the coloured proof:

Property exp_pos:
 Let x and y be two integers, if 0 < x , to prove 0 < x^y, we have three cases:
       If 0 < y   then x^1 <= x^y
       If 0 = y  then x^y = 1
       If 0 > y  then x^y = 1/(x^(-y))

Two extra tags have also be added for naming hypothesis and for justification

Named Hypothesis

It is possible to give a name to an assumption using the n for example

<h>0 < x <n>H</n></h>

As sometimes it is necessary to have some extra characters between the value of the hypothesis and its name, a special tag f allows to indicate the formula of an assumption so for example we have:

<h><f>0 < x 0</f> (<n>H</n>) </h>

Justification

In proofs, it is possible to give reference to others theorems or assumptions with the tag n For example a sentence like:

By theorems exp_inv and exp_rec, we have ...

can be coloured as

<j>By theorems <n>exp_inv<n> and  <n>exp_rec<n></j>, we have ...

Furthermore it also is possible to make reference to assumptions by value instead of by name using the tag f :

<j>By <f>A and B</f></j>, we have ...

How is the proof coloured?

To colour a proof, you first need to run the CYP program. In this example, we are using the Coq version of the CYP program. The interaction with CYP is done in a single window. Initially this window looks like:

For the moment the interface can only be used to colour the proof text. No editing is permitted. The first step is then to load the proof we want to colour using the Open File button:

Let us suppose we load the uncoloured version of our previous example

Now to colour the conclusion of the main proof, we first need it to select the text of the conclusion with the mouse, then we need to select the Set as conclusion menu.

The conclusion is now in blue, it has been coloured.

Colouring the whole like explained in the previous section gives the following result:

In the interface only proof tags are not coloured. As proofs can be nested, the colour of the main proof would hide the colours of the subproofs. For this reason. the interface only shows the immediate surrounding subproof of the current selection. For example, if we select the conclusion of the first subgoal we have:

Selecting the first variable of the main proof gives:

At any time, it is possible to get the tagged version of the proof, selecting the tab Tagged

Once a proof is completely coloured, it is possible to generate the output for a particular prover selecting the last tab (here the Coq output):

Any of this two formats can be saved on file:

In which order should the proof be coloured?

The interface does not privilege any particular way of colouring proofs. In practice, the bottom-up seems to work fairly well. In that case, the order in which the elements should be coloured is the following:

the names
the conclusions
the hypothesis and variables
the proof

How to try it?

It is simple, you just need to download the cyp.jar jar file and run it:

java -jar cyp.jar

Here are some examples. For more information on the command, read this.

What are the current developments?

Current version is 0.24 (api). We are currently working on

Improving the robustness (Error handling is shaky)
Increasing the number of types supported by the generator. Floating-point numbers is our first goal.
Generating output for other provers (for the moment only Coq (version v7 and v8) and Hol)
Accommodating proofs in languages like Arab, Japanese, ...

If you have other ideas, let us know.

Bugs

There are lots (CYP has not yet been formally proved), please send us your bug reports.

Credits

WHY is the main source of inspiration for CYP, instead of generating conditions for programs we do it for proofs. Why has also motivated us to build a system that is independent of a particular prover.

The current implementation of CYP is written in Java. We are happy user of the ANTLR tool.

Laurent Théry

Last modified: Tue Mar 22 13:47:55 CET 2005