coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Existential variables or holes in Lemma types

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Existential variables or holes in Lemma types
Date: Fri, 18 May 2018 10:21:00 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:i3ygaRdMMJwlT5LCFBCKaauplGMj4u6mDksu8pMizoh2WeGdxcu9YR7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM383zZhMxugqxVoh2hqQBwzYnbb4yOO/pyYrnQcMkASGZdXMtcUTFKDIOmb4sICuoMJeJWr47nqFQSrRu+BAysD/7yxz9SmHD23LE60+I/HgHcwQctGNcOv27VrNXxL6oSU+e1w7PUwjXDbvNW3C7x55PSch8/oPGMQbRwftTLyUU1CgzKkEydpIr4ND2b0eQNtnKU7+tmVe+3iW4nrBt+rSSvxsctj4nFn5kaykra+iV43IY1I8O3SFRhbdG5DpRdsTyROYhuQs46Xm1luic3xqcCtJKhYiQG1ZoqywTCZ/GJfYWF5A/oWvyLLjdinn1lfaqyhxas/kikze3xTsm030hQripAjNbMrWoB1wfN5cidVPty4F2h1iyK1w/J8O1LPF47mbLaK54n3LEwioIevVnBEyL3gkn7iLWaels59uWm8ejrf7vrq5GEO49xkA7+M6AumsKlAeQ/NwgDR22b9v691L3n5kD5QrJKgecqnanZsZDaIN0XqbWjAwBL04Yj9xC/ACm80NgCgHYIMkpJeAibgIjxJ1HOPPf4AO+jjFSriTdn3uzJPrn8AprWNXXDi7fgfbNl60FG0gYzzNZf54hVCr4bOv7zVFXx55TkCUoyNBXxyOL6Av180JkfUCSBGPy3KqTX5H2P7+kvIuzETpUYuSr7JuJts/vnjHsRm1gUdqmo2N4dcn25AvJrOQOVbCy/0Z86DW4Ws19mH6TRg1qYXGsLPifgb+cH/jg+TbmeI8LGT4GpjqaG2X3iTJ9Rb2tGC1XJG23ldpmCVu1KZC/AeJY9wAxBbqCoTsoa7T/rrBXzkeM1LO3d8S0ZsNfpztV0++vej1c++G4sVpnP4yS2V2hx21gwaXo20aR4+xUvylqZ1KVjxedVD8Je/fpMW0E2OMyEwg==

Hi,

Am Mittwoch, den 16.05.2018, 18:12 +0200 schrieb Pierre Courtieu:
> I like this trick. Crafting induction principles is an efficient way to
> ease proofs.

I wrote up the trick on my blog:
http://www.joachim-breitner.de/blog/740-Proof_reuse_in_Coq_using_existential_variables

Looks like I soon have to introduce a “Coq” category there :-)

Cheers,
Joachim
--
Joachim Breitner

mail AT joachim-breitner.de
http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Existential variables or holes in Lemma types, Joachim Breitner, 05/16/2018
- Re: [Coq-Club] Existential variables or holes in Lemma types, ikdc, 05/16/2018
  - Re: [Coq-Club] Existential variables or holes in Lemma types, Pierre Courtieu, 05/16/2018
    - Re: [Coq-Club] Existential variables or holes in Lemma types, Joachim Breitner, 05/16/2018
      - Re: [Coq-Club] Existential variables or holes in Lemma types, Pierre Courtieu, 05/16/2018
    - Re: [Coq-Club] Existential variables or holes in Lemma types, Joachim Breitner, 05/18/2018
  - Re: [Coq-Club] Existential variables or holes in Lemma types, Joachim Breitner, 05/16/2018