coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Apply tactics in either hypotheses or goals

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Apply tactics in either hypotheses or goals
Date: Sat, 21 Dec 2019 07:04:42 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f51.google.com
Ironport-phdr: 9a23:gXJNcxb927rHUIpN3b/VFQT/LSx+4OfEezUN459isYplN5qZoM67bnLW6fgltlLVR4KTs6sC17ON9fq5BSdQvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6txvdutQZjIdtKas8xQbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2upxJxzY3abpyLOvViZa7SZ88WSHBbU8pNSyBMAIWxZJYPAeobOuZYqpHwqkUOrRukBAmsH/7kxDFSiX/zxq0xzuMsHh3G3Aw6HtIOq27Yo8jvO6cXSuC51q/IzTHYYvNZ3Dfy8onIchQ7rf6QWrJwdNPcxE8yHA3GllWdsZLpMy+R2+gXsGWW7/BsWfyyh2MlsQ18oiWjy8ExgYfTnI0V0ErL9SBhzYY1O9K4TEl7bMahEJRKtiGaM5J6Qt05Q211oSo6xL0LtYOhcCgFz5QnwBHfa/iZfISS/h3jU+ORLS95hHJjZr2/mw6//Va8xuD4TMW501ZHojBbntXRtH0BzRze5tWfRvt45Eih2DKP1w7J6uFDJEA5jbbUK547wr4xjZofq1nMETXzmEXtlqOWcEEk9/On6+TieLrmp5ucO5VohQH5N6Qigta/DvggMggSQ2ib/vyx26Hk/U3gWblFkvk2krTCv53BPsQapqu5AxdP3Yo56ha/CS2m0NUCknUdIlJFYkHPs4+8MFbXZfv8EP3311+riXJgw+3MFrznGJTEaHbZxuTPZ7F4vmVc0gsohfxW4okcXroBOvPoHEP4sceeCBsRPAm9wuKhA9J4gNBNEVmTC7OUZfuB+WSD4fgidrHVNd0l/Q3lIv1g3MbAyHowmFsTZ66shMJFZ3WxH/AgKEKcMyO134UxVFwStw97d9TEzV2PVTkJOiS3VqM4oy8gUceoUN6FSYeqj7iMmiy8G88OPzwUOhW3CX7tMr68dbIUcivLe51ulzUFUf6qTIpzjRw=

Dear all,

Sometimes I create a set of rewrite rules like

Ltac my_rewrite_step
:= match goal with
| [ |- context [ pattern1 ] ] => rewrite something

| [ |- context [ pattern2 ] ] => rewrite something_else
end.

Ltac my_rewrite := repeat my_rewrite_step.

This can be very useful except that there now is no easy way to apply this tactic to hypotheses instead of to goals.

Sometimes Hint Rewrite/autorewrite works but it does not seem to always fit the bill because the tactics in the match may sometimes be more complicated because the the theorems used for rewriting generate more hypotheses that I also want to solve automatically. I.e., maybe one of the tactics is actually 'rewrite something; [|do_something]'.

So my question is whether there is a way to be apply to apply these kinds of tactics to either goals or hypotheses at the users choice without duplicating all the cases.

Have a nice day,

Chris

[Coq-Club] Apply tactics in either hypotheses or goals, Chris Dams, 12/21/2019