Commit b6eb197a authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td1 english

parent 9e407525
TD1 : First proofs in Coq
=========================
M2 LMFI
Pierre Letouzey (from A. Miquel)
> Online documentation : http://coq.inria.fr/doc/
### Revision : launching Coq ###
There are several ways to use Coq:
* via `coqide`, a graphical interface based on `gtk`
* via `proofgeneral`, which is a plugin for `emacs`
* directly in a browser via `jsCoq`, for instance https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html
(see https://github.com/ejgallego/jscoq for usage instructions)
* or perhaps via `coqtop`, a read-eval-print loop (repl) which is quite bare, similar to the `ocaml` interactive loop.
Each method has its advocates (even the last one...).
The coq source files are always named with `.v` as extension (for "vernacular"...).
After launch, both `coqide` and `proofgeneral` and `jsCoq` provide interfaces with a similar layout : the file being edited is in the left half of the screen, while proofs in progress are in right top and system messages are in right bottom (Coq answers, error messages, etc). In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.
### Revision : Coq commands ###
In Coq, a command is a command name (starting with an uppercase letter), followed by some arguments, and ended by a dot. Examples:
```coq
Check 0.
Check S.
Check nat.
Print nat.
Search nat.
Check 2 + 2 = 5.
Check forall x, exists y, x = 2 * y \/ x = 2 * y + 1.
Definition id := fun (A : Set) (x : A) => x.
Check id.
Check id nat 7.
```
If you haven't yet, try typing some of these commands and submit them to Coq by using one of the navigation possibilities (icons, menu item or keyboard shurtcuts). Observe the advance of the colored zone indicating the part of the file already executed.
### Entering the proof mode ###
The user indicates (s)he wants to start a proof with a command such as :
```coq
Lemma and_commut :
forall A B : Prop, A /\ B <-> B /\ A.
```
This command give a name (here `and_commut`) to the lemma, this will allow later to refer to this lemma later. Instead of `Lemma`, one can use similar keywords such as `Theorem` or `Proposition` or `Fact`. After that, the command `Proof.` is to be used to mark the actual beginning of the proof itself (actually not mandatory but strongly recommanded).
### Subgoals and tactics ###
When a proof is started, the proof mode of Coq will display in the higher right part one or several **subgoals** that are to be proved separately, one by one. These subgoals are essentially sequents of the natural deduction logic, written vertically : the (named) hypothesis comes first on top
and the conclusion is below the bar. In the upper part one can also find the variable declarations.
The proof is to be done by **tactics**, that are orders given by the user to progress in the proof of the current goal, by transforming this goal in various ways. Tactics have lowercase names. For instance, the `intro` tactic performed on a goal of the form `A -> B` will introduce an hypothesis `H : A` in the context, and replace the conclusion by `B`. Each inference rule of the natural deduction logic will correspond to one tactic (or more), but some tactics allow to perform more advanced proof steps, for instance solving linear inequalities in the Presburger arithmetic (tactic `lia`).
Each tactic may generate several subgoals (corresponding to premises of the underlying logical rule), or on the contrary it may completely solve the current goal and hence remove it. The proof is finished when all subgoals are proved. In this case, the command `Qed` is to be used (from *Quod erat demonstrandum*) to conclude the proof and leave the proof mode. Here comes a possible complete proof for the previous statement:
```coq
Lemma and_commut :
forall A B : Prop, A /\ B <-> B /\ A.
Proof.
intros. split.
- intros. destruct H. split. assumption. assumption.
- intros. destruct H. split; assumption.
Qed.
```
When tactics are separated by dots, Coq will execute them steps-by-steps. One can also use semi-colon `;` to **chain** tactics : the second tactic is applied to all subgoals resulting from the first tactic on the current goal, and so forth. For instance, `split;assumption` applies `assumption` on the two subgoals created by `split`.
Before a tactic, one may optionally write a **bullet**, i.e. one of the character `-` or `+` or `*`. These bullets help organizing the proof in a hierarchical way, with delimitation of each sub-part (enforced by Coq).
Such a *proof script* is to be saved in a file with a `.v` extension, for instance `myproofs.v`. Then it can be *compiled* via the unix command `coqc myproofs.v`. If the content of this file is correct, then a binary file `myproofs.vo` is produced, allowing later a fast reload of our proofs (via the `Require Import` command).
### Some elementary tactics ###
- `assumption` if the current goal is exactly one of the hypothesis (cf. the *axiom rule* in logic).
- For all primitive connectors (quantification `∀`, implication `->`):
* introduction via `intro` (or one of its variants `intros`, `intro x`, `intros x y ...`)
* elimination via `apply H` (where `H` is the name of the hypothesis to eliminate).
- The other connectors (which are actually inductive definitions) may ideally be introduced by `constructor` and eliminated by `destruct H`.
But the introduction frequently requires more ad-hoc tactics:
* `split` for a conjunction `/\`
* `left` and `right` for a disjunction `\/`
* `exists ...` for a quantification `` (where `...` is the place where the existential witness is given)
* No introduction tactic for `False` !
* For `True` (seldom used in Coq), the introduction can be done via `constructor`, but nothing to eliminate.
- Some abbreviations:
* A negation `~A` is just a shortcut for `A->False`. Hence introduction via `intro` (or `intros a`, giving a name forces the introduction) and elimination via `apply H` or `destruct H` (whether one wants to focus on the underlying `->` or `False`).
* An equivalence `A<->B` is just a shortcut for `(A->B)/\(B->A)`, hence is manipulated as a conjunction of implications.
- Some automatic tactics : `trivial`, `easy`, `auto`, `eauto`, `intuition`, `firstorder`. See the Coq documentation for more details. Try first to finish the following proofs with no or little automatisation, then experiment with these tactics in a second time. Indeed, it can be helpful later to known how to proceed steps-by-steps, since real-life proofs are seldom doable by just automatic tactics.
### Exercise 1 : Propositional calculus ###
Assume some propositional variables `A` and `B` and `C` via the command:
```coq
Parameters A B C : Prop.
```
Then prove in Coq the following statements :
```coq
Lemma E1F1 : A -> A.
Lemma E1F2 : (A -> B) -> (B -> C) -> A -> C.
Lemma E1F3 : A /\ B <-> B /\ A.
Lemma E1F4 : A \/ B <-> B \/ A.
Lemma E1F5 : (A /\ B) /\ C <-> A /\ (B /\ C).
Lemma E1F6 : (A \/ B) \/ C <-> A \/ (B \/ C).
Lemma E1F7 : A -> ~~A.
Lemma E1F8 : (A -> B) -> ~B -> ~A.
Lemma E1F9 : ~~(A \/ ~A).
```
### Exercise 2 : Predicate calculus ###
First perform the following declarations :
```coq
Parameter X Y : Set.
Parameter P Q : X -> Prop.
Parameter R : X -> Y -> Prop.
```
Then prove in Coq the following statements :
```coq
Lemma E2F1 : (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).
Lemma E2F2 : (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Lemma E2F3 : (exists y, forall x, R x y) -> forall x, exists y, R x y.
```
### Exercise 3 : Formalizing ###
State in Coq and prove some of the questions in this [logical exercises](https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td1.pdf). For simulating the reasoning "by absurdum", you can declare the following axiom:
```
Axiom not_not_elim : forall A : Prop, ~~A -> A.
```
......@@ -52,7 +52,7 @@ On notera que cette commande donne un nom (ici: `and_commut`) au lemme, ce qui p
### Sous-buts et tactiques ###
Une fois le mode preuve lancé, la zone supérieure gauche affiche en permanence un ou plusieurs sous-buts (**subgoals**) qu'il s'agit de démontrer. Ces sous-buts sont essentiellement des séquents de la déduction naturelle écrits verticalement: les hypothèses (nommées) sont en haut, et la conclusion figure en bas sous un trait. Dans la partie haute figurent également des déclarations de variables.
Une fois le mode preuve lancé, la zone supérieure droite affiche en permanence un ou plusieurs sous-buts (**subgoals**) qu'il s'agit de démontrer. Ces sous-buts sont essentiellement des séquents de la déduction naturelle écrits verticalement: les hypothèses (nommées) sont en haut, et la conclusion figure en bas sous un trait. Dans la partie haute figurent également des déclarations de variables.
La preuve se fait à l'aide de **tactiques** (distinguées des commandes par une minuscule initiale), qui effectuent des transformations plus ou moins complexes sur le but courant.
Par exemple, la tactique `intro` effectuée sur un but de la forme `A -> B` introduit une hypothèse `H : A` dans le contexte, et remplace la conclusion par `B`. À chaque règle d'inférence de la déduction naturelle correspond une ou plusieurs tactiques, mais certaines tactiques permettent également d'effectuer des morceaux de preuve plus complexes, comme par exemple la résolution de contraintes linéaires en arithmétique de Presburger (tactique `omega`).
......@@ -121,13 +121,13 @@ Lemma E1F9 : ~~(A \/ ~A).
Après avoir effectué les déclarations suivantes:
```
Parameter X Y : Set.
Parameter A B : X -> Prop.
Parameter P Q : X -> Prop.
Parameter R : X -> Y -> Prop.
```
Prouver en Coq les formules suivantes:
```
Lemma E2F1 : (forall x, A x /\ B x) <-> (forall x, A x) /\ (forall x, B x).
Lemma E2F2 : (exists x, A x \/ B x) <-> (exists x, A x) \/ (exists x, B x).
Lemma E2F1 : (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).
Lemma E2F2 : (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Lemma E2F3 : (exists y, forall x, R x y) -> forall x, exists y, R x y.
```
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment