Personnes présentes
- Chantal Keller
- Safouan Taha
- Burkhart Wolff
- Lina Ye
Preuve avec double induction
Safouan TAHA
Safouan nous montre sa progression depuis la réunion précédente. Quelques questions :
- Peut-on rendre plus concises les utilisations de erule_tac ?
- Style de preuve faisant beaucoup appel à
apply, on peut améliorer en utilisant Isar bleu, par exemple :
proof(induction ...)
print_cases
case 0 fix ... show ?case (* Au lieu de [?case], on pourrait rappeler le sous-but *)
by simp ...
next
case (Suc n) show ?case (* Mettre [Suc n] permet de fixer le [n] *)
term ?case (* Affiche le sous-but *)
proof (...)
print_cases
case Nil fix ... assume ... and ... show ...
...
- Utilisation de thin_tac avec des lieurs (comme le "for all") : difficile de matcher à cause des liaisons, on ne peut remplacer par
_que les parties ne faisant pas intervenir les variables liées.