Travaux dirigés pour le 31 janvier 2012

Le but de cette séance est d'apprendre à faire des preuves en Coq.

Questions à faire en classe

Ecrire des preuves pour les formules logiques suivantes:

• forall a:Prop, a -> a
• forall a b:Prop, a /\ b -> a
• forall a:Prop, a -> a /\ 3 + 1 = 2 + 2
• forall a b:Prop, a -> (a \/ b) \/ (b /\ b)
• forall P Q : nat -> Prop, (forall x, P x /\ Q x) -> exists x, P x
• forall a b c d:Prop, a /\ b -> (a->c) /\ (b->d) -> c/\d
• forall A:Type, forall P Q: A -> Prop, (forall y:A, P y -> Q y) -> (exists x: A, P x) -> exists z:A, Q z
• forall a, ~ (a /\ ~ a)
• forall a b c : Prop, (a -> b -> a -> c) -> a -> b -> c
• forall f g : nat -> nat, (forall x , f x = g (g x)) -> f (f 1) = g (f (g 1))

Quelques exemples et outils

• Pour commencer une preuve, il faut taper Lemma nom : énoncé. Le mot nom est le nom que l'on associera au résultat prouvé dès qu'il sera prouvé, La formule logique énoncé est celle que l'on veut prouver.

  On applique ensuite des tactiques qui sont de la forme suivante: intros nom1 nom2 ...; apply nom; split; left; right; exists formule; change formule with formule; assert formule; revert nom; exact formule; assumption; destruct formule as [ nom1 nom2]; destruct formule as [nom1 | nom2], rewrite formule, rewrite <- formule.

  Quand il ne reste plus de buts à prouver, on termine la preuve par la commande Qed.