From Coq Require Import Arith.PeanoNat.
Import Nat(add_0_l, add_0_r, add_succ_l, add_succ_r, add_comm, add_assoc).

Consignes

Ce devoir est à rendre sur le dépôt moodle avant le : dimanche 13 octobre à 23h59
Vous rendrez un seul fichier appelé DevoirOctobre1.v et complèterez la déclaration suivante ci-dessous :
NOM, prénom, numéro étudiant : Je déclare qu'il s'agit de mon propre travail et que ce travail a été intégralement réalisé par un être humain.
C'est un travail individuel. Vous pouvez vous aider les uns les autres mais vous ne devez jamais vous montrer le code de votre solution. L'usage de ChatGPT ou de toute autre intelligence artificielle pour résoudre les exercices est interdit (vous pouvez à la limite lui poser des questions sur des points mal compris). Si vous avez des questions (autres que "comment résoudre cet exercice"), vous pouvez les poser (en anglais) sur : https://coq.zulipchat.com/ dans le "stream" Coq Users (nécessite une inscription avec une adresse mail). Il est possible aussi d'envoyer des mails à rousselin@univ-paris13.fr.
Le premier but de ce devoir est de vous faire progresser en mathématiques et en informatique. Le deuxième est que tous les étudiants soient bien à jour dans la progression.
Il y a 2 parties inégales et indépendentes.
  • Partie 1 : calcul des propositions. Cette partie revient sur le contenu du premier TP pour s'assurer que vous avez des bases suffisantes en logique.
  • Partie 2 : sur un type clock à deux valeurs, on s'amuse à faire tic-tac-tic-tac..., ceci permet de revenir sur la partie calculatoire de Coq (discriminate et simpl) et l'induction. Les entiers naturels ramènent leur fraise à la fin, avec un dernier exercice dur.
Il n'est pas nécessaire de traiter tous les exercices pour avoir une bonne note. Vous pouvez toujours admettre un théorème pour l'utiliser plus tard dans le devoir.
La difficulté des exercices est notée entre 0 et 50 selon la même gradation que Donald Knuth dans The Art of Computer Programming. 00 : immédiat 10 : simple (quelques minutes, ou alors vous avez raté une information) 20 : moyennement difficile (entre 15 et 30 minutes) 30 : assez difficile (à faire à la fin si tout est bien compris) 40 : projet (plusieurs heures de travail et des initiatives à prendre) 50 : problème de recherche, non encore résolu
Bien sûr, la difficulté est une notion assez subjective... Essayez d'avoir des jolies preuves courtes et structurées.
Vous utiliserez les tactiques :
  • intros
  • unfold
  • exact
  • split
  • destruct pour : un ∧, un ∨, une preuve de False ou une preuve par cas (sur les entiers naturels ou tout ou autre type inductif)
  • left/right
  • exfalso
  • reflexivity
  • apply et apply ... in
  • rewrite, rewrite <-, rewrite ... in et rewrite <- ... in
  • discriminate
  • induction
  • specialize
  • simpl est autorisé et indispensable dans certains cas très faciles, mais on est toujours content de s'en passer
Pour la partie 2, vous pouvez utiliser les lemmes suivants:
  • add_0_l : ∀ n : nat, 0 + n = n
  • add_0_r : ∀ n : nat, n + 0 = n
  • add_1_l : ∀ n : nat, 1 + n = S n
  • add_1_r : ∀ n : nat, n + 1 = S n
  • add_succ_l : ∀ n m : nat, S n + m = S (n + m)
  • add_succ_r : ∀ n m : nat, n + S m = S (n + m)
  • add_comm : ∀ n m : nat, n + m = m + n
  • add_assoc : ∀ n m p : nat, n + (m + p) = (n + m) + p

Partie 1 : logique de base


Section LogiqueBase.

Exercice : Prouver le théorème suivant, difficulté 05.

