递归Ltac执行后如何清理无关的假设与变量？

定义的Ltac代码 #

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.

初始上下文 #

a: list bool
H: length a = 5

执行destruct_list a H.后，得到包含冗余内容的上下文：

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

需求 #

希望仅保留以下核心上下文：

E: a = [x; y; x0; y0; x1]
x, y, x0, y0, x1: bool

解决方案 #

1. 修改原Ltac，自动清理冗余内容 #

在Ltac的递归结束后添加替换和清理步骤，确保执行后直接得到目标上下文：

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;
      subst; clear Hl  (* 替换并清理临时假设 *)
  | [ Hl : length ?l = ?n |- _] => destruct_list l Hl
  | _ => 
      subst;  (* 用所有等式替换变量，消除中间列表变量 *)
      clear -E x y x0 y0 x1  (* 仅保留指定的假设和变量，清除其余 *)
  end.

• subst会自动将l0、l等中间列表变量用对应的元素列表替换；
• clear -<项>语法表示仅保留列出的项，清除上下文里的其他所有内容。

2. 执行原Ltac后手动清理 #

如果不想修改原Ltac，执行完destruct_list a H.后，直接运行以下命令即可：

subst; clear -E x y x0 y0 x1

3. 更简洁的替代实现 #

如果核心需求只是将长度为5的列表拆分为5个元素的形式，完全可以跳过原Ltac，直接用以下命令一步到位，避免生成冗余内容：

remember (x::y::x0::y0::x1::nil) as a eqn:E;
injection H; clear H; intros; subst

内容的提问来源于stack exchange，提问作者epelaez