Coq中Beta展开：如何将指定项抽象为函数？

你需要实现的是将等式一侧的项（如a + 1）展开为(fun x => x + 1) a的形式，但原代码报错是因为混淆了Ltac战术变量/函数和Coq项的区别：你定义的f是Ltac层面的函数（tacvalue），它只能在战术执行中操作上下文，不能直接嵌入到Coq的fun x:T => ...项结构中。

修正后的Ltac实现 #

以下是两种可行的实现方式，都能完成等式内指定子项的Beta展开：

方式一：直接构造抽象项并替换目标

这个版本专门处理等式左侧的子项展开：

Ltac beta_expansion_eq_lhs subterm :=
  match goal with
  | |- ?LHS = ?RHS =>
      let T := type of subterm in
      match LHS with
      | context[subterm] =>
          (* 构造Coq抽象项：将LHS中的subterm替换为x后包裹成fun *)
          let abstracted := constr:(fun x:T => context[LHS][subterm := x]) in
          (* 替换目标中的LHS为抽象项应用subterm的结果 *)
          change (abstracted subterm = RHS)
      end
  end.

(* 测试用例 *)
Goal forall a: nat, a + 1 = 0.
intros a.
beta_expansion_eq_lhs a.
(* 目标转换为：(fun x : nat => x + 1) a = 0 *)
Abort.

方式二：通用的Beta展开函数

这个版本可以对任意项中的指定子项进行展开，再替换回目标：

Ltac beta_expand term subterm :=
  let T := type of subterm in
  match term with
  | context[subterm] =>
      let abstracted := constr:(fun x:T => context[term][subterm := x]) in
      constr:(abstracted subterm)
  end.

(* 测试用例 *)
Goal forall a: nat, a + 1 = 0.
intros a.
match goal with
| |- ?LHS = ?RHS =>
    let new_LHS := beta_expand LHS a in
    change (new_LHS = RHS)
end.
(* 目标转换为：(fun x : nat => x + 1) a = 0 *)
Abort.

另一种简化方案：利用pattern战术 #

如果你只需要处理单个子项的展开，也可以结合set和pattern快速实现，不需要自定义Ltac：

Goal forall a: nat, a + 1 = 0.
intros a.
(* 先将等式左侧存为临时变量 *)
set (LHS := a + 1) in |-.
(* 对临时变量中的a进行抽象 *)
pattern a in LHS.
(* 展开临时变量得到最终形式 *)
unfold LHS.
(* 目标转换为：(fun x : nat => x + 1) a = 0 *)
Abort.

关键原理说明 #

• context[term][subterm := x]是Coq的上下文替换语法，能将term中所有subterm的出现替换为x，生成合法的Coq项。
• constr:(...)用于将Ltac构造的表达式转换为Coq可识别的项，避免了原代码中把Ltac函数（tacvalue）当作Coq项使用的错误。

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