Ltac list of hypothesis · Coq users

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

Théo Winterhalter (Feb 25 2021 at 13:54):

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.

Guillaume Melquiond (Feb 25 2021 at 14:29):

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

Pierre-Marie Pédrot (Feb 25 2021 at 14:33):

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.

Louise Dubois de Prisque (Feb 25 2021 at 14:47):

Louise Dubois de Prisque (Mar 08 2021 at 09:05):

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

Guillaume Melquiond (Mar 08 2021 at 09:09):

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

Guillaume Melquiond (Mar 08 2021 at 09:10):

Needless to say, that is mostly an artifact of Ltac not having a proper exception or error mechanism.

Guillaume Melquiond (Mar 08 2021 at 09:13):

You can get a feel of it by simply running try fail 0 and try fail 1 and compare their behaviors.

Louise Dubois de Prisque (Mar 08 2021 at 09:37):

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

Guillaume Melquiond (Mar 08 2021 at 09:47):

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

Stream: Coq users

Topic: Ltac list of hypothesis

Louise Dubois de Prisque (Feb 25 2021 at 13:51):