Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] proving a lemma in a proof
  • Date: Mon, 28 Jan 2019 11:10:00 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f46.google.com
  • Ironport-phdr: 9a23:GA47GhRsNhdtNxNYax6VewPYstpsv+yvbD5Q0YIujvd0So/mwa6yZRGN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QAogCzBRW1BO711jNEmmP60K883u88EQ/GxgsgH9cWvXrOrdX6Kr0SUfqrw6LV0zjDaO5W2S3h6IjJbB8hvOyHULVoccrQ10YvDRnFgUuKpYP5ODOVy/4Ns3Sa7+V+SOKikGEnqwRrrTiuwscgkJXGhoUQyl3d8yhy3Yg7Jdq9SEFhYN6kFoNdtyCcN4tqXMwiR3tktzskxbAApJW1fzAKxYw5yxLDb/GLaYuF7xL5WOqMIDp1hWhpdb2+ihu07EOu0PfzVtOu31ZPtidFksfDtnQK1xHL78iIUPp9/kO41TaO0ADf9/hIIU47mKfaMZIhzbkwlp0csUTHACD6gln5jKiTdkk8++io7froYqn+q5OCK4N5jhvyP6cul8ClHOg1MwkDU3KU9Om9zLHj+Ff2QLROjv04iKnZt5XaKNwDpq64HQBVyJwj5AilAzi619QYgGMHLE5EeB2ZkojkIF7OIPXiAve+h1Sgiitkx/fDPrH5GJXCMmDDkKv9fbZ680NT1A0zzclG651IDrEBPen8V1TqtN3YCx85Kxa7z/zmCNV7zIMeWHiADrWXMKPI4he04bcEJPDET4sIsn6pIP88ovXqkHURmFkHfKDv04FBO16iGfEzG0SUe2DhyvwGDH0WvwcjBLjyiVCYSzMVbHGvRb496ywTB4evDIOFTYeo1u/SlBynF4FbMzgVQmuHFm3lIsDdA69VOXCiZ/R5mzlBboCPDooo1BWgrgj/kuM1Ie/d+ylevpXmhoEsu7/j0Coq/DkxNPyzlnmXRjgtzGwNTj4ymqt4pB4lkwrR4e1Dm/VdUOdrybZJXwM9b8OOyuV7D5XzXVuEcIvXDlmhRdqiDHc6Sddjm9I=

Le lun. 28 janv. 2019 à 10:03, Soegtrop, Michael
<michael.soegtrop AT intel.com>
a écrit :
>
> Dear Pierre,
>
>
>
> > I think it is pointless to try to be consistent in presence of nested
> > proofs if
>
> > everyone agrees that it cannot remain in a finished proof (like admit).
>
>
>
> I would put it slightly differently. As I explained I sometimes do keep
> lemmas nested or at least keep my proves such that I can move the lemma
> back for the purpose of explaining why one needs a lemma with a rather
> bizarre statement.
>

I think I understand your use case but it seems more of a coqdoc
feature to me: link a statement to a part of a further proof and have
it displayed there for pedagogical reason.

> The point is that most people are using nested lemmas together with fancy
> automation, and an automation system which cannot handle the semantic
> differences which have been discussed in this thread is simply useless for
> practical purposes. So the conclusion is the same.

AFAIU nobody has ever had an automation system that handles this for
now. People just "know what they are doing" when writing a nested
lemma: i.e. "the only problems I will get when I move this lemma
outside (hint stuff, name shadowing...) will be easy to solve". Of
course warning you for these problems earlier would be nice but complicated.


> 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



Archive powered by MHonArc 2.6.18.

Top of Page