coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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, 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, Soegtrop, Michael, 01/23/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
- 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, Christian Doczkal, 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, Jan Bessai, 01/22/2019
Archive powered by MHonArc 2.6.18.