coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How can I make proofs from Standard Library transparent?
Date: Fri, 22 Apr 2016 13:54:22 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f172.google.com
Ironport-phdr: 9a23:dvYj4RS1xF8NeU4hZVg8oj1fxdpsv+yvbD5Q0YIujvd0So/mwa64YxON2/xhgRfzUJnB7Loc0qyN4/CmBjRLvcnJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviq9uMO04U23KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGa7qpxUhKgoyAaLSI4/Xyf3tRxgbhBrVSqoAFl34/ZfamaMfN/euXWetZMFjkJZdpYSyEUWtD0VIAIFedUeL8A94Q=

2016-04-22 0:32 GMT+02:00 Ilmārs Cīrulis
<ilmars.cirulis AT gmail.com>:
> Probably I can't. They're opaque and that's all.

I am afraid so.

> 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.

I don't understand, an equality cannot help "computation" as far as I
can tell. You mean that this equality allows to rewrite *and then* you
can compute right? But then the transparency is not the problem.

> For now I just prove necessary equality again, this time transparently.

Can you give some code here please? I don't see what transparency can help
here.

Best
Pierre Courtieu

[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