Stream: Coq users

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


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Pierre Vial (Dec 07 2020 at 15:01):

Thanks Gaëtan!


Last updated: Feb 08 2023 at 23:03 UTC