I have an Ltac defined as follows.
Ltac destruct_list l H :=
let y := fresh "y" in
let x := fresh "x" in
let E := fresh "E" in
destruct l as [ | x [| y]] eqn:E;
simpl in H; inversion H;
match goal with
| [ Hl : length ?l = 0 |- _] => assert (?l = nil); apply length_zero_iff_nil
| [ Hl : length ?l = ?n |- _] => destruct_list l Hl
| _ => idtac
end.
So, in the following context:
a: list bool
H: length a = 5
If I do:
destruct_list a H.
I get:
a: list bool
x, y: bool
l: list bool
x0, y0: bool
l0: list bool
x1: bool
E1: l0 = [x1]
E0: l = [x0; y0; x1]
E: a = [x; y; x0; y0; x1]
H: S (S (length [x0; y0; x1])) = 5
H1: S (S (length [x1])) = 3
H2: 1 = 1
However, I only care about getting the following context:
E: a = [x; y; x0; y0; x1]
x, y, x0, y0, x1: bool
Is there a way to clear the variables that I do not care about?
Here is a possible solution. The main change is about adding subst ; clear H to the script. I had to split the tactic in two, in order to detect the first time it enters the tactic so as to remember the value of the list before entering the destruction loop.
Require Import List.
Ltac destruct_list_aux l H :=
let y := fresh "y" in
let x := fresh "x" in
destruct l as [ | x y];
simpl in *; inversion H ; clear H;
match goal with
| [ Hl : length ?l = 0 |- _] => assert (?l = nil); apply length_zero_iff_nil
| [ Hl : length ?l = ?n |- _] => destruct_list_aux l Hl
| _ => idtac
end.
Ltac destruct_list l H :=
let y := fresh "y" in
let E := fresh "E" in
remember l as y ;
destruct_list_aux y H.