Library ListTac

Some tactics for dealing with lists

Libraries

Require Import ssreflect.
Require Export List.

Remove x from the list l

Ltac reminlist x l :=
  match l with
    | (nil (A:=?T)) => constr : (nil (A:=T))
    | (?h :: ?t) =>
      let y := reminlist x t in
      match x with
        | h => constr : y
        | _ => constr : (h::y)
      end
  end.

Remove all the elements of the list to_rem from l

Ltac remlistinlist to_rem l :=
  match to_rem with
    | (nil (A:=?T)) => constr : (l)
    | (?h :: ?t) =>
      let l' := reminlist h l in
        remlistinlist t l'
  end.

Concatenate l1 and l2

Ltac applist l1 l2 :=
  match l1 with
    | nil => constr : l2
    | (?h :: ?t) =>
      let y := applist t l2 in
        constr : (h::y)
  end.

Given f:A -> B and a list l = a1::a2::..., makes the list (f a1)::(f a2)::...

Ltac maplist f B l :=
  match l with
    | nil => constr : (nil (A:=B))
    | (?h :: ?t) =>
      let y := f h in
      let z := maplist f B t in
        constr : (y::z)
  end.