coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] proving a lemma in a proof
Date: Sat, 26 Jan 2019 15:20:08 +0100
Authentication-results: mail3-smtp-sop.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-f53.google.com
Ironport-phdr: 9a23:X6prKhcK6G1PSMXbHXNl1M5GlGMj4u6mDksu8pMizoh2WeGdxcu4Yx7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM2/2/Xhc5wgqxVoxyvugJxzJLPbY6PKPZzZLnQcc8GSWdDWMtaSixPApm7b4sKF+cPJ+dYoJfnp1sUsxS1GBehBOTyyj9Smn/23LM10/k8GgzBxAwgHswBsG7OrNrrLqsdTee1zLTSzTXfbvNZxyr95ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHmMTONzukBrXSX4u56We+si2MrsRx9rzmuy8s2ioTEiIQYwU3e+ypj2oY6P9i4RVZ7YdG6FJtQsDmXN45sTcMjR2FkoSc6yrobtZKicigHyJoqywTQa/yAdIiI7RbjW/iLLThkg3Jlfaqzhxe08Ue+1u3xTte43EpOoyZfkdTBtmoB2wHS58WGUPdw/kms1S6K1w/J6+FEJU40lbDcK54k2rMwjpsTvlrZHi/shkr6lrOZdkI5+uiy9+TnY6vppoKHOo97jwHxKKUumsilDeskNQgOWnCX+f6g27374U35XLJKg+UqnaneqZDWPNgUpqqkAwBOyYsj8Ba+DzK+0NsCh3UHLVRFeAiGj4fzIV3OLur4Xr+DhAGnly4uzPTbNJXgBI/MJz7NiuTPZ7F4vnZdxRApwJh04I9OFrAMPbqnQk78rsbVSBQ+Lhaowuv6INp434IaH2mIB/nKY+vprVaU67d3cKG3b4gPtWOlcql317vVlXY83GQlU+ys1JoTZmq/G60/cUqcaHvoxNwGFDVT51ZsfKnRkFSHFAVrSTOqRatlv2M0DYunCcHIQYX/2OXcjhf+JYVfYyV9Mn7JEXrscN/ZCfIFaSbXI8g41zJZDv6uTIgu0Rzovwj/meJq

Hi,

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). It should just be clear that when moving out an inner lemma strange things can happen. Exactly as (but to a wider extent than) when replacing an admit by a real proof.

Le ven. 25 janv. 2019 à 15:10, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Adam,

> That effect is harder to support with hint commands, which at least in my uses
> often follow nested lemmas.

Indeed for hints it is trickier

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
- Re: [Coq-Club] proving a lemma in a proof, Gaëtan Gilbert, 01/23/2019
  - Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019