tutorial itp2016
27 August - Nancy
Satellite workshop of ITP 2016
-
Tactic language and Boolean predicates (09:00 - 10:30, by Enrico Tassi. Slides, Basic cheatsheet, Advanced cheatscheet)
The first lecture introduces the proof language Ssreflect, the Small scale reflection methodology --and in particular boolean reflection. The Mathematical Components library indeed features some systematic formalization patterns, like for instance representing decidable predicates with their decision procedures, which departs from the style employed in other large libraries. Supported by a concise and robust language of proof commands, this formalization style has scaled up to large proofs like the one of the Odd Order Theorem.
-
Big operators and their generic theory (11:00 - 12:30, by Laurent Thery. Slides)
The second lecture is devoted to the formalisation of iterated operations, their notations and generic theory. "Big" operators are the first example of an algebraic theory: whenever an operation validates an interface, e.g. the Monoid laws, the Mathematical Components library provides notations for its iterated form and a comprehensive palette of lemmas to manipulate them.
-
Finite types and finite graphs (14:00 - 15:30, by Yves Bertot. Slides)
The third lecture introduces the basic notion of finite type and its usage in the finite graphs library. This initial part of the Mathematical Components library has a low entrance barrier but can be already used to model many concrete problems expressed in terms of relations and of their transitive closure.
-
The matrix library (16:00 - 17:30, by Cyril Cohen. Slides)
The last lecture presents the matrix library. Matrices are built using most of the concepts presented in the previous lectures and constitute the socle of the linear algebra library. Matrices and their compact notations also provide a convenient device to model algorithms on graphs.
All teaching sessions are followed by or interleaved with exercise sessions. Participants are required to bring a laptop with a recent browser installed. In particular try out the test page.