Table of Contents
LANGAGES ET TRADUCTEURS – Chapitre 5 Jean-François Monin, 2021
Relations inductives
1 Présentations
1.1 Sous forme de règles
prémisse 1 prémisse 2 ... prémisses
------------------------------------------- nom
conclusion
rel a1 b1 c1 rel a2 b2 c2 ...
------------------------------------------- regle0
rel a b c
1.2 Sous forme d'un type inductif Coq
Inductive rel : A -> B -> C -> Prop := | regle0 : forall..., rel a1 b1 c1 -> rel a2 b2 c2 -> rel a b c | regle1 :
2 Technique à exercer d'abord sur un exemple très simple
2.1 Le prédicat even, défini par deux règles :
--------- E0 even 0 even n ------------ E2 n even (2 + n)
2.2 Définition inductive en Coq avec deux constructeurs
Inductive even : nat -> Prop := | E0 : even 0 | E2 : ∀n, even n -> even (2 + n) .
Par exemple, E2 4 permet de conclure even 6 à partir d'une preuve de even 4, Un arbre de preuve complet de even 6 au moyen de E0 et E2 sera :
------ E0 even 0 ------ E2 0 even 2 ------ E2 2 even 4 ------ E2 4 even 6
Écriture linéaire de cet arbre de preuve : E2 4 (E2 2 (E2 0 E0))
2.3 Exemples de théorème
Theorem even_plus : ∀ n m, even n -> even m -> even (n + m).
3 Technique centrale
On raisonnera par récurrence structurelle sur les arbres de preuve