Coq求解器战术中fresh生成可读假设名的常量兼容问题

问题核心 #

fresh战术仅接受标识符或字符串作为参数，遇到常量时会报错；手动嵌套tryif处理变量/常量分支会导致代码指数级膨胀，而is_var非值战术无法直接封装成简洁的辅助逻辑。

可行解决方案 #

方案1：通过字符串转换统一处理变量与常量

定义辅助函数将任意项转换为适合fresh的字符串，变量取其名称，常量用占位符或可读标识替代，再通过字符串拼接生成假设名：

Ltac constr_to_fresh_str c :=
  match constr:(c) with
  | ?x => try (string_of_id (id_of_constr x)) || "_"
  | 0 => "0"
  | 1 => "1"
  | S ?n => "S" ++ constr_to_fresh_str n
  | _ => "_"
  end.

(* 主战术调用 *)
match goal with
| |- context [ if (?a + ?b <? ?a) then _ else _ ] =>
  let s_a := constr_to_fresh_str a in
  let s_b := constr_to_fresh_str b in
  let W := fresh ("W" ++ s_a ++ s_b) in
  solve_overflow_test W a b
(* 其他模式分支 *)
end

这种方式既避免了fresh报错，还能为常见常量生成可读名称（比如1对应"1"），代码结构清晰无冗余。

方案2：将分支逻辑封装到辅助战术

把变量/常量的判断逻辑抽离到单独的辅助战术中，主代码仅负责模式匹配与调用，避免嵌套分支膨胀：

Ltac handle_overflow_test a b :=
  match constr:(a), constr:(b) with
  | ?x, ?y =>
    tryif is_var x then
      tryif is_var y then
        let W := fresh "W" x y in solve_overflow_test W a b
      else
        let W := fresh "W" x "_" in solve_overflow_test W a b
    else
      tryif is_var y then
        let W := fresh "W" "_" y in solve_overflow_test W a b
      else
        let W := fresh "W" "_" "_" in solve_overflow_test W a b
  end.

(* 主战术调用 *)
match goal with
| |- context [ if (?a + ?b <? ?a) then _ else _ ] =>
  handle_overflow_test a b
(* 其他模式分支 *)
end

后续新增参数时，只需修改辅助战术的分支，主代码无需改动。

总结 #

无需放弃生成包含标识符的可读假设名，上述两种方案均可解决fresh适配常量的问题，同时保持代码简洁可维护。

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