如何禁止簡單的策略展開算術表達式？

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。