Personnes présentes
- Frédéric Boulanger
- Chantal Keller
- Yakoub Nemouchi
- Safouan Taha
- Frédéric Tuong
- Burkhart Wolff
Preuve avec double induction
Safouan TAHA
Safouan présente un début de formalisation en Isabelle des patrons de propriétés temporelles. Il s'agit d'une sémantique dénotationnelle basée sur des traces finis.
Une des primitives formalisées subchain prend en paramètre :
- une trace : une liste finie d'états
- une liste de propriétés : une propriété est une fonction booléenne sur l'ensemble des états
et vérifie si les propriétés sont vérifiées par les états de la trace dans l'ordre. Les états vérifiant les propriétés ne sont pas nécessairement contigus et un seul état peut vérifier à lui seul une sous-séquence de la liste de propriétés.
fun subchain :: "'state list ⇒ ('state ⇒ bool) list ⇒ bool"
where
"subchain _ [] = True"
| "subchain [] (φ#φl) = False"
| "subchain (ε#ξ) (φ#φl) = (if (φ ε)
then subchain (ε#ξ) φl
else subchain ξ (φ#φl))"
Un lemme qui semble trivial est:
lemma "subchain ξ (φ#φl) ⟶ subchain ξ φl" apply(induct ξ, simp) apply(rule impI, simp) apply(case_tac "φ a", simp_all) apply(thin_tac "subchain ξ (φ # φl)", thin_tac "¬ φ a") oops
en entamant la preuve par induction de ce lemme, on découvre qu'on a besoin d'un lemme dual tout aussi trivial:
lemma "subchain ξ φl ⟶ subchain (ε#ξ) φl"
sauf que la preuve de ce lemme nécessite à son tour le premier lemme. les deux lemmes sont inter-dépendants. Il faudra prouver les deux en même temps. D'où le lemme:
lemma "(subchain ξ (φ#φl) ⟶ subchain ξ φl) ∧ (subchain ξ φl ⟶ subchain (ε#ξ) φl)"
De nouveau la preuve par induction sur une des deux listes ξ ou φl n'aboutit pas à l'hypothèse d'induction. On a besoin d'une double induction (proposée par Chantal) sur la somme des longueurs des deux listes:
lemma "n = length ξ + length φl ⟶ ((subchain ξ (φ#φl) ⟶ subchain ξ φl)
∧ (subchain ξ φl ⟶ subchain (ε#ξ) φl))"
sous cette forme la preuve aboutie.
En exercice une seconde formalisation de subchain est discutée:
function subchain_v2 :: "'state list ⇒ ('state ⇒ bool) list ⇒ bool"
where
"subchain_v2 _ [] = True"
| "subchain_v2 [] (φ#φl) = False"
| "subchain_v2 (ε#ξ) (φ#φl) = (if (φ ε)
then subchain_v2 ξ (dropWhile (λ φ. φ ε) φl)
else subchain_v2 (dropWhile (λ ε. ¬ φ ε) ξ) φl)"
apply(simp_all)
apply(case_tac x, simp, case_tac b, simp, case_tac a, simp_all)
done
termination
apply(relation "measure (λ(a,b). length a)")
apply(simp_all)
apply(simp add: le_imp_less_Suc length_dropWhile_le)
done
Il reste à prouver le lemme suivant:
lemma "subchain ξ φl = subchain_v2 ξ φl"