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: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proving a lemma in a proof
  • Date: Fri, 25 Jan 2019 07:55:24 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:DRstTRVU8SFE1jxuISzmE7U3lbXV8LGtZVwlr6E/grcLSJyIuqrYYxeGt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/KlMJwgqJVrhGvqRNxzIHbYp2aOvVlc6PBft4XX3ZNUtpfWiFDBI63cosBD/AGPeZdt4Twu0YBogG7BQKxGu7vyjtIhn7u3aIg1+QuCxzN0Qs6EN0TqnvUqcn6ObwOXuCu1qbIzDHDY+lT2Tf89IjEaA4uruyRXb9pd8fa1EohFxvdg1mNt4DoPCmZ2+oRv2SB8eZsT/yjh3M7pw1poDWj290ghpfHi48b0FzI6CV0zYQvKdGmVUJ2b9ipG4ZKuS6ALYt5WMYiTnlouCkkzr0Gvoa2fC8XyJQ7yB7fbP2Hc46H4h76T+aRPS13hG5/d76lmxmy6lKvyuz4VsWu1VZKrzZFnsPSuX8Qyhzf8smHSv1j8Ue9wTuDyh7f5+JeLU06iabXMYAtzqQumpYOrUjPBir2l1/3jK+SeEUk4O+o6+H/b7r8u5CTLYp0hR3lP6sygcywG+U4MgwUU2ie+OS8yKfv8lPkT7VXlvE2iLXWsIjGJcQHoa60GxNa0oE66xqmEzim1MkYkmIcIVJeeBOHipDpNEvULPD5C/e/mVWsny1xy/DIJL2ySqnKe3PEifLqeat3w09a0gs6i95FtLxODbRUCf76XwfatNjZFhY9OkTgyuruDd5V3ZgXWGbJB66Fdq7erAnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCOx0NwaGGYO+A8/UKrnhEDQCGcPNUb3ZLo143QAMKzjFZ3KH93/i6eI3SP9G5xKIG1KFwLUSCq6R8C/Q/4JLRmqDIphnzgDDuDzTJI92havsgC/0KZuMuOS8TYRtJal0dlpoeDfiENq+A==

On 1/25/19 3:24 AM, Soegtrop, Michael wrote:
Can't we say: "A nested lemma is only supported if it's effect is
indistinguishable from the same lemma in front of the outer lemma"?

That effect is harder to support with hint commands, which at least in my uses often follow nested lemmas.  In principle, one would need to go back and check all [auto] invocations!  I'm actually fine with a semantics where add-lemma effects must appear the same as with top-level commands, but where hint state is allowed to be mixed up.




Archive powered by MHonArc 2.6.18.

Top of Page