Langages et Traducteurs – Planning
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 Rocq
Bonne pratique :
- indiquer l'idée de la la preuve papier a priori
- dérouler en Rocq
- reformuler la preuve papier a posteriori
4.1.2 Révision rapide sur simpl_rec, 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 -> coul_suiv c = Vert.
D'autre part : Definition c := Rouge. Lemma lulu2 : coul_suiv c = Vert.
Voire Lemma lulu2' : let x := Rouge in coul_suiv 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 coul_suiv vue dans le fichier rocq B A BA du cours 2. Voici le code en mode interactif, incluant une nouvelle tactique : refine
4.3 Retour sur les égalités
4.4 Initiation aux arbres de preuve
5
∼∼∼
Made with Org mode