[coq] [mathcomp2] comSemiRing example

coq/mathcomp/mathcomp2/b3-comSemiRing.v

@@ -0,0 +1,61 @@
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Local Open Scope ring_scope.
+
+Module b3.
+  Definition t: Type := option bool.
+  Definition one: t := Some true.
+  Definition zero: t := Some false.
+  Definition add (a b: t): t :=
+    match a, b with
+    | Some true, _ => Some true
+    | _, Some true => Some true
+    | Some false, Some false => Some false
+    | _, _ => None
+    end.
+  Definition mul (a b: t): t :=
+    match a, b with
+    | Some false, _ => Some false
+    | _, Some false => Some false
+    | Some true, Some true => Some true
+    | _, _ => None
+    end.
+
+  Lemma addrC: commutative add.
+  Proof. by do !case. Qed.
+  Lemma addrA: associative add.
+  Proof. by do !case. Qed.
+  Lemma add0r: left_id zero add.
+  Proof. by do !case. Qed.
+  Lemma mulrC: commutative mul.
+  Proof. by do !case. Qed.
+  Lemma mulrA: associative mul.
+  Proof. by do !case. Qed.
+  Lemma mul1r: left_id one mul.
+  Proof. by do !case. Qed.
+  Lemma mulrDl: left_distributive mul add.
+  Proof. by do !case. Qed.
+  Lemma mul0r: left_zero zero mul.
+  Proof. by do !case. Qed.
+  Lemma oner_neq0: is_true (one != zero).
+  Proof. by []. Qed.
+End b3.
+
+HB.instance Definition _ := Choice.on b3.t.
+HB.instance Definition _ := GRing.isNmodule.Build b3.t b3.addrA b3.addrC b3.add0r.
+HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build
+  b3.t b3.mulrA b3.mulrC b3.mul1r b3.mulrDl b3.mul0r b3.oner_neq0.
+
+HB.about b3.t.
+(*
+HB: b3.t is canonically equipped with structures:
+    - choice.Choice
+      eqtype.Equality
+      (from "(stdin)", line 2)
+    - GRing.SemiRing
+      GRing.ComSemiRing
+      (from "(stdin)", line 1)
+    - GRing.Nmodule
+      (from "(stdin)", line 1)
+*)