如何禁止简单策略展开算术表达式？

The simpl策略展开诸如2 + a“匹配树”这看起来一点也不简单。例如：

Goal forall i:Z, ((fun x => x + i) 3 = i + 3).
simpl.

导致：

forall i : Z,
match i with
| 0 => 3
| Z.pos y' =>
    Z.pos
      match y' with
      | q~1 =>
          match q with
          | q0~1 => (Pos.succ q0)~1
          | q0~0 => (Pos.succ q0)~0
          | 1 => 3
          end~0
      | q~0 =>
          match q with
          | q0~1 => (Pos.succ q0)~0
          | q0~0 => q0~1
          | 1 => 2
          end~1
      | 1 => 4
      end
| Z.neg y' => Z.pos_sub 3 y'
end = i + 3

如何避免此类并发症simpl tactic?

这个特定的目标可以通过以下方式解决omega，但如果它更复杂一点，欧米茄就会失败，我必须求助于类似的东西：replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a).

您可以使用以下命令控制定义的展开Transparent and Opaque命令。在你的例子中，你应该能够说类似的话

Opaque Z.add.
simpl.
Transparent Z.add.

或者，Arguments command可以用来指示simpl避免在某些情况下简化术语的策略。例如。

Arguments Z.add _ _ : simpl nomatch.

在你的情况下对我有用。这个特殊变体的作用是避免在一个又大又丑的情况下简化术语。match这样做后会出现在头部位置（您在示例中看到的）。然而，还有其他变体。

最后，为了完整起见，反射库提供了良好的基础设施，使某些定义在本地不透明。所以你可以这样说

rewrite (lock Z.add) /= -lock.

意思是“锁”Z.add，这样它就不会简化，然后简化表达式的其余部分（/=开关），然后再次解锁定义（-lock)".