Thursday 27 April 2017, 14:00: Automatic and Transparent Transfer of Theorems along (Iso)morphisms in the Coq Proof Assistant, Théo Zimmermann (πr²).

In mathematics, it is common practice to have several constructions for the same objects. Mathematicians will identify them modulo isomorphism and will not worry later on which construction they use, as theorems proved for one construction will be valid for all. When working with proof assistants, it is also common to see several data-types representing the same objects. We present the Transfer library for Coq, which allows transporting theorems between related structures. We detail its implementation, which was strongly influenced by the generalized rewriting capacity of Coq, and is also connected to the Isabelle package of the same name. We give some examples of applications, both in Coq and Isabelle, and some perspectives.