coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Laurent Thery <Laurent.Thery AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] proving a lemma in a proof
- Date: Tue, 22 Jan 2019 13:25:09 +0100
- Autocrypt: addr=thery AT sophia.inria.fr; prefer-encrypt=mutual; keydata= mQENBE3a3V8BCADTeORKU7I7UmBBcs4VhSCq1IgKD8vdmdrGAlF3IJSFng7Fk8+MgS2gWYcS Ukf5t+rjNM3Z6brfYXc1naZlf2JPGHvAGiz8+TkXL+/ZA6+gAoIKy/iKyD+hCD8m92WH3rPH vCX6EJ44FEI7gUJ37GlTjvuP0I55vaFcwEg8nDgkALaCJvrSHtePuPKR1Q+9q2dgR7fTObal HYGMAsgT6k6n2ofe4Q6VFRLJhruU02qAfV5zgIoa3xgrTwSr4RRDILHttAw7EN6aLG6JycJ7 sPsPsiQzrd/tFsNbiHYeojJCkU2pDSQ3pBtXAJL/z2pMWTeTXvA60l9w0sDO7M3mkC3vABEB AAG0J0xhdXJlbnQgVGjDqXJ5IDxMYXVyZW50LlRoZXJ5QGlucmlhLmZyPokBOAQTAQIAIgUC TdrdXwIbAwYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQHHaWvRTi0tpIgggAnSUYcU2N uchXkGGwmPuLmvSUMiLkyFPs9GF2YF1ONOuJtpnQMcpsseCkcmIjESz0h5OpknpyraUXvbh0 ZdFqaLC2E+GyV8/YQi71wSsTPgWP450u0XUt0ysjwkKW6aIxIhSzrtgNp4E6w5KzXVJxA/yM V5RNFHg/5uifgfv4b7xaGHV8L93NbSvedk1O7yje5Hqgfab0t6J5Kf0M3sG+pB3gEkDVK9B7 +0fhe7/5u1Nj5HoLWid8UNZfFzJzb18Xe2ckzNye0KdDtQFac8qGUzhLbEYt3ScYjRYTq9/d V4Cin39j7Oo64Nk71iiLBISyuk0Q9D+Jq7nwwcQr/R8s1rkBDQRN2t1fAQgA7H6aX6BfdO/X Vlf4EGEoyFQ5u/JDe+giIHWSS34YWDWVUYyp320CrAYAkh9lQ1Nvh1tsmgiUh5xnY7wY0tOi wJSm94XlYAmHrddmWVNXRn09GvZJhfI2LdVBg3oxPfc8+bV+Hz83z/5BMPLOogxB22QMPJ6e iD2EsUMPNsuCVQ8WNo6ZmueuuYe7vEUXLYdRXNumJJgekEuG/q1BD4xgfzWpWfUODm6WygWZ oov50DomcDcAHW03bgnHlqnYu20Qg00GqgR3FKlORTvnOxD5TMCXe+eLUxkQfvnjbIPhtrnJ hgJMKVkRBEoaQ/XA4FdvxloInYPbqxNZ72yd09BbewARAQABiQEfBBgBAgAJBQJN2t1fAhsM AAoJEBx2lr0U4tLaWNQH/2/fIaF9ngbKPBJbDxYa7glJuCfamJgy3R8mJ//VYsS4RbdroSX3 29EgWlTx2reu1b4C5n5k7l4KpLgsRIc3bLUasGv15nf8BqmKIMulidzsxJv86S2imY/0870Q NOiO9SElHE7/2q4J1m2ew77SegiqGVWHl6Zs+4ROfOILTy24o26BQMAZhPX7jEs04Atv6yjw OUIPbzFO+XRuKqkBwHn9S8+GQelT0Gh84Dc5D2jIF0+kWY7uHqe2O+2LPfgO2CYhqmVfr/Ym mZv2xUyhJ7gui2hYaggncQ96cM2KhnKlgMw8nStY0GTqVXLEjPYblz8mqtF8aBPRSk/DjjrF QeI=
- Openpgp: preference=signencrypt
Hi,
On 1/22/19 6:08 AM, Jeremy Dawson wrote:
> So my question is, having decided during a proof that a particular lemma
> would be useful, how to I prove and use it?
If it is a local assertion that you will use only inside the proof,
you can use the tactic have (ssreflect) or the tactic assert (standard
Coq) to add it to the context.
If it is a global lemma, good practice is to abort the proof. Prove the
lemma and then replay the proof.
- Re: [Coq-Club] proving a lemma in a proof, (continued)
- Re: [Coq-Club] proving a lemma in a proof, Andrew Appel, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Jim Fehrle, 01/22/2019
- 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, James McKinna, 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, Gaëtan Gilbert, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Jeremy Dawson, 01/23/2019
- 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
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Ralf Jung, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/24/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
Archive powered by MHonArc 2.6.18.