Table of Contents
LANGAGES ET TRADUCTEURS – Planning Jean-François Monin, 2021
3 Cours 3
Preuves par cas, récurrence structurelle Illustration sur B A BA
4 Cours 4
4.1 Questions concrètes issues du TD2
4.1.1 Récurrences meilleures avec Coq
Bonne pratique :
- indiquer l'idée de la la preuve papier a priori
- dérouler en Coq
- reformuler la preuve papier a posteriori
4.1.2 Révision rapide sur simplrec, simpl0 :
répartition des tâches, diviser pour régner
4.1.3 Utiliser eval dans simpl0 ?
–> pas assez général pour des expressions dépendant d'un état.
4.1.4 Quand utiliser cbn ? Quand utiliser rewrite ?
Quelle différence entre
D'une part : Lemma lulu1 : c = Rouge -> coulsuiv c = Vert.
D'autre part : Definition c := Rouge. Lemma lulu2 : coulsuiv c = Vert.
Voire Lemma lulu2' : let x := Rouge in coulsuiv x = Vert.
Une égalité en hypothèse (ou démontrée ailleurs) est en général entre deux expressions quelconques. Une définition est entre un nom et une expression.
On y revient ci-dessous.
4.2 Démo surprise
Développement pas à pas de la fonction coulsuiv vue dans le fichier coq B A BA du cours 2. Voici le code en mode interactif, incluant une nouvelle tactique : refine