Pcoq beginner tutorial, step 5

We shall now perform the proof of this silly theorem. The first step, is to assume the existence of x, y, and z and assume that x is smaller than y and that z is greater than y. All this reasoning step can be done in one step of proof-by-pointing, by simply clicking with the right button on the expression x < z that appears in the middle part of the pcoq window. As a result the pcoq window should look as follows:

You can now click on Do it to execute the commands that has been generated by the proof-by-pointing operation. The contents of the pcoq window middle part is updated to receive a new goal, where the statement to prove is displayed on top (x < z) and assumptions are displayed below an horizontal line, see the following figure.

Click here to proceed

---

Yves Bertot

Last modified: Tue Feb 1 13:25:24 MET 2000