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.
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
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
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 = c
c + 1 = next c
c + 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
.