Theorem P1_ex1 : ∀ (P Q R : Prop), (P → Q) → (Q → R) → (P → R).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Theorem P1_ex2 : ∀ (P Q : Prop), ~(P ∨ Q) ↔ ¬P ∧ ¬Q.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Theorem P1_ex3 : ∀ (P Q : Prop), ¬P ∨ ¬Q → ~(P ∧ Q).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Theorem P1_ex4 : ∀ (P : Prop), (((P ∨ ¬P) → False) ↔ False).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

End LogiqueBase.

Partie 2 : tic, tac


Section TicTac.

On considère un type clock avec seulement deux valeurs distinctes: tic et tac:

Inductive clock :=
| tic : clock
| tac : clock.

C'est un type à deux constructeurs tout comme nat mais il n'y a ici aucune auto-référence, donc il y a seulement deux valeurs. On peut utiliser discriminate pour réfuter une égalité entre constructeurs distincts et destruct c pour faire une preuve par disjonction de cas sur une variable c de type clock.

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma tic_not_tac : ~(tic = tac).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma tic_or_tac : ∀ (c : clock), c = tic ∨ c = tac.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Après tic, c'est tac, après tac, c'est tic.
Definition (c : clock) :=
match c with
| tic ⇒ tac
| tac ⇒ tic
end.

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma next_tic : next tic = tac.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma next_tac : next tac = tic.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma next_involutive : ∀ (c : clock), next (next c) = c.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Maintenant, on itère l'opération next, intuitivement next_iter c n = next (next (next ... c)), où l'opération next est répétée n fois.
Fixpoint next_iter (c : clock) (n : nat) :=
match n with
| 0 ⇒ c
| (S p) ⇒ next (next_iter c p)
end.

On va utiliser la notation c + n, où c vaut tic ou tac et n est un entier à la place de next_iter c n. Par exemple, on a
  • c + 0 = c
  • c + 1 = next c
  • c + 2 = next (next c)
Notation "c + n" := (next_iter c n).

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma next_iter_0 (c : clock) : c + 0 = c.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma next_iter_succ (c : clock) (n : nat) :
  c + (S n) = next (c + n).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 20.

Lemma next_iter_assoc (c : clock) (n m : nat) :
  (c + n) + m = c + (n + m).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On s'intéresse maintenant à la parité des entiers. On crée un nouveau type à deux éléments :

Inductive pair_ou_impair :=
| pair : pair_ou_impair
| impair : pair_ou_impair.

Tout ce qui a été dit sur le type clock est évidemment encore vrai sur pair_ou_impair.
On calcule maintenant par récurrence la parité d'un entier naturel n :
  • la parité de 0 est "pair"
  • la parité de 1 est "impair"
  • la parité de n + 2 est la même que la parité de n.

Fixpoint parité (n : nat) :=
match n with
| 0 ⇒ pair
| 1 ⇒ impair
| S (S p) ⇒ parité p
end.

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma parité_0 : parité 0 = pair.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma parité_1 : parité 1 = impair.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma parité_succ_succ (n : nat) : parité (S (S n)) = parité n.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Pour énoncer des résultats sur la parité des entiers, on définit l'opération autre :
Definition autre (e : pair_ou_impair) :=
match e with
| pair ⇒ impair
| impair ⇒ pair
end.

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma autre_pair : autre pair = impair.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 05.

Lemma autre_impair : autre impair = pair.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma autre_involutive (e : pair_ou_impair) : autre (autre e) = e.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma autre_eq (e f : pair_ou_impair) : autre e = f → e = autre f.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Maintenant que les lemmes évidents sur autre sont prouvés, on peut s'attaquer aux résultats intéressants sur parité et next_iter.

Exercice : Prouver le théorème suivant, difficulté 20.

Lemma parité_succ (n : nat) : parité (S n) = autre (parité n).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 30.

Lemma next_iter_even (c : clock) (n : nat) :
  (parité n = pair → c + n = c) ∧ (parité n = impair → c + n = next c).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

End TicTac.