coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 ofexpr0
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.
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
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
>
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
>
- [Coq-Club] how to combine tactics, Jeremy Dawson, 08/04/2019
- Re: [Coq-Club] how to combine tactics, Laurent Thery, 08/04/2019
- Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/04/2019
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/04/2019
- Message not available
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Fabian Kunze, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Li-yao Xia, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/06/2019
- Re: [Coq-Club] how to combine tactics, David Holland, 08/15/2019
- Re: [Coq-Club] how to combine tactics, Pierre Courtieu, 08/20/2019
- Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Re: [Coq-Club] how to combine tactics, Laurent Thery, 08/04/2019
Archive powered by MHonArc 2.6.18.