如何将Coq中的let变量移至独立假设？

需求场景 #

我们需要将定理中某个假设（如cmplx）内部的顶层let绑定变量，提取为独立的命名假设，同时保持原复杂表达式（如g a b）的可读性，不使用simpl等会改写表达式的策略。

例如，将初始定理：

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (cmplx :=
      let a := f 0 in
      let b := f 1 in
      g a b
    )
    : False.

转换为：

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (a := f 0)
    (b := f 1)
    (cmplx := g a b)
    : False.

通用Ltac实现 #

以下是实现单个变量提取的let_up策略，它会匹配目标中指定假设的顶层let绑定，将变量转为独立假设并更新原假设的定义：

Ltac let_up hyp var :=
  match goal with
  | [ H : context[let x := ?v in ?body] |- _ ]
    where hyp = H
    where var = x =>
    pose (var := v);
    change (let x := v in body) with body in H;
    clearbody H
  end.

用法示例 #

在目标定理中，依次调用以下命令即可提取a和b：

let_up cmplx a.
let_up cmplx b.

扩展批量处理 #

如果需要一次性提取所有顶层let变量，可以扩展Ltac自动遍历处理：

Ltac let_up_all hyp :=
  repeat match goal with
         | [ H : context[let x := ?v in ?body] |- _ ]
           where hyp = H =>
           pose (x := v);
           change (let x := v in body) with body in H;
           clearbody H
         end.

调用let_up_all cmplx.即可一次性提取cmplx中的所有顶层let变量。

注意事项 #

• 该策略仅处理顶层let绑定，嵌套的let需要多次调用或调整匹配逻辑。
• 不会修改原复杂表达式的结构，完全保留可读性，避免了simpl等策略带来的表达式改写问题。

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