coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cases in leq proof

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] cases in leq proof
Date: Tue, 22 Dec 2020 15:16:15 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:dkG7cBdg2rxTHTmTNHOFRnLrlGMj4u6mDksu8pMizoh2WeGdxcS5ZB7h7PlgxGXEQZ/co6odzbaP7Oa6ATBLuMzc+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi0oAnLqMUanYRvJqksxhfXonZDZvhby35vKV+PhRj3+92+/IRk8yReuvIh89BPXKDndKkmTrJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4qJ2QxLmlCsLKzg0+3zRh8dtjqxUvQihqgRizYDKboGbNPlwcK3TctwVR2VOQt1cWDZdDo6mdYYDE+QMMOReooLgp1UOtxy+BQy0Ce7z1zBHnHr21rAk3uQhFQHG3RQgEMgKsHvOsd74M70dXv2vw6nN0TrOdO9Z2Szn54jJdhAtu/SMXbNsccbL10YgCh7Fg0yWpIf4MDybyv4DvHKH7+p8S+2vkWgnphlzrzWs2MoglJXEipwVxF3Y9ih03oc4K9O6RUNlfNOqH5teuiOVOodrQs4vTGFmtSk+x7Abp5K2fSoHxpsnyhPQbfGMbouG4gr7WeqMPzt1h2hpdbyjixqo70Ss0PPwWtSo3FpSrCdInMPAum4Q2xHX8MSKS/tw8l281TqRywze7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gEL2jLKKdkUr/eio6uLnYrr/qp+HK497kB3+Pb40lsOjGuQ3KAkOX2yB9eS51b3j4Vf1T6tXgf0riqXZsZbaKtoHpqOhHgNZzIUu5wyxAju6ytgUg2MLIExYdB6bl4TpPkvBIPH8DfexmVSslzJryujcMbL8GJrNK2TMnaz9crZm8UFcyQ4zwcpa55JVFrENOuz8VVLstNDAFB82LxS0w/r7CNV6zo4RRWWPAraAPKzOtV+I+/kgLvKXZI4VvTb9M+Iq6+TvjX8/g18dfLOm0YEZaHCiTbxaJBCSZmOpidMcG08LuBA/Rarkkg6sSzlWMl++Vqd0zTE/CZqvCY6LEomhibmK9CygF5xSIGVHFhaBHWq+JNbMYOsFdC/HepwpqTcDT7X0E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090sur/Yjhgz8XpxDtjb3m2QHTgtwzE4AgQu1aU6mnRTj1eO1a8j265fCMBc4PJPXUIhKZfAxqpxENnzXkTEf8vPRVq7EI3/XWMBC+kpytpLWH5TXs24h0mejSGxCr4R0bmKGNo5/r+Oh3U=

Certainly, that's the most standard way to prove anything from an assumption of "leq". It sounds like you should probably go back to a source like Software Foundations for details. A useful keyword is "inversion."

On 12/22/20 3:04 PM, Patricia Peratto wrote:

Is there some way to make a case analisis over a proof

of a leq proposition?

Regards,

Patricia

[Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
  - Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Robbert Krebbers, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
      - Re: [Coq-Club] cases in leq proof, Dominique Larchey-Wendling, 12/23/2020
      - Re: [Coq-Club] cases in leq proof, Castéran Pierre, 12/23/2020