coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] existT

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] existT
Date: Wed, 16 Oct 2019 16:04:30 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f45.google.com
Ironport-phdr: 9a23:pEeNqR+ZkFVZ7P9uRHKM819IXTAuvvDOBiVQ1KB40egcTK2v8tzYMVDF4r011RmVBN6dtK8P1LGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgtFiCC/bL5yIxm7rwvcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZI+tYr5P9p1oVrRCjCwejHubvyiRVjXLxwaI60/4hEQDd3AA6At0BqnHUrM7vOKcUVeC416bIzTDZYPNX3Tfx8pTHchckofyVW797bMnfyVE3Gg/bklmdrZbpMjCV2+gXrmSX8eltWfighmMnrQx6vyKhyd02iobTg4IY0lDE+jt9wIYyPdC4TVR0Yd+gEJdJuSCaMpZ6TtosQ2xnuCs20LIGuZm8fCgFzJQo2QTTZOCAc4iN+h7jVeCRLilkhH99Zr6zmxK//VKjx+D8TMW4zUhGoylfntTDtn0BzxnT5dKGSvt58EehwzGP1wXL5+5YIUA0j6vbK4U7zrEtjJUTtF/DEjXwmEXyl6KWeUAk9fKp6+TjeLnpupicN4pshgHkLqsugtC/Afg/MgUWQ2eb/v282KT/8k39XbVFleY7krLZsZDfPcQUvLS1Aw5T0oY56hawFS2q0NoCnSpPEFUQcxWeyoPtJluGdPv/FLK0h0mmuDZt3fHPeLP7VMbjNH/GxZzhZ7dmo2JVzRF7mdtf/ZNPTL0IJem1XEvZu9nRDxt/OAuxlbW0QO5h358TDDrcSpSSN7nf5AfRurAfZtKUbYpQgw7TbuA/7qe333A8kF4ZO6Ku2MlPMSHqLrFdO0ycJEHUrJIEGGYOsBA5SbWz2lKHWD9XIX21WvBlv2xpOMedFY7GA7uVrvmB0SO8RMAEY2lHDhWTFC6tednZHfgLby2WL4lqlTlWDbU=

Hello Jeremy,

Well, you have assumed an axiom here. It is quite possible to prove anything by assuming the

right (or wrong) axiom. 'Print Assumptions existT_inj.' shows what axioms you are relying on.

To understand what is going on you should study how the match operation works in coq. First

you could read the reference manual, more specifically the section

Calculus of Inductive Contructions/Inductive Definitions/Destructors. After that, try to

understand what you see when you do 'Print eq_rect.' After that you could try to construct

an injectivity lemma all by hand for pair. Next, try the same for a dependent type and notice

that you run into trouble.

Good luck,

Chris

Re: [Coq-Club] existT, (continued)
- Re: [Coq-Club] existT, Pierre Casteran, 10/01/2019
- Re: [Coq-Club] existT, Dominique Larchey-Wendling, 10/01/2019
  - Re: [Coq-Club] existT, Jeremy Dawson, 10/02/2019
    - Re: [Coq-Club] existT, Dominique Larchey-Wendling, 10/02/2019
      - Re: [Coq-Club] existT, Chris Dams, 10/02/2019
        
        Re: [Coq-Club] existT, Tom de Jong, 10/02/2019
        
        Re: [Coq-Club] existT, Jeremy Dawson, 10/16/2019
        
        Re: [Coq-Club] existT, Sylvain Boulmé, 10/16/2019
        Re: [Coq-Club] existT, Laurent Thery, 10/16/2019
        
        Re: [Coq-Club] existT, Matthieu Sozeau, 10/16/2019
        
        Re: [Coq-Club] existT, Chris Dams, 10/16/2019