Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to combine tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to combine tactics


Chronological Thread 
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] how to combine tactics
  • Date: Mon, 5 Aug 2019 13:44:31 +0000
  • Accept-language: en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=anu.edu.au;dmarc=pass action=none header.from=anu.edu.au;dkim=pass header.d=anu.edu.au;arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=d5he41XfnjHZ9+ziItfbzDUcDqrItJHyiBjFqG3fkpw=; b=lcO4jDnLzA293uDfrx1i+fKNcHQEnj7uhY8pj5FUY2Eyj8GD+q9JGPnbaNKV2yqsWJpml7ipdsk0rLWZVGMdXCFGMEmCeVEUPgxRg/vxnoBeXlHeVtp7qkg8QPJasHKyt/m2+jAMVDsnv8jtx6GeeGVR730SnVITp1nA6rR4TSqDWS6ij+k+iToOh39U2xyPfNbDSK5oklmfSfaSAXe/rGe0MAhfAmoQoshZDsV7DyXjLDtMMFlUwaB1UmlysMSACgQR3shSaz6lNgoGwUVjRf4TMTZ6M6pWdqJpWybVA9Uu0A4d75rRqQiUvXqBJ8op1K8EwExbO02SiiV08bMePw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=N00lywlb/Ra4HO2hL2lt6aAmQ310P+Q+Yv1WWiMdhHV4RqL0fOKCerZrCaL1RD1pkmQkMq//ERx0pgRPUXDrbQ+RIjfC3+F+pzcg8SVVoSHcQrOxydglgU7fvWj9SRVv17iI9kpC+FeV1WiMQ2x5iOKYP8y5cAzLsWSu5Cb7oaQVuD6yvJIn9TPAKshMoqDefzUbO9y45fNMbzBpSayoLFqHHQz8OLclLCyv+deTFVX/PdHk73xV9MsnwOtYk4gpA76pG/EuMpXHnCaHeERU8VxLNyeeWLs4WFyAUGS7n8ZhrGs1lcvfWEqdKwgzPYK+1LV/e3HliupTQtJuTav8sw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:jAWVNBFF5bja1AXvbgE9QZ1GYnF86YWxBRYc798ds5kLTJ7zr86wAkXT6L1XgUPTWs2DsrQY0rCQ6vi/EjJbqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAndqssbjYRjJ6s/1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPR8caPcYdwUSmVOU91NVyNaGI6wc5cDA/YDMOtesoLzp0EOrRy7BQS0AO3g1CVIiWHz3aw6zu8vHxvJ3QI7H9IJtnTfsdL4OqMMXuCv0qbIyDXCY+lY1zjn5onIaRchofeXUL1qd8rR1FMjGB3YgVWNs4DqJS6V2/0LvmOG7ORgTfqihmE7pw1rvzSj2sUhhpPUio8byF3I7yF0zYYtKdGlVkJ3fcSoHIZSui2AKod7QccvT3t2tCs017EKoZC7czYJxZg7whPSbv+KfoiH7x/sUeuRLzN1iXBrdb+6mhm+7VWvx+75W8ap1FtFsDRKn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lYLE86iKTXN4MtzqctmJURv0nPByj2l17og6OMcUUk5/So5P/gYrX7oJ+TKpV4ihnkMqQphsywH/g3MhQPX2ic/+Swzrrj/VDlQLVOif02larZvIrGKsQco661Gw5V0oA95BajFzqr38gUkWMaIF5Zeh+LlZXlNl/MLfziCfqyg0ygkDJxyPDHOr3hDI/NLn/GkLr5ebhy9VRcxxQ2zdFf/Z5aBKsOIfzoWk/2stzVFQU2Mwqpw+r9Ftpyy54eVXiVDa+EKK/Sq0OH5vozI+mQY48YoCryK/885/L3kXA5nUIdcrKy0JsMaHG4G+xmLF+DbXrthNcBC2YKsRAkQOzkkl3RGQJUMjy5WLt57TUmAqqnC53CT8ajmvbJiCy8B9hdYn1MIlGKC3bhMYueDaQiciWXd+1siDEBRPCNQpA60hfm4C330bdiP6z48zIDspTL3d5ooeDfiFc76GonXIymz2iRQjQszSszTDgs0fUn+BAv+hK4yaF9xsdgO5lL/foQCFUzM4OawuBnTdnvCFqYL4W5DW2+S9DjOgkfC9c4wtsAeUF4Qo/whxbemSemHvkciu7SXcFmwufnx3H0Yv1F5TPG2a0m0wZ0a/Z0bTTjvZ8ksg/ZCsjOjlmTkLuseeIExinR+WyfzG2I+kZFTAp3VqaDVncaNBLb
Further to my previous messages I have experimented some more, and find that

induction H ; (eapply derI ; [ NLrule_I | idtac]).

does work. Ie the parentheses are needed, and make a difference, in
this case.

(contrast tac1 ; tac2 ; tac3 where parentheses don't make any
difference, though I would have expected them to).

Cheers,

Jeremy

On 8/5/19 11:27 PM, Jeremy Dawson wrote:
> Hi Laurent,
>
> I'm guessing you mean something like this (but not exactly)
>
> induction H ; (eapply derI; [apply: NLrule_I | idtact]).
>
> but not exactly, since it gives this error
> > ^
> Error:
> Syntax error: '<-' or '->' or [constr_with_bindings_arg] expected after
> 'apply' (in [tactic:simple_tactic]).
>
> I've never seen the "apply:" construct, can you clarify?
>
> Thanks
>
> Jeremy
>
>
> On 8/5/19 3:22 AM, Laurent Thery wrote:
>>
>> If you are sure that eapply derI always generates 2 subgoals,
>>
>> you can of course do (eapply derI; [apply: NLrule_I | idtact]).
>>
>>
>> On 8/4/19 3:57 PM, Jeremy Dawson wrote:
>>> Hi,
>>>
>>> I have a tactic eapply derI
>>> which when applied to a goal produces two resulting goals.
>>> Of these two I want to apply the tactic NLrule_I to the first one.
>>> The tactic induction H results in 7 goals.
>>>
>>> So when I try
>>> Proof. intros. induction H ; eapply derI ; [> NLrule_I | ].
>>> I get the error (not unexpected)
>>> Error: Incorrect number of goals (expected 14 tactics, was given 2).
>>>
>>> When I try
>>> Proof. intros. induction H ; (eapply derI ; [> NLrule_I | ]).
>>> I get the same error, which I don't understand at all
>>> (though the fact that putting in parentheses doesn't have the
>>> expected result has been discussed on this list previously).
>>>
>>> When I try
>>> Ltac derI_NLr := eapply derI ; [> NLrule_I | ].
>>> Proof. intros. induction H ; derI_NLr.
>>> although sometimes defining a tactic using Ltac
>>> has previously given me what I want and expect,
>>> in this case again I get the error
>>> Ltac call to "derI_NLr" failed.
>>> Incorrect number of goals (expected 14 tactics, was given 2).
>>>
>>> How do I apply eapply derI to all goals, then NLrule_I to
>>> the first subgoal resulting from each instance of eapply derI?
>>>
>>> Thanks,
>>>
>>> Jeremy
>>>

Archive powered by MHonArc 2.6.18.

Top of Page