Coq `ring` tacti c с логическими значениями: неверное уравнение кольца

Question

Документы Coq говорят, что кольцо логических значений предопределено, и все, что нужно сделать, это Require Ring.

В документах также говорится, что ring tacti c работает путем нормализации относительно ассоциативности и коммутативности.

Однако ring tacti c не удаётся для этого тривиального доказательства, которое опирается только на коммутативность || (orb):

Lemma ors: forall (a b: bool), a || b = b || a.
Proof.
intros.
ring.

Error: Tactic failure: not a valid ring equation.

Что пошло не так?

Answer 1

Это происходит потому, что стандартная библиотека Coq определяет структуру логического кольца для операций andb и xorb. Но чтобы доказать свою лемму с помощью ring tacti c, вам нужно булево полукольцо. Вот как вы можете определить это, используя 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.

К сожалению, теперь это нарушает использование ring для целей, включающих функцию xorb.