module BoolRing where

open import Function
open import Data.Bool
open import Relation.Binary.PropositionalEquality

open import Structures
open import BoolTactic

-- Example ring. All the proofs uses a brute force (tabulation)
-- boolean decision procedure defined in BoolTactic.
boolRing : Ring
boolRing =
  record {
    C = Bool;
    `0 = false;
    `1 = true;
    _+_ = _xor_;
    _*_ = _∧_;
    -_ = id;
    isRing =
      record {
        +-isAbelianGroup =
          record { isGroup =
            record { isMonoid = record { left-id = auto _;
                                         right-id = auto _;
                                         assoc = auto _ };
                     left-inv = auto _;
                     right-inv = auto _ };
              commute = auto _ };
        *-isMonoid =
          record { left-id = auto _;
                   right-id = auto _;
                   assoc = auto _ };
        left-distr = auto _;
        right-distr = auto _ } }