coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] using the tactical do in a Ltac definition

From: Nicolas Magaud <magaud AT unistra.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] using the tactical do in a Ltac definition
Date: Fri, 9 Feb 2018 11:55:33 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=magaud AT unistra.fr; spf=Pass smtp.mailfrom=magaud AT unistra.fr; spf=None smtp.helo=postmaster AT mailhost.u-strasbg.fr
Ironport-phdr: 9a23:MAydUxDjhvQlAzU467ArUyQJP3N1i/DPJgcQr6AfoPdwSPv6pcbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyI2/m7ZhMJtkqxVox2uqRtkzo7IeYGVMeZyfqPBcd4YQ2dKQ8ZfVzZGAoO5d4YBF+sBMvpfr4n5vVQOtga1Cw62C+Pg0DBIm2L51rA93uQkCw7G0xYvH88Tv3nPsdX1MqYSUfupzKnS1zrPdf1W2S3k5YXObxsvoumMUKptfcff1UUjDQHIg1GKpYD7IT+ZyP4Bv3aG4+djTe6iiHArpxtvrjWh28sgkIjEi4APxlzZ6Sl0wYA4LsCiRkFhe96rCp5QujmaN4RoRsMiRHlluCMgxb0HvZ67fC8KyI87xxLFdvyLapOI4g75VOmLOjd3n31ldKixhxao6USgy+v8Wdeo0FtSsyZInMXAumoP2hHX8MSLVOVx8lm71TqRygze6flIIUUumqraL54hzKQwlp0WsUnbGy/5gkr2g7WLdko54eWo9uLnYrT9pp+ALY97kBvyMqo0msCnG+Q3LhAOX3SH+eS7zLDs4Ur5QKxTgvIqlqnZrYvVKN8Apq+5Bg9Vypws5wy+DzegytQYnGMIIEhLeBKd3MDVPATFJ+m9BvOiiXytli1qzrbIJO7PGJLIe17Cm7DldK01zkdTwRc/hYRa7p1dF70pPfTyQVPrvZrWFElqYESP3+/7BYAlhcslUmWVD/rBafKAgRqz/usqZtK0SsoQsTf5JeIi4qe032I/mEQBZ6Dv04FFMSnkTMQjGF2QZD/XuvlECX0D51BsUerrk0GYWHhdfSTqBv9u1nQAEIujSLz7aMWtjbiGhnzpG5RXYmBBEUzKDDLza5+NQP0DLiyIcJds

Below are 2 tactics t and u which I expect to behave in the same way.

They perform (if possible) x times the tactic “intro”.

However I do not manage to run “t”. Writing "t 2. "leads to an error message.
I can still achieve my goal by writing a recursive tactic, but using the “do”
construct would be more straightforward.

Am I missing a constr: , ltac: or something similar somewhere ?

Thanks in advance

Nicolas Magaud

--------------------------------------------
Ltac t x := do x intro; idtac "stop".
Ltac u x := match x with O => idtac "stop" | (S ?p) => intro; u p end.

Lemma f : forall x y z:nat, x= y -> z= y.
Proof.
t 2. (* Error: Ltac variable x is bound to a term which cannot be coerced
to an integer.*)
u 2.

[Coq-Club] using the tactical do in a Ltac definition, Nicolas Magaud, 02/09/2018
- Re: [Coq-Club] using the tactical do in a Ltac definition, Pierre Courtieu, 02/09/2018