coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Easiest way to recover broken proof

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Easiest way to recover broken proof
Date: Tue, 3 Aug 2021 18:47:00 +1000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f44.google.com
Ironport-hdrordr: A9a23:3HlCXqmcAwc/mGL4ovH1R0w9RzHpDfIh3DAbv31ZSRFFG/Fw9vre+8jzsCWftN9/YgBCpTntAsm9qBDnlKKdg7NhX4tKNTOO0ACVxepZnO7fKlPbaknDHy1muZuIsZISNDQ9NzdHZA/BjjWFLw==
Ironport-phdr: A9a23:wLsibhJSX0rkJVHNu9mcuK9mWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvbMz1xSUBM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipy+y+4ZzebgtHiDe9fL95MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8r1rRQfnhykHOTA383zZhNJsg69AvBKtuwZyz5LIbI2JNvdzeL7Wc9MARWpGW8ZcTylBAp6/b4QRFOoBPftTr5X8p1oAtxS+HwisD/7oxz9Nm3/23rM10/8hEQHa3QwhEcgBsG7VrNnvNacSUOG1zLXNzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyGAzLkk+eppb5PzOJyOsNqW6b4vJvW++ylWMppB99rzeyysool4TEmIIbxF7G+Ch3wIg4OMC1RFN1b9O5E5ZdtS+XOYVoT84/QWxkpSg3x70Jt5KmeiUB1Zopxxnaa/OdcoiI5AruVOmQITdkhHJlZamwiwyu/kinz+3xUNS/3lVSriddjNXAqnQA2wbQ58WHUPdx4Fut1DWV2w3c5exJJ10/m7DBJJ472LEwk4IesUTdES/yn0X7lKqWeV8l+uis8ujofKjpqoKFO496hQzzPb4imsO4AeQ/PQgOW3aU9f6g273k+E31WLRKjvsonanFqJ3WO9gXq6qjDwJW0osv8QizAyul3dgCknQKI0pJeBedgIjoP1HOLur4DfC6g1m0lTdr2vPGMaP6ApXNMnjDkbngcqxn605d0gYzzNFf55NICrEEO//zVUrxu8bZDh89KQC73+HnCNBl2oMERW2PGrOZML/VsVKQ+u0vJPCMaJYJtzb5Nvgq/OXjjWQ5mF8YZammx4EbaHG+HvR8IkWWe2DggtkbETRCgg1rR+vzzVaGTDR7ZnCoXqt66CtoJpihCNLGW4Ogm7zJwCakF4dXLjRDF1OBCnf0dpqNQfZKaSOTPspJnTkNVLznQIgkg0L9/DTmwqZqe7KHshYTsojugYAdDwL7mhQ79DgyBMOYgTjlp4RckWYBRjtw16d68xQVIrar1KF5h7lVGYUW6a8VFAg9MpHYwqpxDNWgAmr8

Hi Everyone,

2 years ago, I wrote a proof [1] using Coq 8.10 (if I remember
correctly), but now the proof can't get past Coq 8.12.2. With Coq
8.10, I used the 'firstorder' tactic generously, to build the terms,
and now most of these are broken.

My question is: how can I fix it with the least amount of effort? One
idea that I have is to get the Coq 8.10 and replay the proof. From the
proof, get the Gallina terms by using 'Show Proof' and use the Gallina
terms directly to build the current proof. I am curious if there is
another way to do this.

Best,
Mukesh

[1]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/Workingcode/ValidityExist.v#L83-L1460

[Coq-Club] Easiest way to recover broken proof, mukesh tiwari, 08/03/2021
- Re: [Coq-Club] Easiest way to recover broken proof, Gaëtan Gilbert, 08/03/2021
- Re: [Coq-Club] Easiest way to recover broken proof, Théo Zimmermann, 08/03/2021