coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] proving a lemma in a proof

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] proving a lemma in a proof
Date: Wed, 23 Jan 2019 09:52:43 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga07.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.400.15
Ironport-phdr: 9a23:VhvH8hQIDmz1yoyiCLaoHk8lUdpsv+yvbD5Q0YIujvd0So/mwa6yYRCN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO/Vwc7jBfdwBQWdNQtpdWzBDD466coABD/ABPeFdr4TlqVcAsBy+ChejBOPz0D9IgWf20bUn2OomEAHJwAwgEMgQv3TQotn+KaAfUeW0zKbUzTXMde1Z2TPn5IjTdRAuv/6MXa5qccrW0UkiDALFjlOMqYP7OzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEhoMTylDY6yp5xJw5KsCmR0N9fNWqE4NQujmHO4Z4Tc4uWXxktSg1x7EcpJK2cikHxI46yxLDd/CLa5WE7xPtWeqLLzp1imhpdKyxihu260Ss1+7xWtSs3FpXrydIlsPAum4N2hHc8MSLVOFx80ah1DuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbGy/2l1/5gLOUe0k+++io7fjnbavippOGK4B0jQT+Prwvmsy5H+s4LhADU3WV9OmzzrHv4EP0TbpQgvErnKTUsYrWKdkHqqKlGwNV15ws6xe7DzeoytQYmnwHIUpAeBKGk4fpO0vBL+78DfulmFSslylkx//aPr37BZXNNmPOkLbnfbZh9UFczBA/wsxY55JREr0BOu78WlfttNzECR80KxC7w+H+CNlkyoweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiNEcb2n9FfB7KW2YZ2Dti5EPCy1C6gE5VanhjECIeT9VfXe7GawmsGIVEoWjWM34QY2inKaGxGPzO5xdZmlLDhrERXLpfIWNVvNKcyWfLdN7lSQsVL69Rotn3har4lypg4F7J/bZr3VL/ano08J4srWKxEMCsAdsBsHY6FmjCmR9n2cGXTgzhfktoEphx1PF2q990aUBSY5joshRWwJ/DqbyivRgAomrCAPHYtqNDl2hR4f+WGxjfpcK29YLJn1FNZCigxTEhnX4BrAcz+PNBZoo/6aa1H/0dZ5w

Dear Gaëtan,

> What's the local context? It sounds like the following, however that
> doesn't work

actually I don't know since I never used this local context - and as I said I
don't want it. When I discussed this on the CIW and asked what the technical
difficulty with nested proof was, the answer I got was that nested lemmas can
use some sort of local context of the outer proof which results in a lot of
trouble. It is of cause quite possible that I misunderstood the answer. I
know that the context of the outer proof is hidden when a nested proof is
started, but for me it is hard to tell what fraction of what is really there
is shown by the UI.

In case I got it wrong, can you explain what the problem with nested proofs
is, so that a mere Coq user can understand it?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] proving a lemma in a proof, Jeremy Dawson, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/22/2019
  - Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/22/2019
    - Re: [Coq-Club] proving a lemma in a proof, Andrew Appel, 01/22/2019
    - Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/22/2019
      - Re: [Coq-Club] proving a lemma in a proof, Jim Fehrle, 01/22/2019
      - RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
        
        RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/24/2019
        Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/24/2019
        Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/24/2019
        
        RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
        RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
        Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/25/2019
        RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
        Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/26/2019