coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jan Bessai <jan.bessai AT tu-dortmund.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] proving a lemma in a proof
Date: Thu, 24 Jan 2019 20:49:18 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jan.bessai AT tu-dortmund.de; spf=Pass smtp.mailfrom=jan.bessai AT tu-dortmund.de; spf=None smtp.helo=postmaster AT unimail.uni-dortmund.de
Ironport-phdr: 9a23:fNpPeRdwxPz+5mRS94nMJvQGlGMj4u6mDksu8pMizoh2WeGdxcu+Yh7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM3/mHZhNJtgqxYrhKuqABwzJPWb46bL/d+Yr/RcMkGSWZdRMtdSSpMCZ68YYsVCOoBOP5VoY3nqFsIsBCzGBejBPj0yjBSh3/9wKo30+Y7HgHAxgAvBMwBsG/PrNrvNacfSvy1zLTRwTreaPNWwyv96I3VchAnvP6AR69/ftTIxEQpCgjLjU2QpJT4Mz+L0ukBqXaX4/diWO61lmIrtQJ8riKvy8sxkoXEhYIYxkra+Sln2oo4Idm1RFRlbdOrHpZdsTyROZFsTcM4WW5ovT43yr0Ytp6/eygH0Iknxxjea/yCaYeI4xbjWPyMITd+hXJpYa+whxGo8Ui8z+38S8+030tQoiVYjNbArnEN1xrN5cibUvZx41mt1DKV2wzN9+1JI1o4mbfFJ5Mi2LI9locfvVzGHiDsmUX2iKGWdl8j+uit8+nnYK/pppmGO4BvlA7+Kb8ulda+AekjLggOQnGX9vm71L354U35RahKjvsrnaXDrZ/VO9wXprSlDA9NzoYj9xG/Ai+639QfhHkLNU5KeBaaj4fyIFzOO/D5DfKng1u2ijtrxvbGPqfgAprXNHTDnq3hLv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdWz0wNUSezv38AdQ1goEXXySFD7SCOaL6rULN6uU1P+yRYoNTtDureKtt3OLnkXJswQxVRqKux5ZCMCnpTMQjGF2QZD/XuvlEFG4LugQkS+mz1g+eTHtfYGyuWr866nc3BdD/VNuRdsWWmLWEmRyDMNhOfGkfVAKQDDLkcJ+YXuoKZGSeL505y2FWZf2aU4YkkCqWmkr6xr5gdLeG5ysZsJvi0J5o4eyWmRYo6TlpCcjb32zfF2w=

On Thu, Jan 24, 2019 at 06:40:38PM +0100, Enrico Tassi wrote:

> Take this example:
>
> Lemma a ...
> ..
> apply b.
> ..
> Lemma b ...
> ...
> Qed.
> ..
> apply b.
> ..
> Qed.
>
> Note that the two "apply b" are different, the former is
> from an Imported module, for example, while the latter is
> the nested lemma b.
>
> One cannot really check the document as if b was coming before a
> since he would "capture" both occurrences of "b" and change the
> meaning of the document.

Out of curiosity:
Do nested Lemmas also pose problems in presence of the (co-)fix tactic?
These can change behaviour depending on the exact translation of the
Lemma: depending on whether the lemma is turned into a local/global let
binding or inlined, (co)fixpoints can sometimes deduce if structural
recursion conditions are met and sometimes they cannot. Or would
opaqueness via "Qed." always forbid that? If so: how is opaqueness
guaranteed if the whole outer lemma is translated into one term?

[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
        RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/28/2019
        Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/28/2019