coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How can I make proofs from Standard Library transparent?

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] How can I make proofs from Standard Library transparent?
Date: Fri, 22 Apr 2016 01:32:02 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f180.google.com
Ironport-phdr: 9a23:jdBKiBHDIzr4DeePhgg/8Z1GYnF86YWxBRYc798ds5kLTJ75ociwAkXT6L1XgUPTWs2DsrQf27qQ7fGrADRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bsqtaKO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvNa8/VPlTCCksG2Ez/szi8xfZB0Pb7XwFF24SjxBgAg7f7Ri8UI2n4QXgse8o+S2fltftBZs1Qymm7rwjHB7sjS4dLHgy8XvKjs1rpK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MJWg==

Probably I can't. They're opaque and that's all.

I need them, for example, to prove that types list A (n + 1) and list A (S n) are equal and then use this equality in computations. For now I just prove necessary equality again, this time transparently.

[Coq-Club] How can I make proofs from Standard Library transparent?, Ilmārs Cīrulis, 04/22/2016
- Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Pierre Courtieu, 04/22/2016
  - Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Matthieu Sozeau, 04/22/2016
    - Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Ilmārs Cīrulis, 04/22/2016
      - Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Emilio Jesús Gallego Arias, 04/22/2016
        
        Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Daniel Schepler, 04/22/2016
        
        Re: [Coq-Club] How can I make proofs from Standard Library transparent?, Ilmārs Cīrulis, 04/25/2016