带有布尔值的Coq`ring`策略：不是有效的环方程

Question

Coq docs说布尔值的环是预定义的，而所有要做的就是Require Ring.

[文档还说ring策略通过标准化w.r.t。关联性和可交换性。

但是，对于仅依赖于ring（||）的可交换性的琐碎证明，orb策略失败了]]

Lemma ors: forall (a b: bool), a || b = b || a.
Proof.
intros.
ring.
Error: Tactic failure: not a valid ring equation.
出了什么问题？

Coq文档说，布尔值的环是预定义的，而所有要做的就是Require Ring。这些文档还说，通过将w.r.t.关联性和...

Answer 1

之所以这样，是因为Coq的标准库为Boolean ring structure和andb操作定义了xorb。但是要使用ring策略证明引理，您需要布尔半环。这是使用Add Ring本地语言定义的方法：