Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
| Autor: | Théo Zimmermann, Hugo Herbelin |
|---|---|
| Přispěvatelé: | École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs ( PI.R2 ), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Paris (ENS-PSL) |
| Předmět: |
Computer Science - Logic in Computer Science
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES formal proofs [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Coq plugin isomorphisms proof assistant ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.4: Mechanical theorem proving Coq [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Computer Science - Mathematical Software theorem transfer [INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS] |
| Zdroj: | HAL Conference on Intelligent Computer Mathematics Conference on Intelligent Computer Mathematics, 2015, Washington, D.C., United States |
| Popis: | International audience; In mathematics, it is common practice to have several constructionsfor the same objects.Mathematicians will identify them modulo isomorphism and willnot worry later on which construction they use, as theorems provedfor one constructionwill be valid for all.When working with proof assistants, it is also common to see severaldata-types representing the same objects.This work aims at making the use of several isomorphic constructionsas simple and as transparent as it can be done informally inmathematics.This requires inferring automatically the missing proof-steps.We are designing an algorithm which finds and fills these missingproof-steps and we are implementing it as a plugin for Coq. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|