Ce devoir est à rendre sur le dépôt moodle avant le :
dimanche 12 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. N'hésitez pas à vous aider les uns les autres, mais
sans jamais vous montrer le code de la solution. 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.
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 plus dur.
introsunfoldexactsplitdestruct pour : un
/\, un
\/, une preuve de
False ou une preuve
par cas (sur les entiers naturels ou tout ou autre type inductif)
left/rightexfalsoreflexivityapply et
apply ... inrewrite,
rewrite <-,
rewrite ... in et
rewrite <- ... indiscriminateinductionspecializesimpl est autorisé et indispensable dans certains cas très faciles, mais
on est toujours content de s'en passer
add_0_l : ∀ n : nat, 0 + n = nadd_0_r : ∀ n : nat, n + 0 = nadd_1_l : ∀ n : nat, 1 + n = S nadd_1_r : ∀ n : nat, n + 1 = S nadd_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 + nadd_assoc : ∀ n m p : nat, n + (m + p) = (n + m) + p
On considère un type
clock avec seulement deux valeurs distinctes:
tic
et
tac:
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.
Après tic, c'est tac, après tac, c'est tic.
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.
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 = cc + 1 = next cc + 2 = next (next c)
On s'intéresse maintenant à la parité des entiers. On crée un nouveau type à deux éléments :
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 :
Pour énoncer des résultats sur la parité des entiers, on définit l'opération
autre :
Maintenant que les lemmes évidents sur
autre sont prouvés, on peut
s'attaquer aux résultats intéressants sur
parité et
next_iter.