coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Translation of Euclid's book 1 from GeoCoq

From: Yoan <yoan.geran AT mines-paristech.fr>
To: "deducteam AT inria.frcoq-club"@inria.fr, isabelle-users AT cl.cam.ac.uk, hol-info-request AT lists.sourceforge.net, matita AT cs.unibo.it, pvs AT csl.sri.com, coq-club AT inria.fr
Subject: [Coq-Club] Translation of Euclid's book 1 from GeoCoq
Date: Fri, 17 Dec 2021 17:52:25 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yoan.geran AT mines-paristech.fr; spf=Pass smtp.mailfrom=yoan.geran AT mines-paristech.fr; spf=None smtp.helo=postmaster AT antispam-1.ensmp.fr
Dkim-filter: OpenDKIM Filter v2.10.3 z-smtp.mines-paristech.fr 0C4F81C00D7
Ironport-data: A9a23:1TRh1KC04GBhMBVW/1fiw5YqxClBgxIJ4g17XOLfV1S51Twh0DdRzTMXWGGGPf2CZGvzKIgiPt/kpkoAsJGkm99gGjLY11k9FiMQ8ZKt6fexdxqrYXvKdqUvdK/WhiknQoGowPscEzmM9n9BDpC79SMljPvRGeKlYAL5EnkZqTFMGH9JZS1LwLZRbr5A2bBVMivV0T/Ai5W31GyNh1aYBlkpB5er83uDihhdVAQw5TTSbdgT1LPXeuJ84Jg3fcldJFOgKmVY83LTegrN8F251juxExYFA9W5k63je0hPG/jfOxOLkjxYQcBOgDAd+Wprj/Z9baVHLxcN49mKt4gZJNFlpJu5T0EmM7fFnswYUh9VCGRmNLdH46PKKnj5v9b7I0juLySymqU0ZK0xFdRCqrstWwmi78cwIzcUKxuHmuie26O+UuAqh8I5LcCtMpl3h53K5SWBWK5gGYSaFv2MvcsCiW922pETQeKFMpJfNC4wOT3eRTZKHHsXLbM3uNuyoG2mK2gA7AqBzUYsy2PU0RZr0bXpdYGTf92MSN4Qhk+Cp3na8m/5RB8AXOFzAAGtqhqE7tIjVwuiMG7TKFG5yhKuqFSV2m0IEBQTEAL9rP+ij1b4Vcg3x4k8ksYxhfBayaBpZoCVs96ETLqsux8aVsEVC+Qg6RqRx6HUpQiDboTBZiAUc8Qo7afaWhRzvmJkXLrV6fhHtbyTRGnY7r6OrCiuNCMVa2EYDcPBZWPp/PG7yLwOYtnzohqP3UJ7YhAZ2d09/txSkBUDug==
Ironport-hdrordr: A9a23:bPdpqa84TJojqhbczQxuk+DFI+orL9Y04lQ7vn2ZJiY6TiX1raGTdYoguSMc4Qx5MBpM9uxoU5PwIk80m6QU3aAheZOZdE3dmFLAFutfBeeO+UyDJxHD
Ironport-phdr: A9a23:tUGoRh/uAEabaP9uWSm7ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZQqOuL401gOBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdm72/q29pDTbAlEmSSxbLxvJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlicJOSM6/m/ZhMN/g75Urh26qhxjwYPZep2ZOOZwc67fe94RWGpPXtxWVyxEGo6zbYwPAPAHPe1FqIT8p1wOogG4BQW2C+Pg1CVIiWXw3aAh1uQhEAfG0xI7H94XqHTbts/1NKYJUeCp0qbH0TXDY+lY2Tfn8YXFdA0qrv6QU7xqa8XR1VUvGB3fjlWWsYHoIS2Z2+QMvmaV8edsS/+ihnAjpgxzoDWj2tkhh5fXio8V1l3I6CZ0zYU0KNGkSkN3fcKpHpRQui2EM4Z4TMcvTmd1syg0zb0GvIS0fCkMyJk/yB7fauCHc4iV4h34TuqePTB4hHdjdbmihBiy6VCtx+/+W8WuzVpHrilInsPRun0P2RHf8MuKRuVl8ku81zuC1Brf5v9KLEwpj6bXNpEsz7wqmpYOv0nOHSn7k1jsgqCMbEUr4O2o5vznYrr4op+cMJd5hRv4MqQym8y/Gvw4PRILX2SC5OiwzqPs/UviQLVPlv06iKfZsIrCKcQaoK62HRNV354h5hu9FTuqzdQVkHodIF5Yeh+KgZLlNlLQLPzgCPewmVWskDNlx/DcOb3hB43AL3jEkLj7e7Zx8UFcxxQpzd9F4ZJZEbQBIPP1WkDvr9zUFwc5PBauw+bmE9V9yp0RVn6PAqODPqPSq0eE5vgzLOmUeI8VpDH9JuA56P7plH81gEMSfa203ZQMc324BfRnI0CBYXX2mNsBEGEKvhA/TOPwklGCXyRTa263X6I7+z40FpqrDZzGRoCxmLyB2zq7HoEFLlxBXxqAHHv1fJmJUvIkaSSII8YnnCYPUqHkQIs831uGtQngyrMhIPCQsiwDvJju0Nx4ovDImAsp3TdwSc+U1ieERCdpnSdARzgymaF5r0s40FqazKVjn9RcFMdP/LVSVRogPpPSyPZ1Bpb0Vx6FNtKAVFe6S/2tGncsSNM7xJkPfwI1A8u5phvY22yxGb5TnLuOQNQ/9buZ1HzsLe58zWzH3e8vlQoIWMxKYFyhj6g3oxnUDoiPnEiDnqCCcKUa0TWI7G6ZzHGSsUpYFgBqB/aWFUsDb1fb+IyqrnjJSKWjXOxP2uRpzM+EJ7APctTzjE5aSfzjftrEMTvZc4aYDBCUx6iUZY+vIiMQ2j7YEA4KiVJLlZ5jHQ0/ACq65nrXFj11CV/kYwXi67smwE4=

Hello,

We are glad to announce that we have translated the proofs of Euclid's
book I, originally developed in Coq, to five other proof systems: HOL
Light, Lean, Matita, OpenTheory (hence Isabelle/HOL and HOL4), and
PVS.

The Coq original development is described in [1] and available in [2].
The translations are available in [3]. For now, only the source files
are available, without a Makefile.

These proofs have been produced in four steps: the definition of (part
of) the theory of Coq in the logical framework Dedukti, the
translation of the Coq proofs to Dedukti, the transformation of the
Dedukti proofs, so that they fit in a much smaller theory: Predicate
logic, and the export of these proofs to the aforementioned systems.

Best regards,

Yoan G.

[1] M.Beeson, J. Narboux, and F. Wiedijk, Proof-checking Euclid,
Annals of Mathematics and Artificial Intelligence, Springer, 2019.

[2] https://github.com/GeoCoq/GeoCoq/tree/master/Elements/OriginalProofs

[3] https://github.com/Karnaj/sttfa_geocoq_euclid

[Coq-Club] Translation of Euclid's book 1 from GeoCoq, Yoan, 12/17/2021