Commit 788a8a8a authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

parentheses

parent 2b44811a
......@@ -94,7 +94,7 @@ Si les preuves que contient ce fichier sont correctes, un fichier compilé `mes
* Pour `True` (rarement utilisé en Coq), l'introduction peut se faire via `constructor`, par contre il n'y a rien à éliminer.
- Abbréviations:
* Une négation `~A` n'est qu'une abbréviation pour `A->False`. Donc introduction via `intro` (ou `intros a`, mettre un nom pour forcer l'introduction), et élimination via `apply H` ou `destruct H` (selon qu'on s'intéresse au `->` ou au `False` sous-jacent).
* Une équivalence `A<->B` n'est qu'une abbréviation pour `A->B/\B->A`, donc se manipule comme une conjonction.
* Une équivalence `A<->B` n'est qu'une abbréviation pour `(A->B)/\(B->A)`, donc se manipule comme une conjonction.
- Quelques premières tactiques automatiques : `trivial`, `easy`, `auto`, `eauto`, `intuition`, `firstorder`. Voir la documentation de Coq pour plus d'information. S'entraîner tout d'abord à savoir faire sans ces tactiques. En effet, si les dernières tactiques de la liste peuvent résoudre les exercices ci-dessous, elles n'aident pas forcément tant que cela sur des preuves plus délicates, et il pourra être utile alors de savoir procéder par petits pas.
### Exercice 1 : Calcul propositionnel ###
......
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