coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re:[Coq-Club]

From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
To: Benoît Viguier <beviguier AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re:[Coq-Club]
Date: Wed, 30 Mar 2016 18:21:33 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT boipeva.ensmp.fr
Ironport-phdr: 9a23:e+it6BDPmP05XMFdOVImUyQJP3N1i/DPJgcQr6AfoPdwSP7zrsbcNUDSrc9gkEXOFd2CrakU26yM4+uxCSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTnkbrisMyDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZwaJ4f0AGlsXnQdJDhKNuBv3QJb+ryr3rMJy3SCbOYv9SrViChq46KI+RVzjjz5CPDok+knH2pQ2i7hU6FKMoh17womcQoyOpuE2UarZed4VQiJoRMdYTG0SUcuHc4ITAr9Zbq5jpI7nqg5L9EPmCA==
Organization: X80 Heavy Industries

Dear Benoît,

Benoît Viguier
<beviguier AT gmail.com>
writes:

> I have this proof I would like to use with some list ordering.
>
>> Fact orderbleb : (fun a b : Unit =>
>> is_true (orderb a b)) = order.

As it has been pointed out, this lemma is a bit strong.

Maybe you could restructure your development so

Fact orderbleb a b : is_true (orderb a b) <-> order a b.

would suffice?

E.

[Coq-Club], Benoît Viguier, 03/30/2016
- Re:[Coq-Club], Pierre Casteran, 03/30/2016
- Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
  - Re:[Coq-Club], Benoît Viguier, 03/30/2016
    - Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
      - Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], roux cody, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
        
        Re:[Coq-Club], Clément Pit--Claudel, 03/30/2016
        
        Re:[Coq-Club], Thorsten Altenkirch, 03/30/2016
- Re:[Coq-Club], Emilio Jesús Gallego Arias, 03/30/2016