coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
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 22:38:09 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:YUoKUxzninzojNHXCy+O+j09IxM/srCxBDY+r6Qd2+0SIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1boQ6uqRNwzIPPfIGaL+Bzcr/Bcd8GR2dMWNtaWSxbAoO7aosCF+4PMvhCr4bjolsPrQa1Cwe2C+Lh0T9IgXn21rA93uolDw7GxhIvH9cOsXjOotv6LqkTUfuyzKnO1jjMdfVW2Srn5IfWbx8hvOuAUqhtccfIz0QkCgDLjk2IpIHqIz+ZzPkBv3SZ4uZ6SO6ihWwqpxtsrjSx2MsgkobEi4YPxlzZ8Sh0wJw5KcCmREJne9KoDZVduiKCO4t4XMwvQH1ktSM/x7ACupO0ZycHxZE6yxPRdfOIbo2F4hz9W+uSPTt1gWxpd6mxhxu990Wr1/fyWdOu0FlQqypIitnMuW4J1xzU8sWKVvVy8Fq91TqSzgzd9+NLLE4tmarcMJEu3KQ8lp0OsUTfBSD2n1j2jKmLeUk+4uio8ePnYqn4qZCAK490iwb+MqI0lsy4HOQ4LgwOX2+c+eS/zrHs4Ur5QLBSgv03lKnWrozaKNwUq6KlGQNZz5ov5hSlAzu73tkVn2MLIE9bdB6Zl4TpPkvBIPH8DfexmVSslzJryujCMLL/GJXCMH3Dkbf7cbhz8UFdxhEzzddZ559PEL4BJu/zVlXvu9PFEx81KRa7w/v/BNVnyoweQX6PArOeMK7KrVCI4fsvL/CQa48RpTbyMOMo5+XujH88gV8SZ7Ol3ZoRaHCiH/RpOV+VYXT2goRJLWBf9AE5VanhjECIeT9VfXe7GawmrHlvA4W/SIzHW4qFgbqb3S79EIcANU5cDVXZM3ryeoCVE9sFdzmVJIc1sDEeWL2wDaMoygqpsifzzachI+bJvCQF48GwnONp7vHewElhvQd/CN6QhjnUHjNE21gQTjpz55hR5El0y1ONy6992qYKHNpOof5FT0EzKMyFlrAoO5XJQgvEO+yxZhO+WNz/W2M4SM93ztMTJU9gSY3700LzmhGyCrpQrISlQZw59qWAgCrYGv0lkjP95fJkiFMrBMxSKWehm6hzsRDJAJLEmFmYkKDscrkA2CnK9yGIym/c5Uw=

Hi Theo,

I assume "proper interface" refers to, for example, coqide.

Are you simply alluding to the fact that coqide makes it easier to
follow Laurent's answer ie "abort the proof. Prove the
lemma and then replay the proof",
or is there some feature of coqide (which I haven't found) which
facilitates "state your lemma and prove it outside (above) your current
proof"

Thanks

Jeremy

On 01/22/2019 06:47 PM, Théo Zimmermann wrote:
> Hi Jeremy,
>
> Sorry to insist but the simplest answer to this question is: use a
> proper interface which will allow you to state your lemma and prove it
> outside (above) your current proof. Nested lemmas are a feature whose
> use is strongly discouraged. Some users insist they need it (in
> particular during computation heavy proofs) and that's the only reason
> the feature has not been removed but the Coq developers are not
> interested in fixing bugs it may have...
>
> Théo

Re: [Coq-Club] proving a lemma in a proof, (continued)
- Re: [Coq-Club] proving a lemma in a proof, Laurent Thery, 01/22/2019
  - Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/22/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, Pierre Courtieu, 01/23/2019
    - Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
      - Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
        
        Re: [Coq-Club] proving a lemma in a proof, Ralf Jung, 01/24/2019
        Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/24/2019