## Stream: Coq users

### Topic: Match pair of terms in Ltac (beginner question)

#### Pierre Vial (Dec 07 2020 at 14:45):

Hello,
I would like to define a simple Ltac tactic on pair of lists.
Let's say for instance that I want a dummy tactic that computes the sum of the length of two listes. I would write something like:

``````Ltac sum_length_tac l1  l2 :=
match (l1 , l2) with
| (nil , nil) => O
| (_ :: ?s1 , _ ?s2) => constr:(S (S (sum_length_tac s1 s2)))
| _ => constr:(S O)
end.
``````

I get the nice error message:

``````Error:
Syntax error: ')' expected after [tactic:tactic_expr] (in [tactic:tactic_expr]).
``````

But is it just possible to match on pair? Is there some `constr:` missing somewhere e.g. before `(l1,l2)`?

#### Gaëtan Gilbert (Dec 07 2020 at 14:48):

``````Ltac sum_length_tac l1  l2 :=
match constr:((l1 , l2)) with
| (nil , nil) => O
| (cons _ ?s1 , _ ?s2) =>
let s := sum_length_tac s1 s2 in
constr:(S (S s))
| _ => constr:(S O)
end.

Goal False.
let x := sum_length_tac (cons 0 (cons 1 nil)) (cons 0 (cons 1 nil)) in
idtac x.
``````

#### Pierre Vial (Dec 07 2020 at 15:01):

Thanks Gaëtan!

Last updated: Oct 04 2023 at 22:01 UTC