coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] goal selectors; tactic expressions
- Date: Thu, 24 Jan 2019 04:35:56 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.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:iFelXx+sBNZxP/9uRHKM819IXTAuvvDOBiVQ1KB20+wcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZis1sg6xUrx2svAB/zJXObY2JKPZyYqHQcNUHTmRBRMZRUClBD5u4YYQRFeoOI+NYrongrFUAtxS/CxKsBOTpyjRVgXL42bM10/4/HgHD3A0sBdwAv27ardXuM6cSV/u4w7POzTXedf9Zxyry6JXSfh87vPGBRLR9etffx0koEgPKlFSQqYr9MjOU0OQNqWmb4PB6WeKhkW4qrRx6rDu3xso0hYTFmpgZxk3Y+Sh72oo5ONO1RU9hbdK5DZdcqjmWO5Z2T88+WW1kpjo2x7MctZKlYSQG1I4rywPRZvGDa4SI7AzsWeWNLTp9gX9ofLGyiA29/EWl1+HxWNe730tPoypLjNbBtWwB2hnN5secRPtw8UGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIevFjNESHrhEn6kbaaeEIr9OS18ujnZa7pqYGGO49zlwH+Lr8hmsuiAeQ+LwcCRXCb+f671L3/40L2XKlKjvwxkqnfqpzaItkbprK9Aw9S1YYj6AyzACuh0NQdhXUHLVRFdwybj4XxNFzCPOr0Aeqjj1muijtn2v7LM7z7DpnQM3TPja/tfbNn5E5dzAozw8pf55VRCrwZJPz8RFXxu8LdDh45KQC6zfzoCdtm1oMZX2KCGbWWMKXPsVOS+O0gPvSMaJUPtzbgM/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1faK2z7+FZlLbEhHDEqNGDHmbc/MD/wLcWeZJtJruj0CT7moDYE7g0KArgj/nphqNOfR62U0vI340949s8/ejxw35HpYBtuG1GelRmdp2G4EWnk/wfYs8gRG1l6f3P0g0LRjHttJ6qYRC1ZoBdvn1+V/TuvKdEfEd9aNRkyhR4z8Uzg3U5Q8z8JIalsvQoz+3CCG5DKjBvour5LOHIY9q/iO1n7sYctx1jDPyft51gR0co50LWSjw5VH2U3TCorOzxrLvpuRLf1Z+QOUsWCJwCyJoV1SVxN2XePdR3cDa0DKrNP/oETfU7upDrdhOQxEm5eP
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
Hi,
I'm having difficulty with the description of the tactic language in
https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html,
regarding goal selectors
Currently I have two subgoals, and a tactic called solve_eqs defined
using Ltac.
At the present point,
repeat (2 : solve_eqs).
gives the message Syntax error: ')' expected after
[tactic:tactic_expr] (in [tactic:tactic_expr]).
repeat (only 2 : solve_eqs).
has no effect
2 : solve_eqs.
solves goal 2
After backing over this (ie we're looking at two unsolved goals)
the following two attempts give the same syntax error message as above.
repeat (only 1 : solve_eqs || only 2 : solve_eqs).
repeat (1 : solve_eqs || 2 : solve_eqs).
repeat ((only 1 : solve_eqs) || (only 2 : solve_eqs)).
gives Error: No such goal.
The following two just do nothing
repeat (only 1-2 : solve_eqs).
repeat (only 1-2 : try solve_eqs).
(and, by the way,
1: solve_eqs. does nothing, but
2 : solve_eqs. 1 : solve_eqs. solves both goals)
how do I write a tactic to repeatedly apply solve_eqs to goals 1 and 2
until either both are solved or there is no further progress?
Thanks
Jeremy
- [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Laurent Thery, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, David Holland, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Laurent Thery, 01/24/2019
Archive powered by MHonArc 2.6.18.