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

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. 

另外，该Argumentscommand可以用来指示simpl战术，以避免简化在某些情况下而言。例如。

Arguments Z.add _ _ : simpl nomatch. 

对我来说在你的情况下会有诀窍。这个特定的变体做什么是避免简化术语，当一个大的，丑陋的match会出现在头后的位置（你在例子中看到的）。但也有其他变体。

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

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

意为“锁定Z.add，所以它不会简化，然后简化表达式（/=开关）的剩余，然后再解锁定义（-lock）”。

Answer 2

您可以调整简单策略的行为方式，从而获得更少的匹配。

了解更多关于here。您可以使用other tactics，让您选择如何减少。例如，cbn beta。