LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on March 25 2016

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.


Previous meeting -- Next meeting