coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] proving a lemma in a proof
- Date: Mon, 28 Jan 2019 09:02:49 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga11.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:l5KyqRQl0nspfwalzp1vNsL3Xdpsv+yvbD5Q0YIujvd0So/mwa6yYBSN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO+FzcbnBcd4eX2dNQtpdWi5HD4ihb4UPFe0BPeNAooXzulUOqgWxBQawBOP1zT9Inmf61rA93eQgDQ7G3BYvEMwKsHjasd74M6ISUeGpw6nI1zrMcfdW1S3m6IjPbB8hru2MXah3ccrJ0kQvFgXFjkmOpozhJT+ayuMNs22C4udmSOmhhWknqwRrrTiuwMchkojJhoQJyl/a8SV12ps6KsO+RUVmYtCkCINduzyeOodoWM8vQ2FltDw6x7EYo5K2eCYHxIw6yxPeZfGLaYaF7xz5WOqPLzp1gGhpdK+8ihqv6USs1+zxW82u3FpUridIncPAum4X2xHS6sWKTOZ28F271jaVzQ/T7/lJIUAqmqrfLJ4s2rswlpUJvkjeAyP6gkT2jKmKdko6/uik8fjoYrLjppOENo90jB/xMrg2l8CiBek0LBICUmib9Oim1LDv41f1TbFEg/Eul6nWqpHaJcAVpq6jBA9V154u6xO+Dzi60NQXh2cILFZfdBKciIjmJV7OIOziDfe4m1ShizZrx/baPrL/BpXBNGTMkLDkfbpl8U5T1BIzzcxD55JTErwOPPXzWlbouNPECh85Lhe7zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK1v7Pn3yHQ9hFU1fK+z3JJRZmryVqBtJFzcan7xiP8AF30Lt0wwVrq5pkeFVGsZXHG/UL4m4Sl/QKenBofKS4TnyOiE3Sy7F5BSIHtBB1+QC3DwX4SCR/oILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3EgWCLU2xw2GgPQm1vhfwtkQlG0l6GlJNArblAD9UKvqFIVBs3MdjXyOkoU4mvCDKERc+ATROdevvjATw1SYtukdoBah8kXdSkkh3HmSGtBu1Nmg==
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.
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.
Best regards,
Michael Intel Deutschland GmbH |
- Re: [Coq-Club] proving a lemma in a proof, (continued)
- 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, 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, 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
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
Archive powered by MHonArc 2.6.18.