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

Question

这种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策略？

这个特定的目标可以解决omega,但如果它更复杂,欧米茄失败了,我不得不求助于:replace (2 + a) with (a + 2); simpl; replace (a + 2) with (2 + a).

Answer 1

您可以使用Transparent和Opaque命令控制定义展开.在你的例子中,你应该能够说出类似的话

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

或者,该Arguments 命令可用于指示simpl策略避免在某些上下文中简化术语.例如

Arguments Z.add _ _ : simpl nomatch.

在你的情况下为我做的伎俩.这个特殊的变体所做的是避免match在这样做之后简化一个术语,当一个大的,丑陋的出现在头部位置时(你在你的例子中看到的).但是,还有其他变种.

最后,为了完整起见,Ssreflect库提供了很好的基础结构,可以使某些定义在本地不透明.所以你可以这样说

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

意思是"锁定Z.add,以便它不会简化,然后简化表达式的剩余部分(/=开关),然后再次解锁定义(-lock)".