coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] finite data types

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Xavier Leroy <xavier.leroy AT college-de-france.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] finite data types
Date: Wed, 20 Mar 2019 16:27:28 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:RweaOhe5VBIn4FR+Ggh/GZO5lGMj4u6mDksu8pMizoh2WeGdxcu8YR7h7PlgxGXEQZ/co6odzbaP6+a+Bydfvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMBm6twTcu8gZjYZgJas61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuQBI+hWso79p1UAoxS8BgejCuzgxSNHiHLtwa06yv4sHR3a0AE6Hd8DtmnfotXvNKcVVOC41KbGzTDCb/NS2Df975DHfBQ/rvGXR6pwatLex0g1GAPBilWft4PlPzSN2ekRqWib7vBvVfmygGMgtQ58uTeuy8QwhoXTgYIV0F/E+Dx/zY0oJtO4UFZ2bcOnHZZTrS2WKZV6T8I4T211uis216cKtYO1cSQU0JgqxB/SZ+aGfoWK+B7uUPydLDV8iX9jZbmxnQy98VK6xe35TsS00EhFri5CktTUuXEA1ADf5tKASvtn8UetwTeP1wbN5eFYOU04iKnWJp07zrIuiJYesF7PEjL0lUnrlqOaa0sp9vaw5+TieLrmp5ucN4FuigH5N6QjgtKwDP83MwUNQ2SX4+O81Kfs/UHhWrVFkuU2krXFsJDdPckUuqm5AxZM3ok/7xa/Eiyp3c8DnXgHKVJFYAiIg5LoO1HIOvD4DO2wj06ikDdxlLj6OejRC4vMI2KLtLr7eqc1v15V1gs+15Zb6ohTG5kKJ/b3V0D88dDVSxEjOgq/zqDpEoMu+JkZXDeiB66dMaTlk1KTdPkYDOCIYIIavwHUMfks/La6gFcpyQdberOmi8hEIEukF+hrdh3KKUHnhc0MRCJT5lJnHb7azWaaWDsWXE6cGqc15zU1EoWjXNXTFtjrh6aOjn7iQs9mI1teA1XJKk/GMp2eUqZeeHLKZMh7nW5cDOXze8oazRir8TTC5f9nI+7Tq38I5cql08J6tbTe
Organization: X80 Heavy Industries

Xavier Leroy
<xavier.leroy AT college-de-france.fr>
writes:

>> > so that proofs of the proposition "-1 < x /\ x < max" are unique.
>>
>> Isn't that also true with "x >= 0 /\ x < max"?
>
> Sadly, no. "x >= 0" is defined as "Z.compare x 0 <> Lt", i.e. the negation

Indeed I have never understood why `>=` and `<` are not boolean
functions in these cases; things seem to become _much_ simpler as you
can handle generically sigma types with an irrelevant proof à la
math-comp's subType.

E.

[Coq-Club] finite data types, fritjof, 03/18/2019
- Re: [Coq-Club] finite data types, Mario Alvarez Picallo, 03/18/2019
- Re: [Coq-Club] finite data types, Jan Bessai, 03/18/2019
- Re: [Coq-Club] finite data types, Maximilian Wuttke, 03/18/2019
  - Re: [Coq-Club] finite data types, Gregory Malecha, 03/19/2019
- Re: [Coq-Club] finite data types, Alix Trieu, 03/19/2019
  - Re: [Coq-Club] finite data types, Xavier Leroy, 03/19/2019
    - Re: [Coq-Club] finite data types, Gaëtan Gilbert, 03/19/2019
      - Re: [Coq-Club] finite data types, Xavier Leroy, 03/19/2019
        
        Re: [Coq-Club] finite data types, Fritjof Bornebusch, 03/20/2019
        
        Re: [Coq-Club] finite data types, Emilio Jesús Gallego Arias, 03/20/2019