coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof-local LTac

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Proof-local LTac
Date: Mon, 07 May 2018 09:50:56 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:Ml2/th9Fqwb2bv9uRHKM819IXTAuvvDOBiVQ1KB41OscTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhz1hikHKTA3/n3YhMt/g69ArxKtuwZyzpTObY2JNvdzeL7Wc9MARWpGW8ZcTyhPAoSmYIQTD+oBPONYpJTgqlsUsxS+BBWsBOXxxT9Sm3T72qg63P4gEQHCxwEgHdUOv27Io9X1NacSVPm5w7LSzTrdbvNWxTH955bSchw7vP6DQ6t9fMzMwkchEAPFi0+fqY3jPz6N1OQNtHKU4PZgVeKujm4rshp+oiKxycctlonJgJwaykre+Spk3ok4I8CzRk1jYdO8DZddtSCXO5FyT884XW1kpSg3xqcbtZO1ciUHzoksyQTFZPydaYeI5wruVOaPLjd8g3JoYLK/iAio8Uil1OL8TdO40E1UoSpfjNnDqGoN2AbW6sedUPdy41mu1S6O1wDV9O5EPVg5mbfZJpMg2LI9koAfvVreEiL4gkn6kaGbe0s89uit8evnY7HmppGGN49zjwHzKqEulda+AeQ8KQUOXW+b9v6g273j/E35RaxGgeYskqbHsZDaOcIbqbCjAwNPz4ks9Q6zDy2639QAgXkHMFVFdQqbgIjuIlHCOez3DfOig1u3izpr3PDHPrj5AprXNHTDkbHhfax860FG0gYzw8pftNpoDeQKJ+u2UUvsvvTZCAU4Okq62bXJEtJ4g6EZUGmPA6rRGrnfsEOO6/hnd+yFZYs9ujH0IPgk4rvkl3I4hVkQZ++l0M1EOziDAv16LhDBMjLXidAbHDJS51tsfKnRkFSHFAVrSTO3VqM46Cs8Ddj/X4XET4utgbnE1j22H4FQa3oABl3eSy60JbXBYO8FbWepGuEkiiYND+HzSYgo3hGvsUrw0bdmMuzZ4GsUuMC7jYUn16jojRg3sAdMIYGd3mWKFTgmnm4SQjItmrtyu1Jw0F6G2O50jq4AGA==

Hi,

at some point recently I wrote

Lemma …
Proof.
Ltac foo := …
…
Qed.

and was very surprised when later someone else working on the same
project started using the `foo` tactic in a different proof further
down.

Also, I noticed that an Ltac definition inside a Proof cannot mention
local variables, so I cannot do

Ltac IH := apply IH; only 1: my_termination_tactic.

Is there a way to define proof-local ltacs that capture local
variables?

Thanks,
Joachim

--
Joachim Breitner

mail AT joachim-breitner.de
http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Proof-local LTac, Joachim Breitner, 05/07/2018
- Re: [Coq-Club] Proof-local LTac, Emilio Jesús Gallego Arias, 05/07/2018