Coq中多等式场景下如何控制subst命令？

当然可以！当你遇到inversion生成一堆a = b式的假设，又不想让subst碰某个特定假设（比如H0）时，有几个实用的方法可以精准控制替换行为：

• 显式指定要替换的变量
  别直接用无参数的subst（它会自动替换所有可等式化的变量），而是明确写出你想要替换的变量名。比如你想替换a和b但保留H0里的变量，就执行：

  subst a b.
  

  这样subst只会处理和a、b相关的等式，完全不会碰H0中的内容，从根源上避免rel1、rel2这类表达式被不必要地膨胀。

• 手动用rewrite替代subst，精准控制替换范围
  如果subst的自动替换逻辑太“贪心”，可以改用rewrite命令，明确指定要改写的目标和假设。比如你想把H1: x = y的替换应用到除了H0之外的所有地方，就执行：

  rewrite H1 in -H0.
  

  这个命令会在所有假设（除了H0）和当前目标里替换x为y，既能完成替换需求，又能保护H0不被修改。

• 暂时隔离不想处理的假设
  如果你需要先执行全量subst但又不想让H0参与，可以先把H0临时移出上下文：

  (* 先复制H0到临时变量 *)
  assert (H0_temp := H0).
  (* 移除原H0，让subst看不到它 *)
  clear H0.
  (* 执行需要的subst操作 *)
  subst.
  (* 把H0加回上下文 *)
  assert H0 := H0_temp.
  clear H0_temp.
  

  这个方法适合你需要处理大部分等式，之后还要用到H0的场景，虽然步骤多一点，但能保证H0完全不受subst影响。

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