coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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.

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