coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to combine tactics

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] how to combine tactics
Date: Sun, 4 Aug 2019 13:57:48 +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=+a3B/c1RB+X81nEPNekRfsUmzqE8OY6m2Ev0LdI51SA=; b=oS3emV/XJMmEp/hA3tXw9bXQyNOzmWpIToVDg5XvNN9zGk9uKNPtFSmouyJBY3nmDZAySuV/8Lc7lg1YVunXjXzHlvRMDHBcTAbQCq5x4vTXf+6dVoFy0yrdY4V7GZ4G206ME4XSpK0YJx1u/9LVmb+GjZb9gHGBuIQJ+cWg0nNCSHHCi6gxXOKgEH0+3eg2FNM0LmrP7bca7b7M21uepThE3xZXPn+UMtro6K2OUrIrmGbQqVEfngH/vNSX3fbKsDHlUzYJux1J5x/FMSUh6787f46vfl9BaOQ4+2GRbFUssDzQxBGaGTOWIdtAy/2a/9L5y8QmEZERKfkw0W7y4g==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=QLqaZmZNTx+Y+8fEJ14z1FsBG/ppf7kG2jTs96aBSoeV0nBV0gpG2MY0Uf0sb7HxJJD3e30TRNhbEFPQhOXxRTP6M4gTKK9hJYpdtNjJtFlTJZB8btdQ4Kw5+3alQHUKucNLJhyoLY3VcatXsQQP//CqGHcrxZWpWJarjJDNLrS5HC3yj7332HyVhI8oXLcLDUjWsNv42oEGNbijEfGZA/ZizNAx2KewNLNGawVlg4x+ZTFbjkpJMjiUeUUKOn5/260Hw1L8C/7INCJGNw19uBxaYgaxy5D6qe7DJf01AibTuYDXLKl+2rJpWNe32qz9dKRpcY/dELVXsPBeZVEzPQ==
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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:c7EcaRR0B/zdR1O0d7C5z/yOSNpsv+yvbD5Q0YIujvd0So/mwa6ybBKN2/xhgRfzUJnB7Loc0qyK6vqmADRdqsnZ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAiooQnLq8UanYtvJqkzxxfVv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRxhzYDJfIGbOvlwfq3fctMbWWVPUcleWjddAoyndYYDE/YNMfpaooT7ulAArQG+BQ6pBO73zjFHmGX20rM/0+UhDArI0hYvHtwVsHTTqtX+KaAfX+Srw6nS0zrDavNX1S3z5ofSfBEhuvaMXbRrfMXLz0kvChnJgUuNpoz4JT+azPkNvnGd4uF9Vuyvk3Yqpg5trjS128sglovEipgIxl3K9Ch12ps5KcOmREJjfNKoDodcuzuHO4Z0WM8uXmJltSIgxrEYt5O3YTAGyJo5yBPcd/CKdo2F7xHjWeueLjp1gXxldba9ihu89EWv1/HwWdS33VtPsyVIlsfDuW4L2hfO8MaIUOF98V2k2TuX1wDc9OVEIUcsmKfHJZEv36I8mocKvUrEESH6hVz6jKiNeUo64OSo7PnnYqn9qZ+bKo90jBzxPr42msylBuQ4LhYBUHSH+eS9073j+1f1QLJXjv0qlqnZt5faJccBqqGlBA9V154v6xe5Dzi4zNQVhXYKIE5fdB6ak4TkOUvCLO32APq+mVigjSlny+7eMr3kGJrNL3zDkLn7fbZ67k5R0A49ws5F551KD7EAIOj/VEHru93WFR85NAq0zv39B9V7y4MSQ3yADbKEMK/Iq1CI+/ojI/OQa48NpDb9N/8l6ubygn8+gF8RZLWm3Z8KaH+jBflmOEWYYX/0gtgbC2sKvww+TPbriFKYSzJTaWyyDOoA4WRxA4W/SIzHW4qFgbqb3S79EIccLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO2DRpUs0ADmmAbl0L1hZr729zcVsIOl+NFq/OrVvRg06Hp5A9nb2nzbHDI8pX8BWzJjhPM3mkd60FrWifEp0cwdLsRa4rZyail/MJfdy+JgDNWrAFDIeMrPRVq7BNy7U2hoEoABhuQWakM4IO2MywjZ1nPwUbYTivqGCIFy+7+OhyGsdfY48G7P0ewat3djQsZLMjH51IdCzFCKQqvkygCenavscrkA1inQ8mvF1XCJoExTTA93V+PCQGwbYUzV69/+4xGbQg==

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
- 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