I would like to know whether it is possible for a tactic to take a list of hypothesis in parameter and applies recursively a given tactic on it. For instance, I would like to do this :
Ltac foo h := lazymatch h with | nil => idtac | cons ?hd ?h' => idtac hd ; foo h' end.
Of course I have a typing error as soon as I give two hypothesis with different types in my list but maybe there is a trick that you know to avoid this problem...
Thank you !
Not very pretty but a trick would be to have a list of type
unit for instance like
[ let _ := h1 in tt ; let _ := h2 in tt ; let _ := h3 in tt ]
Then when matching you have to match on the
let to get the body. Any way of "hiding" the info would work.
In CoqInterval, I am using tuples instead of lists to pass arguments to tactics. That way, it can be heterogeneous. It however requires a special branch to handle the very last value of a tuple. (Straightforward but a bit ugly.)
Alternatively you can mix Ltac2 in your Ltac1 tactic. The former has a list datatype that lets you manipulate them in a first-class way.
Thanks a lot for all these possibilities
@Guillaume Melquiond I looked at your tactics in CoqInterval but I don't understand why you need to add a branch with
fail 100, for instance in this tactic :
Ltac tuple_to_list params l := match params with | pair ?a ?b => tuple_to_list a (b :: l) | ?b => constr:(b :: l) | ?z => fail 100 "Unknown tactic parameter" z end.
Indeed, I tried a similar method without the last branch and it seems to work as well.
It depends on your use case. If you do not put the last branch, the error propagates only one level upward. By putting
fail 100, I ensure that this is a hard error that aborts everything until it reaches the user. (Or at least until 100 levels have been aborted, which hopefully is enough to reach the user.)
Needless to say, that is mostly an artifact of Ltac not having a proper exception or error mechanism.
You can get a feel of it by simply running
try fail 0 and
try fail 1 and compare their behaviors.
Thank you ! So if I understood well,
fail 100 is mainly useful here when the tactic is combined with others, to be almost sure that it will reach the user. Otherwise, when the tactic is used alone, one level of error is probably enough to reach the user
Yes and no. The error might indeed reach the user, but not necessarily with the message you wanted. You may end up with
No matching clauses for match instead of an informative message. It depends on how your
match constructs are nested (possibly due to recursion).
Thank you very much for your help, this is clear to me now !
Last updated: Sep 30 2023 at 05:01 UTC