coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
- Cc: coq-club AT inria.fr, Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- Subject: Re: [Coq-Club] clone evars in destruct
- Date: Fri, 15 Jan 2021 17:00:25 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f169.google.com
- Ironport-phdr: 9a23:+ewJNxWAAGbByTH9Fw9EdgbLC9rV8LGtZVwlr6E/grcLSJyIuqrYZRWFuKdThVPEFb/W9+hDw7KP9fy5CCpYu93Y6ylKMMQVEUNc1oNOx01oKfXGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iy42O+o5pLcfRhDiiajbrNuNhW2qhjautULjYd4Jas91x/ErmFUd+hIym9kOFyekwvh7cu04JJv7j5ctv08+8NCS6n2Y7g0QblFBzk6Lm4549HmuwPeRgWV/HscVWsWkhtMAwfb6RzxQ4n8vCjnuOdjwSeWJcL5Q6w6VjSk9KdrVQTniDwbOD4j8WHYkdJ/gaRGqx+8vRN/worUYIaINPpie67WYN0XSXZdUstXSidMGZ23YZcRAOUdPOZYt4j9qEUIrRuiHgmnGefjxiZVinPqwaE21uIsGhzE0gM9BdIDqHraotXrOqkPUu66zqfIwzLMYPxK1jnw85TIcgk7rP2QR798bcjcxE8yHA3FlFWQronlMiub2uQPtGib6etgVeGxhG4jtQ5+vCOixsgpiobTh4IVzkrI+jl+wIYwK9GzVUl2YdyjEJtWtiGaNJV5Qsc8TG52oys6xbgGtoS6fCgO0pgo2xnfa/mefoWO/xnsW/qfLy1ii3J5ZLKwmQyy8U64x+P8VcS50FlEoyhKnNTSqnwA1hze58qaR/Z+8Uqs2jaC2g/S5+xAPUw5lbTWJpA8z7MyiJcev0vNEy/2lkjrjqKbcFgv9Oav6+TieLrmp5mcOpd7igH/LqQumtG/Dv8iPgcSWGib/Pyw26Hk/U3jRrVFkPk2kq3DvJ/EOMsbu6i0CBJW3IY78xuzESuq3dACkXQELF9JYg+Lgon1N13UPfz1DPOyj0yynDpq2/zKI7jsDojJI3fflbrscrdw51JAxAc20NxT+5xUB7QcLP3vVUL8sNnVAxw9Pgy6zebqDdt92Z0EVm+AB6KUMr/dvFuG6+8pPuKCfpUauCznJPgg//PujWE2mVsafaSx2JsYcnG4HvB/L0WAfXrgn84NEWkXsgc/SOHmklKCUTlUZ3a9W6Iz+Cs3B56hDYfGXoytgbqB0zmnHpBOeGxKFlSBHW3reoiEQfsAdSOfLtN7njAZVLWsT5ct1RS0uw/7z7pnIPDU+iodtZ/71th14OvTlRAx9TNqC8SSzX+CQnp7nmMNXTA23aR/rVZhxVeE1Kh0m+ZYGsBL5/NVTgc6MobRz+xkBNDoQQ3OYNOJSFegQti9ADAxT9cxzMQUY0lnAdmijxbD3zCrA7APjbCLCoY0+LrG33ftP8Z912rG1K45glY6RctPLHSqibJ79wjOHIHEiF6ZlqavdaQExiHB7maDzWyUvEFZSgF8S6vFXWpMLnfR+PTk6USKb7K0A7kjMw0Jne6fJawMStDzh1hCRfHLOdLEYmv3lX3mVjiSwbbZJojtfWQe0SHQBWALlgkS+TCNMg10TnOjpGTfDzFqGF/HbEbl8O04o3S+GBxnhzqWZlFsguLmsiUeguaRHrZKhupd5XUR7g5sFVP45Or4TtqNow07IvdZaNI5pU5bjCfX7lIseJOnKK9mixgVdAEl5xq/hSUyMZ1JlI0RlF1vyQNzLayC11YYLmGX2JnxPvvcLWygpUnzOZ6T4UnX1ZOtwolK8O4x8gyxswSgF05k+HJigYFY
Abhishek,
Your issue sounds similar to something I raised a few years ago:
https://github.com/jonleivent/ceps/blob/patch-1/text/011-coevolving-evars.md
Jonathan
On Fri, 15 Jan 2021 22:48:07 +0100
Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:
> Hi Abhishek,
>
> I don't know who would have the opportunity to implement it, a way or
> another, but that seems indeed to be a very good idea!
>
> Best,
>
> Hugo
>
> On Fri, Jan 15, 2021 at 01:18:37PM -0800, Abhishek Anand wrote:
> > eexists is very helpful in proofs because it lets us avoid
> > computing/ simplifying complex things in our head and let Coq do
> > all that and almost figure out the right answer.
> > However, the eexists implementation in Coq does not achieve the
> > full potential. For example, making cases is dangerous as it
> > requires the value on both sides to be equal:
> >
> > Require Import Nat.
> >
> > Lemma xx (b:bool): exists n, n = if b then 1 else 2.
> > eexists.
> > destruct b.
> > - reflexivity.
> > - (* cant prove 1=2 *)
> > Abort.
> >
> > In the above simple/contrived, the right answer is immediately
> > clear but it is not the case in many proofs. Is there a way to ask
> > destruct to clone some chosen evars for each case as I did below
> > manually:
> >
> > Lemma xxx (b:bool): exists n, n = if b then 1 else 2.
> > eexists.
> > Unshelve.
> > Focus 2.
> > evar (x:nat).
> > evar (y:nat).
> > exact (if b then ?x else ?y).
> > simpl.
> > destruct b.
> > - reflexivity.
> > - reflexivity.
> > Qed.
> >
> > -- Abhishek
> > http://www.cs.cornell.edu/~aa755/
- [Coq-Club] clone evars in destruct, Abhishek Anand, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Hugo Herbelin, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, jonikelee AT gmail.com, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Clément Pit-Claudel, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Siegfried, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Maximilian Wuttke, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Jeremy Dawson, 01/16/2021
- Re: [Coq-Club] clone evars in destruct, Hugo Herbelin, 01/15/2021
Archive powered by MHonArc 2.6.19+.