这是因为Coq的标准库为
Coq文档说布尔值环是预定义的，只需要Require Ring.
文献还说，ring策略通过规范w.r.t.结合性和交换性来工作。
然而，对于这个仅依赖于||(orb(的交换性的琐碎证明，ring策略失败了：
Lemma ors: forall (a b: bool), a || b = b || a.
Proof.
intros.
ring.
Error: Tactic failure: not a valid ring equation.
出了什么问题？
andb和xorb操作定义了一个布尔环结构。但要用ring策略证明你的引理，你需要一个布尔半环。以下是如何使用Add Ring语言定义它：
From Coq Require Import Ring.
Open Scope bool_scope.
Lemma boolSRth : semi_ring_theory false true orb andb (@eq bool).
Proof.
constructor.
exact Bool.orb_false_l.
exact Bool.orb_comm.
exact Bool.orb_assoc.
exact Bool.andb_true_l.
exact Bool.andb_false_l.
exact Bool.andb_comm.
exact Bool.andb_assoc.
exact Bool.andb_orb_distrib_l.
Qed.
Add Ring boolsr : boolSRth (decidable bool_eq_ok, constants [bool_cst]).
Lemma ors a b : a || b = b || a.
Proof. ring. Qed.
不幸的是，现在对于涉及xorb函数的目标，使用ring是不可行的。