[inria-00407778, v1] An Ssreflect Tutorial

INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUEAn Ssreflect TutorialGeorges Gonthier — Stéphane Le RouxN° 367July 2009Thème SYMapport technique inria-00407778, version 1 - 28 Jul 2009ISSN 0249-0803 ISRN INRIA/RT--367--FR+ENGinria-00407778, version 1 - 28 Jul 2009°An Ssreflect Tutorial∗ †Georges Gonthier , St´ephane Le RouxTh`eme SYM — Syst`emes symboliques´Equipes-Projets Composants Math´ematiques, Centre Commun INRIA Microsoft ResearchRapport technique n 367 — July 2009 — 30 pagesAbstract: This document is a tutorial for ssreflect which is a proof language based on Coq. Thistutorial is mostly dedicated to people who already know the basics of logic.Key-words: proof assistants, formal proofs, Coq, small scale reflection, tactics.∗ Microsoft Research, Cambridge, R-U, Centre commun INRIA Microsoft Research† Centre commun INRIA Microsoft ResearchCentre de recherche INRIA Saclay – Île-de-FranceParc Orsay Université4, rue Jacques Monod, 91893 ORSAY CedexTéléphone : +33 1 72 92 59 00inria-00407778, version 1 - 28 Jul 2009Un tutoriel SsreflectR´esum´e : Ce document est un tutoriel pour ssreflect qui est un langage de preuve d´eriv´e de Coq.Ce tutoriel est principalement ´ecrit pour qui connaˆıt d´eja` les bases de la logique.Mots-cl´es : assistants `a la preuve, preuve formelle, Coq, r´eflexion `a petite ´echelle, tactiques.inria-00407778, version 1 - 28 Jul 2009°An Ssreflect Tutorial 3Contents1 Introduction 51.1 Ssreflect is ...