Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Proofs working in Coq 8.10 needed

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proofs working in Coq 8.10 needed


Chronological Thread 
  • From: Mario Frank <mafrank AT uni-potsdam.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Proofs working in Coq 8.10 needed
  • Date: Wed, 10 Jul 2019 13:20:19 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mafrank AT uni-potsdam.de; spf=Pass smtp.mailfrom=mafrank AT uni-potsdam.de; spf=None smtp.helo=postmaster AT cl-mail.uni-potsdam.de
  • Autocrypt: addr=mafrank AT uni-potsdam.de; prefer-encrypt=mutual; keydata= mQINBFoxDJEBEADR2Sq8pVKjj8rhF/ybxsEPg9wXNvpBi13nslcbZEWl6DmuZprwPi4pFU1y nH1PPsTFImbpIQWXdAMlXiBi2QdLW1yvw7Hl9nPYQdnrhiZXYrL7ECslAKVcdZXb/+k3i6h9 B5xBQTPGApPkShWgcIl6bNROxQ7lpq9nWK93z6XRxW01bSKi8FLIBp+zHZvoAgnFbwqa9zv7 n+6MvaOlI1yMf4izFMrd3IrswpciIKCmfiWHzhFsFyi09Wd4I7G3etxbYC9/Eg6vuWJjttYl rjyeQxTSWuIs88eyra0fNPjxRZ/alyVAyx9GDPJMIKTjpx8i8YoA9kh2NtNOrbi9hG6yy/Cs QfRkS47JKkKFGJvGuxxtd/WesqPy2VSzVoqr91LNdn6d8QKHEDJkG8G4Jhl8UovbbBWZ+0oX zdxogAGEDWqcHIWbprb2R21BgsZP40RFsdxvQstn5eKzwSy1A+XBLl8piCeFBeX/1HL4XkTA BuPjuk3Jcct7684J8duLDyWLqbEoboEV7KoNf+uDvQFDt0SYyznVu5w3keulb5BdDAPBFTux U1mBBMOf6Gf6dF7NNeOEPJvytR+8qzeh8OgwO6h8kmxRtxLwOm8Qt/rHitbKlRaikB4buRXu IYxE8YChpClA9cBjyUnoqFbQkGZhiOW9Ywhyb8JcvzjJhfcRCQARAQABtCRNYXJpbyBGcmFu ayA8bWFmcmFua0B1bmktcG90c2RhbS5kZT6JAlcEEwEIAEECGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AWIQQKmKntZdGhu/uI1pptG7hdbe5oSwUCWjENZQIZAQAKCRBtG7hd be5oS8ggD/43a8LyfUFV4lC75MkA98jVpVgwSIK1Qte1D4/bgTALWUVmHrvmwu6bTCOQ6ar5 pmSORdc/xiOM8UR+X6WGgAHV/4/jYMtrwLV0pGP027idEq4fpO68DzlC3xFEFbJTrq9NS7Jn vfIO3fWPNoMs7xBtgcc6I9ynZHEDsYX2YR6xjjBznOsKEVk6sWv/IaechL71qqyzGKPkZOCp vlGzJo84D7XzFC6cHa3eqwSEBPrBGK1HlJSHHk4/hEhThvUkTtroDNbojnfgI90X3qfWLUcZ QRU7AaZtbpProuc+So53stamzlX8o4uO8IkVznwbbC97Gr+XpvP4CFiw6N2gtr3xbDvd5Ekk MIGrZyY22r5WLx3C3ba0ykUMdcyZjtdY72j9BMHsNWpVyUimYvWu3n01ZzVGiwmEiXKAnRVI 59tuHFoB0VIRRy2EqXr/DQw8gB1y2HQVivA/pIWmrrKy99olEHcM6W1gvoWuUZ/FhPogkWv6 YZBx9wScM2Empt06+WqTueSJbhAFRfJmXHoc0niCE4wSmeF0+Pu1VzADm0eXzmxvadYm8iXM TGY22Dcpepyaa1AA4xG0DhmwxO1dxp+XuZvuvt/w8JufM5cFQCSRwIbD4wczjAqRs24l8LSF aI9KVLh3ifzu9OfZhN5xbt1/wWry+xIewC8BkZqOQ/p4HLkCDQRaMQyRARAAy2urmyA86ZX6 /0KymXZCuMFoulPuHiMUxP2Wrbj0jn1vZA7icUDVLlrFkq2FtU2+/tesA/TmeM9zsXN7jGxA je1A/KmwMt+nyqlMde/2kXLvQ3JRckWiyuaoHAFR/B8qzDqy9NApT2cWM85edK6h1LhxCqna XUzRj8NCpXfxq6W4mY+Ey7A2Pf1tWVWWNzMPt1hfaXiY1Q2OMMqkquDUkj0mXxOJfh+SzXh1 LkA5hkPLzIz6RQYgS93ck5Wvbf4WlMqr6MuQNXVbK55jX6h3XJKcHB0P4TM45MDf+CxxApxX sZf1NJKuP0e+GKuMm8f0owdr34l4vWDezwvtLfiagYR15DpGtXs6Eqqy+eYhBrEPg6obrPzZ bHYcBHowASLMv0NqQLtcA5LcT7WxDfAeEVEMmw4eEIGNP0ImE89po9vstKIrvLR8tAwWInqb zUCWNeF80htfDG13phb6VCchefK3b67uwVyA9queR0wj+21txOzm3ZGnI+4browrvpRYiQPw +q01p+8bgF6BQ5qGgI/Qewg7g0qRJ+HAaPBtxW7MsGygGcJCdjhmALz+sAh5pn4JF7MUXcQh v8B9nRpjnnkFKMf5wV39sA4H4WMrQ7ACOdBSG3SrNABs7dc/6omJMEaEZcN7aW1oHDHtzYA7 CwpolaYs+9sjZyeroWrjxiEAEQEAAYkCPAQYAQgAJhYhBAqYqe1l0aG7+4jWmm0buF1t7mhL BQJaMQyRAhsMBQkJZgGAAAoJEG0buF1t7mhL0hcQAKkKx6SyDexz5JXFog3VlADoo8RCvNFS ctuoaqBVTmfljTD4dhRR3Nc0y02xhHu2BKb3XscacdUVV/29G3jaRUGLZKiEpo5DMTrODJAo qrs0VUYkfFBxQXwKEbAppaOcXKbQKi+OFMPGF3sEoO81y6JGm+vym4/OskrHROyduLqTakG0 by9xm8nmCoOulDl7shIbyGaWzaVBXBQPGJIp+JDgOh99ftwe5S8APFn9hYi5YSrJt1iXwGWb 7Fri0Nepsm4cVsVYdecZe6Z8ucDR7rUTzxVS5fgmDPRqJbeZY7g8/nDaD/HN7o03YLpYLWw9 wIA4oHHNcTF6ldErb2kvWbVLxf7WjtnlgFa/MBLKkse8ClJAKXvnYY0vHJwuBn+aVn3ne24X 702Wpt4uKKIHLZaBOgnenS9LYzwRUyUeTY2P4sm4Z+sFBsmT2uC9PW7YJuvuYnMeqpnuMp0N +UCbzr1hm6iw8DEO8HhJaKQCP3kX/nivRpmaWn4MAYBEJfPVx/9GE++CucgmxPgF3fShTACE ANwF/AmPakk5rd1W7Sk7pfYMqw6iMtcVr70590TGX8ZbwVbtfIFBTLYWeThHG3Gn9gwtkV5p 1LgFIdW8M4y244gq6TvtaQ4iHSrXbiwZ6LZ38bCR8lCcz3TY+a5c399ve8KcOdEl1C4m8DhW g4TQ
  • Ironport-phdr: 9a23:AVpR/hD8cNTyCfPYGiusUyQJP3N1i/DPJgcQr6AfoPdwSPv5rsbcNUDSrc9gkEXOFd2Cra4d0ayK7eu7CSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagf79+Nhq7oATeusQYgoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RtgqxFrhKvpx9xzYDab46aNvVxYrjQfdwGSWdbQstdSyJMD4O6YoASD+QBJ+FYr4zlqlUJtxS+HwisBOTywTFInH/5x6s60+c8GgzB2QwvBdwOsG7Oo9XzN6cfSv21zK/JzTnad/NW3iv96JPVfR87pPGAR69/ftTIxEQpCgjLjU2QpJT4Mz6ay+gBqWuW4u56We+uiGMrsRx9riCyysojl4XFnIEYx1Te+Sh5zos5P8C0RU95bNOiDZBerTuVN5FsTcMnW2xouDg1yrkBuZOjYCcKzI0rxxvFZPyGd4iE+A/jVOCQITthnHJlf66/hw2v/ke6z+3wTNS730hSoipElNnDqGwN2gTO5sWIV/dx5ESs1DKV2w3S6exIO104mbLeK5E7w74wkpQTsV7EHi/zgEj2ibWZdks++uey7eTnYa7rpoKaN491kw3+KqMumtCkAeslKAcOWnKX9vmi27H75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mPVW/ZNTQp8bKfTwEhv0vdLCBxk6GxGywqP/D8lm2oobH26CVPzKeJjOuEOFs7p8a9KHY5UY7W6kd6oVosX2hHp8omczOLGz1MJJOm2+H7F+JFmCbXPpxNsMQz9T41gOCdfygVjHagZ9Ina/W6VmumMwDMejBIbHAJ2rgfmZ2zugEpRTIGxLWAjVQCXYMr6cUvJJUxq8Z8pokzgKT7+kEtFzyBev8Rf916FrJ++S9iBK7J8=
  • Openpgp: preference=signencrypt

Dear Coq Team and users,

we are working on a tool for Coq 8.10 that aims to extract information
about proofs e.g. for teaching purposes and currently lack proof files
written
for that version that are complete, self-consistent and sufficiently
complex.

Thus, I would be glad about any .v file that contains at least one not too
easy proof and does not use other .v files except the ones that Coq
provides.
I would appreciate even more proofs with use of bullets, focus and pose
commands.

Best regards,
Mario

---
Dipl.-Inform Mario Frank
Wissenschaftlicher Mitarbeiter
Universität Potsdam
Insitut für Informatik und Computational Science
- Lehrstuhl Theoretische Informatik -
eMail:
mario.frank AT uni-potsdam.de
fon: +49 331 977 3069


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature




Archive powered by MHonArc 2.6.18.

Top of Page