Commit 2b44811a authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

listes de tactiques de base

parent 07797e4f
......@@ -79,6 +79,24 @@ Un tel *script de preuve*, une fois sauvé dans un fichier tel que `mes_preuves.
ensuite être *compilé* via la commande unix `coqc mes_preuves.v`.
Si les preuves que contient ce fichier sont correctes, un fichier compilé `mes_preuves.vo` est alors produit, qui permettra de recharger ces preuves rapidement par la suite (cf. la commande `Require Import`).
### Premières tactiques élémentaires ###
- `assumption` si le but à prouver est déjà en hypothèse (cf. la *règle axiome* en logique).
- Pour les opérateurs primitifs (quantification `∀`, implication `->`):
* introduction via `intro` (ou ses variantes `intros`, `intro x`, `intros x y ...`)
* élimination via `apply H` (si `H` est le nom de l'hypothèse à éliminer)
- Pour les autres opérateurs (qui sont en fait des définitions inductives), en théorie on introduit avec `constructor` et on élimine avec `destruct H`.
Mais l'introduction nécessite souvent des tactiques dédiées:
* `split` pour une conjonction `/\`
* `left` et `right` pour une disjonction `\/`
* `exists ...` pour une quantification `` (et les `...` doivent donner le témoin)
* Aucune tactique d'introduction pour `False` !
* 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.
- 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 ###
Poser l'existence de variables propositionnelles `A`, `B` et `C` via la commande:
......
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