coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Talia Ringer <tringer AT cs.washington.edu>
Cc: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}
Date: Fri, 21 Feb 2020 18:29:33 -0500
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:V6RD5RDeZNH3eYYv3aowUyQJP3N1i/DPJgcQr6AfoPdwSPv8p8bcNUDSrc9gkEXOFd2Cra4d16yG7uu4CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIxi6twbcu8kZjYd+Lqs61wfErGZPd+lKymxkIk6ekQzh7cmq5p5j9CpQu/Ml98FeVKjxYro1Q79FAjk4Km45/MLkuwXNQguJ/XscT34ZkgFUDAjf7RH1RYn+vy3nvedgwiaaPMn2TbcpWTS+6qpgVRHlhDsbOzM/7WrakdJ7gr5Frx29phx/24/Ub5+TNPpiZaPWYNcWSXNcUspNSyBNB4WxZJYNAeUcJ+ZVt4nzqUUToxu5CwmiCuHgxDxGiXD5waI3yPghHR3c0QA8A94DqnbZodPoP6kSS+C1y6zIwC3MYfNT2Df97InIchc5rv+IQ71watDJyVI3GA3ElFqQrYjlMC2a1uQKq2eW8/BgVeO1hG48tgp8pSagy9wji4TKmo4Z0FfE9T92wIssI9CzVU11Yca8HZdNtCyXNJF6Tt08T2xpoio2178LtYOhcCQXxpkr2QbTZv6JfoSS/x7uW/idLS18iX9lYr6zmhe//VSmx+bhTMe7ykxKoTBAktTUtnACyRjT6s+fR/py/UqtxSyD1wfJ6uFLOUw0lKzbJIA9wrMoi5YeskfOEjXolEnojaKabFgo9+q15+j9f7nrqIGQO5dxig7kM6QunsK/Af4/MggLR2WU5/+x1bLg8EHlWrlKiec2kqbBvJDAOcsbvrK5AxNS0os79xm/CC6m3M0EknkDMVJKYwmKj5PpOlHLOPD3F+2zg1WqkDdxxvDJJKftApvXLiuLrLC0Qb956kcU8gs1wt1Fr8ZIELAHL//pckTq8sPRFR84NQOoxOChBdlggNAwQ2WKV4KcMafTtmiq6/m9ON6jbYsRtTn6HNE/5vf1xSs0sU9NJe+ux5RBOyPwJehvP0jMOSmkudwGC2pf+1NmFLW32m3HaiZaYjOJZ4x55jw/D9P0HdebAIe3j+7YhXvpLthtfmlDT2u0PzLwbYzVCedcMGSVOMAzymVVB4jkcJco0FSVjCG/zrNmKuTO/ShJ54KzjJ5y/eKBzBw=
Organization: X80 Heavy Industries

Talia Ringer
<tringer AT cs.washington.edu>
writes:

> Is there a useful induction principle for { l : list T & length l = n }
> that people use in general?

I'm not sure if understand your question but isn't the eliminator you
want the one that is [indeed] provided by math-comp's subtype: basically
for

{ x & P x }

(you can make P boolean if you want) you go to

x /\ P x

then you can compose with the eliminator for x's type (being careful
about quantification of free variables of P.

Kind regards,
E.

[Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
- Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/21/2020
  - Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
    - Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Daniel Schepler, 02/21/2020
      - Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Valentin Robert, 02/21/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/21/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Dominique Larchey-Wendling, 02/21/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Emilio Jesús Gallego Arias, 02/22/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/22/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Hugo Herbelin, 02/22/2020
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Arthur Azevedo de Amorim, 02/22/2020
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Jason Gross, 02/22/2020
        
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Hugo Herbelin, 02/22/2020
        Re: [Coq-Club] Ideal eliminator for { l : list T & length l = n}, Talia Ringer, 02/23/2020