Next:Expressions, parsing and pretty Up:Examples Previous:How to read the Contents

An example in analysis

The example given below is a typical small standalone proof (using no library).

We prove that two definitions of the continuity of a function are equivalent. We give only one of the directions, the other is similar. We have written it in a rather elaborate way in order to show the possibilities of the system.

We define the sort of reals.
>PhoX> Sort real.
Sort is the name of the command used to create new sorts, but you can also use it to give name to existing sorts.
We give a symbol for the distance and the real 0 (denoted by ) as well as predicates for inequalities.
>PhoX> Cst d : real -> real -> real.
>PhoX> Cst R0 : real.
>PhoX> Cst Infix[5] x "<=" y : real -> real -> prop.
>PhoX> Cst Infix[5] x "<" y : real -> real -> prop.
>PhoX> def Infix[5] x ">" y = y < x.
>PhoX> def Infix[5] x ">=" y = y <= x.
The command Cst introduces new constants of given sorts while def is used to give definitions. The commands to define inequalities are quite complex, because we want to use some infix notation with a specific priority.
Here are the two definitions of the continuity:
>PhoX> def continue1 f x =
$\forall e{>}R0 \,\exists a{>}R0 \,\forall y (\hbox{d}\,x\,y < a \rightarrow \hbox{d} (f x) (f y) < e)$ .
>PhoX> def continue2 f x =
$\forall e{>}R0 \,\exists a{>}R0 \,\forall y (\hbox{d}\,x\,y \leq a \rightarrow \hbox{d} (f x) (f y) \leq e)$ .
and the lemmas needed for the proof.
>PhoX> claim lemme1 $\forall x,y (x < y \rightarrow x \leq y)$ .
>PhoX> claim lemme2 $\forall x{>}R0 \,\exists y{>}R0 \forall z (z \leq y \rightarrow z < x)$ .
The command claim allows to introduce new axioms (or lemmas that you do not want to prove now. You can prove them later using the command prove_claim). Beware that there may be a contradiction in your axioms!
We begin the proof using the command goal:
>PhoX> goal $\forall x,f (\hbox{continue1} \, f \, x \rightarrow \hbox{continue2} \, f \, x)$ .
goal 1/1
|- $\forall x,f (\hbox{continue1} \, f \, x \rightarrow \hbox{continue2} f x)$
We start with some ``introductions''.
%PhoX% intro 5.
goal 1/1
H :=
H0 :=
|-
An ``introduction'' for a given connective, is the natural way to establish the truth of that connective without using other fact or hypothesis. For instance, to prove $A \to B$ , we assume and prove . Here, PhoX did five introductions:
- one for $\forall x$ and one for $\forall f$ ,
- one for the implication $(\hbox{continue1} \, f \, x \rightarrow \hbox{continue2} f x)$ ,
- one for the $\forall e$ inside the definition of $\hbox{continue2}$
- and finally, one for the hypothesis .
Therefore, PhoX created three new objects: and two new hypothesis named H0 and H1.
We use the continuity of with , and we remove the hypotheses H and H0 which will not be used anymore.
%PhoX% apply H with H0. rmh H H0.
goal 1/1
G := $\exists a{>}R0 \,\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
|- $\exists a{>}R0 \,\forall y (\hbox{d}\,x\,y \leq a \to \hbox{d} (f x) (f y) \leq e)$
The apply command is quite intuitive to use. But it is a complex command, performing unification (more precisely higher-order unification) to guess the value of some variables. Sometimes you do not get the result you expected and you need to add extra information in the proper order.
We de-structure hypothesis G by indicating that we want to consider all the $\exists$ and all the conjunctions (You can also use lefts G twice with no more indication).
%PhoX% lefts G $ $\exists$ $ $\land$ .
goal 1/1
H :=
H0 := $\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
|- $\exists a_0{>}R0 \,\forall y (\hbox{d}\,x\,y \leq a_0 \to \hbox{d} (f x) (f y) \leq e)$
The left and lefts are introductions for an hypothesis: that is the way to use an hypothesis in a ``standalone'' way (not using the conclusion you want to prove or other hypothesis).
We need to write a ``$'' prefix, because $\exists$ and $\lor$ have a prefix syntax and need other informations. The ``$'' prefix tells that you just want this symbol and nothing more.
We use the second lemma with H and we remove it.
%PhoX% apply lemme2 with H. rmh H.
goal 1/1
H0 := $\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
G := $\exists y{>}R0 \, \forall z{\leq}y \; z < a$
|- $\exists a_0{>}R0 \,\forall y (\hbox{d}\,x\,y \leq a_0 \to \hbox{d} (f x) (f y) \leq e)$
We de-structure again G and we rename the variable created.
%PhoX% lefts G $ $\exists$ $ $\land$ . rename y a'.
goal 1/1
H0 := $\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
H1 :=
H2 := $\forall z{\leq}a' \; z < a$
|- $\exists a_0{>}R0 \,\forall y (\hbox{d}\,x\,y \leq a_0 \to \hbox{d} (f x) (f y) \leq e)$
Now we know what is the we are looking for. We do the necessary introductions for $\forall$ , $\exists$ , conjunctions and implications (again, you could use intros several times with no more indication). Two goals are created, as well as an existential variable (denoted by ?1) for which we have to find a value.
%PhoX% intros $ $\forall$ $ $\exists$ $ $\land$ $ $\to$ .
goal 1/2
H0 := $\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
H1 :=
H2 := $\exists z{\leq}a' \; z < a$
|- $\hbox{?1} > R0$
goal 2/2
H0 := $\forall y (\hbox{d}\,x\,y < a \to \hbox{d} (f x) (f y) < e)$
H1 :=
H2 := $\forall z{\leq}a' \; z < a$
H3 := $\hbox{d}\,x\,y \leq \hbox{?1}$
|- $\hbox{d} (f x) (f y) \leq e$
The first goal is solved with the hypothesis H1 indicating this way that ?1 is . The second is automatically solved by PhoX by using lemma1, and this finishes the proof.
%PhoX% axiom H1. auto +lemme1.

Remark. Instead of the command auto +lemme1 one could also say elim lemme1.elim H0. axiom H3. or apply H0 with H3. elim lemme1 with G. where G is an hypothesis produced by the first command. We could also give the value of the existential variable by typing instance ?1 a'.

A good exercise for the reader consists in understanding what these commands do. The appendix A should help you !

Next:Expressions, parsing and pretty Up:Examples Previous:How to read the Contents

Christophe Raffalli 2005-03-02