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: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] how to combine tactics
  • Date: Sun, 4 Aug 2019 17:56:05 +0000
  • Accept-language: en-CA, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1;spf=none;dmarc=none;dkim=none;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=S8fKv6G/OWrLpdkWZBQPMi6FgNEjFfmvyFzQUavjm30=; b=NR94cav2D1NOfmRqrXE437AVOCUsQv/06M5O1ctG/Nn4c6oE1VGqCTggpWamC8pWqJjPZk5IFpZBoS6h8tZakckrQDfN28WDJeSj/DR0+h6aQyKgPCLltRAi1J4gGttLH6YJpcuLogZOXsDjzdFFylqLbtejGyweLeV++95XuPJ2ez7prNsOe/Zraqhh1x+qYWmK2hBlj48xBadLY1tkxlsv31eElj5HDQPNbRfPZc1EO3MlD1yH/bdVEsVtZPr23mPsnS4J39DmXuRF4R3P7PBK8tLq3b1HICcM0tCgHXQTQ1X8s6K64NlDbB4SCknQk3L1T5OIuubqcmI6CWyo4Q==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=gyc3XPWDqkVSMC6L65u6mTsfx9dSWyJcZ7A4ABMneXQx++z9bU2/DcdjKUQmNQ1sKRIls72ooJed7s1UPSJ5AkGLsS9YYE0JUItyBmtP78qPdyMO06eFi06nnHlu3q//nLBWymZgG9x8D3Ds3OuZSNgOfU9FHsyYUe8h2nefLh2Y+sB9JdkvtRRj3lT2ALwIuIR6PAz/QtZembSHFpZEFH74hqXqc+ZzEDXoft/v/2W82usDD84r63BV2CPwTvXm+aYMFKgpdNmWu8KOvLMYtaQofrNi9kViFRiGVxKiYY0HiHlEZc4HD2dg5W6tByEeeSYT5ZUJs4B6V0egbu99lg==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-CY1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:QPuYyRV3ZF4xl9WSEk1LkhDz8BjV8LGtZVwlr6E/grcLSJyIuqrYbRCDt8tkgFKBZ4jH8fUM07OQ7/m6HzVYvN3Y6S9KWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sBvdutMLjYd+Kqs9xQbFrmZKdu9L2W5mOFWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8t/gr9GoBK6vxxw3ZLbYJ2bOvp5e6PSZ9IaRWxcVcpVWCFMBoawYo0SBOQDIOlYtZHwqVsQoxWjGQmiCuDhyjFKiXDq0qI3yP4uHR3a0AE6A94CrHTZodPoP6kSS+C1y6zIwC3HYfxMwjf9747IeQ04rf6PXbJwdszRyUYyHA3YjlWft4rlPzyM2u8QsWab8vdrWOWhi2E6qwFwoyOvytkwhoXUmo4Y0VDE9SJlwIYwP9K4SUp7bcS4H5tXsiGXLo17Sd4sTWFvvSY10LwGuZijcSgLzpQn3R/fZOadf4iG+BLvTOmRITZkhHJlZbKwnAy+8UmnyuD6S8K6005KozJKn9XQrHwA0wLf5tKIR/dn/0qs1y6D1w7N5exHPUw5kK/WJIU9zbEumJcetEfOEy/2lUjyiaKbdEEp9+u15OniYbjpupGcOJJyhwrjKKohgNa/Dv49MgUWX2iU5+C81Lr78EPhXLhEieE6nrfAvJ3EJ8sXu7e1AwhO3Yk98Rq/CCqm0MgDknkAMVJFfg+Ig5LxO1HUJ/D4EemwjEiwkDdqwPDGOKftApLQLnjflLfherF9601GxAUvytBf4opYCrAHIP3tRk/8rNPVAgMjPwGw3errEtpw2pkfVG+BGqOZNbndsV6M5uIhOemMY4oVtS7zK/c45/7vjGQ5lUEBcaW0wZcac3C4HvN6I0Wce3Xsg9MBHX0WsQo5SezmkEeCXiJLZ3auQ6I84Sk2B56hDYfaX4yinLiB3DqgEZBNfWBHClWMEW/yeImeWvcMbjiSIs57nTAeW7ihUdxp6Rb7/gT90v9sKvfe0iwer5PqktZvraWHnhYrsDdwEs610meXTmgykHleFBEs26Uqg0VmzVHLlJp4hPpXXedT6vVGF08aKNaIweB6GcuoAluZVteOVFOvQ9HgCjY0GIFii+QSalpwTo3xxivI2DCnVuNEzuDZNNkP6qvZmkPJCYNl0X+fj/shiEUjS8pLc2ahg/wnrlmBN8vyi0yc0p2SW+EZ1S/J+n2EyDPV7kFfTAt5UKGDVncaNBKP8IbJo3jaRrrrMowJdwtMzcnedflsQ/ix1xBtda6mP97TJWWsh223GBCEgKuWa5bncHkc2yObD1UYlwcU/jCNMg1sXyo=

Hi Jeremy,

have you tried

eapply derI ; [ NLrule_I | ].

notice that > is dropped. you can read it from the refman: https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch
The tactic language¶. This chapter gives a compact documentation of L tac, the tactic language available in Coq.We start by giving the syntax, and next, we present the informal semantics. If you want to know more regarding this language and especially about its foundations, you can refer to .Chapter Detailed examples of tactics is devoted to giving small but nontrivial use examples of this ...
coq.inria.fr
Variant expr0 ; [expri*|]

This variant of local tactic application is paired with a sequence. In this variant, there must be as many expri as goals generated by the application of expr0 to each of the individual goals independently. All the above variants work in this form too. Formally, expr ; [ ... ] is equivalent to [> expr ; [> ... ] .. ].

I suppose this is what you want.

Thanks,
Jason Hu
https://hustmphrrr.github.io/

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Laurent Thery <Laurent.Thery AT inria.fr>
Sent: August 4, 2019 1:14 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] how to combine tactics
 
Hi Jeremy,

the selector you try to apply seems to be work globally and not locally
like you think. As a ssreflect user,

https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html

I will use the ssreflect tactical first to solve your goal

================================================

From Coq Require Import ssreflect.

Inductive Seven := one | two | three | four | five | six | seven.

Definition  double (x : Seven) := x.

Lemma derivI : forall (n y : Seven), y = y -> double n =  double n ->  n
= n.
Proof. now trivial. Qed.

Ltac NLrule_I := trivial.

Goal forall h : Seven, h = h.
Proof.
induction h; (eapply derivI; first NLrule_I).

================================================================



As I usual

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