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(arg1, ..., argn).
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(term1, ..., termn),
- 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