//
// # Example: The binary field _F2_.
//
// The _binary_ values {`F`,`T`} form a _finite field_ with binary XOR
// as "addition", binary AND as "multiplication", and binary NOT as
// "negation". This field is known as _F2_ or _GF(2)_ [GF2].
//
// This means the familiar digital logic or computing _boolean_ type
// effectively forms a (finite) field.
//
// [GF2]: https://en.wikipedia.org/wiki/Field_(mathematics)
//
#![allow(non_snake_case)]

use proptest_derive::*;
use un_algebra::tests::*;
use un_algebra::prelude::*;


//
// The binary field F2.
//
#[derive(Copy, Clone, PartialEq, Debug, Arbitrary)]
pub enum F2 {
  F, T
}


//
// F2 values form an additive magma.
//
impl AddMagma for F2 {

  // F2 addition is binary "exclusive or".
  fn add(&self, other: &Self) -> Self {

    // Redundant branch expressions used for clarity.
    match (self, other) {
      (F2::F, F2::F) => F2::F,
      (F2::F, F2::T) => F2::T,
      (F2::T, F2::F) => F2::T,
      (F2::T, F2::T) => F2::F,
    }
  }
}


//
// F2 values form an additive semigroup.
//
impl AddSemigroup for F2 {}


//
// F2 values form an additive monoid.
//
impl AddMonoid for F2 {

  // F2 false acts as zero.
  fn zero() -> Self {
    F2::F
  }
}


//
// F2 values form an additive group.
//
impl AddGroup for F2 {

  // F2 negation is binary identity.
  fn negate(&self) -> Self {
    *self
  }
}


//
// F2 values form an additive commutative group.
//
impl AddComGroup for F2 {}


//
// F2 values form a multiplicative magma.
//
impl MulMagma for F2 {

  // F2 multiplication is binary "and".
  fn mul(&self, other: &Self) -> Self {
    match (self, other) {
      (F2::F, F2::F) => F2::F,
      (F2::F, F2::T) => F2::F,
      (F2::T, F2::F) => F2::F,
      (F2::T, F2::T) => F2::T,
    }
  }
}


//
// F2 values form a multiplicative semigroup.
//
impl MulSemigroup for F2 {}


//
// F2 values form a multiplicative monoid.
//
impl MulMonoid for F2 {

  // One is binary true.
  fn one() -> Self {
    F2::T
  }
}


//
// F2 values form a multiplicative group.
//
impl MulGroup for F2 {

  // Invert is binary identity.
  fn invert(&self) -> Self {
    *self
  }


  // Only binary true elements are invertible.
  fn is_invertible(&self) -> bool {
    *self == F2::T
  }
}


//
// F2 values form a multiplicative commutative group.
//
impl MulComGroup for F2 {}


//
// F2 values form a ring.
//
impl Ring for F2 {}


//
// F2 values form a commutative ring.
//
impl ComRing for F2 {}


//
// F2 values form a field.
//
impl Field for F2 {

  // Invert is binary identity.
  fn invert(&self) -> Self {
    *self
  }


  // Only boolean true elements are invertible.
  fn is_invertible(&self) -> bool {
    *self == F2::T
  }
}


//
// Generative tests for F2 algebraic axioms and properties.
//
proptest! {
  #![proptest_config(config::standard())]


  #[test]
  fn add_closure((x, y) in any::<(F2, F2)>()) {
    prop_assert!(AddMagmaLaws::closure(&x, &y))
  }


  #[test]
  fn mul_closure((x, y) in any::<(F2, F2)>()) {
    prop_assert!(MulMagmaLaws::closure(&x, &y))
  }


  #[test]
  fn mul_closure_t2([xs, ys] in any::<[(F2, F2); 2]>()) {
    prop_assert!(MulMagmaLaws::closure(&xs, &ys))
  }


  #[test]
  fn mul_closure_a2([xs, ys] in any::<[[F2; 2]; 2]>()) {
    prop_assert!(MulMagmaLaws::closure(&xs, &ys))
  }


  #[test]
  fn mul_associativity((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(MulSemigroupLaws::associativity(&x, &y, &z))
  }


  #[test]
  fn add_associativity((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(AddSemigroupLaws::associativity(&x, &y, &z))
  }


  #[test]
  fn add_associativity_t1([xs, ys, zs] in any::<[(F2,); 3]>()) {
    prop_assert!(AddSemigroupLaws::associativity(&xs, &ys, &zs))
  }


  #[test]
  fn add_associativity_a1([xs, ys, zs] in any::<[[F2; 1]; 3]>()) {
    prop_assert!(AddSemigroupLaws::associativity(&xs, &ys, &zs))
  }


  #[test]
  fn left_add_identity(x in any::<F2>()) {
    prop_assert!(AddMonoidLaws::left_identity(&x))
  }


  #[test]
  fn left_add_identity_a2(xs in any::<[F2; 2]>()) {
    prop_assert!(AddMonoidLaws::left_identity(&xs))
  }


  #[test]
  fn right_add_identity(x in any::<F2>()) {
    prop_assert!(AddMonoidLaws::right_identity(&x))
  }


  #[test]
  fn right_add_identity_a2(xs in any::<[F2; 2]>()) {
    prop_assert!(AddMonoidLaws::right_identity(&xs))
  }


  #[test]
  fn left_mul_identity(x in any::<F2>()) {
    prop_assert!(MulMonoidLaws::left_identity(&x))
  }


  #[test]
  fn left_mul_identity_t3(xs in any::<(F2, F2, F2)>()) {
    prop_assert!(MulMonoidLaws::left_identity(&xs))
  }


  #[test]
  fn right_mul_identity(x in any::<F2>()) {
    prop_assert!(MulMonoidLaws::right_identity(&x))
  }


  #[test]
  fn left_add_inverse(x in any::<F2>()) {
    prop_assert!(AddGroupLaws::left_inverse(&x))
  }


  #[test]
  fn right_add_inverse(x in any::<F2>()) {
    prop_assert!(AddGroupLaws::right_inverse(&x))
  }


  #[test]
  fn right_add_inverse_t2(xs in any::<(F2, F2)>()) {
    prop_assert!(AddGroupLaws::right_inverse(&xs))
  }


  #[test]
  fn right_add_inverse_a2(xs in any::<[F2; 2]>()) {
    prop_assert!(AddGroupLaws::right_inverse(&xs))
  }


  #[test]
  fn left_mul_inverse(x in any::<F2>()) {
    prop_assume!(MulGroup::is_invertible(&x));

    prop_assert!(MulGroupLaws::left_inverse(&x))
  }


  #[test]
  fn right_mul_inverse(x in any::<F2>()) {
    prop_assume!(MulGroup::is_invertible(&x));

    prop_assert!(MulGroupLaws::right_inverse(&x))
  }


  #[test]
  fn right_mul_inverse_a2((x, y) in any::<(F2, F2)>()) {
    prop_assume!(MulGroup::is_invertible(&[x, y]));

    prop_assert!(MulGroupLaws::right_inverse(&[x, y]))
  }


  #[test]
  fn add_commutivity((x, y) in any::<(F2, F2)>()) {
    prop_assert!(AddComGroupLaws::commutivity(&x, &y))
  }


  #[test]
  fn add_commutivity_t2([xs, ys] in any::<[(F2, F2); 2]>()) {
    prop_assert!(AddComGroupLaws::commutivity(&xs, &ys))
  }


  #[test]
  fn mul_commutivity((x, y) in any::<(F2, F2)>()) {
    prop_assert!(MulComGroupLaws::commutivity(&x, &y))
  }


  #[test]
  fn mul_commutivity_t1((x, y) in any::<(F2, F2)>()) {
    prop_assert!(MulComGroupLaws::commutivity(&(x,), &(y,)))
  }


  #[test]
  fn mul_commutivity_a1((x, y) in any::<(F2, F2)>()) {
    prop_assert!(MulComGroupLaws::commutivity(&[x], &[y,]))
  }


  #[test]
  fn left_distributivity((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(RingLaws::left_distributivity(&x, &y, &z))
  }


  #[test]
  fn left_distributivity_t2([xs, ys, zs] in any::<[(F2, F2); 3]>()) {
    prop_assert!(RingLaws::left_distributivity(&xs, &ys, &zs))
  }


  #[test]
  fn right_distributivity((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(RingLaws::right_distributivity(&x, &y, &z))
  }


  #[test]
  fn right_distributivity_t1((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(RingLaws::right_distributivity(&(x,), &(y,), &(z,)))
  }


  #[test]
  fn left_zero_absorption(x in any::<F2>()) {
    prop_assert!(RingLaws::left_absorption(&x))
  }


  #[test]
  fn right_zero_absorption(x in any::<F2>()) {
    prop_assert!(RingLaws::right_absorption(&x))
  }


  #[test]
  fn left_mul_negation((x, y) in any::<(F2, F2)>()) {
    prop_assert!(RingLaws::left_negation(&x, &y))
  }


  #[test]
  fn right_mul_negation((x, y) in any::<(F2, F2)>()) {
    prop_assert!(RingLaws::right_negation(&x, &y))
  }


  #[test]
  fn mul_commutivity_t2((x, y) in any::<(F2, F2)>()) {
    prop_assert!(ComRingLaws::commutivity(&x, &y))
  }


  #[test]
  fn mul_commutivity_a4([w, x, y, z] in any::<[F2; 4]>()) {
    prop_assert!(ComRingLaws::commutivity(&(w, x), &(y, z)))
  }


  #[test]
  fn mul_commutivity_a2([w, x, y, z] in any::<[F2; 4]>()) {
    prop_assert!(ComRingLaws::commutivity(&[w, x], &[y, z]))
  }


  #[test]
  fn field_left_inverse(x in any::<F2>()) {
    prop_assume!(Field::is_invertible(&x));

    prop_assert!(FieldLaws::left_inverse(&x))
  }


  #[test]
  fn field_left_inverse_t1(x in any::<F2>()) {
    prop_assume!(Field::is_invertible(&(x,)));

    prop_assert!(FieldLaws::left_inverse(&(x,)))
  }


  #[test]
  fn field_left_inverse_a1(x in any::<F2>()) {
    prop_assume!(Field::is_invertible(&[x]));

    prop_assert!(FieldLaws::left_inverse(&[x]))
  }


  #[test]
  fn field_right_inverse(x in any::<F2>()) {
    prop_assume!(Field::is_invertible(&x));

    prop_assert!(FieldLaws::right_inverse(&x))
  }


  #[test]
  fn field_right_inverse_t2(xs in any::<(F2, F2)>()) {
    prop_assume!(Field::is_invertible(&xs));

    prop_assert!(FieldLaws::right_inverse(&xs))
  }


  #[test]
  fn field_right_inverse_a2(xs in any::<[F2; 2]>()) {
    prop_assume!(Field::is_invertible(&xs));

    prop_assert!(FieldLaws::right_inverse(&xs))
  }


  #[test]
  fn add_cancellation((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(FieldLaws::add_cancellation(&x, &y, &z))
  }


  #[test]
  fn add_cancellation_t1((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(FieldLaws::add_cancellation(&(x,), &(y,), &(z,)))
  }


  #[test]
  fn add_cancellation_a1((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(FieldLaws::add_cancellation(&[x], &[y], &[z]))
  }


  #[test]
  fn mul_cancellation((x, y, z) in any::<(F2, F2, F2)>()) {
    prop_assert!(FieldLaws::mul_cancellation(&x, &y, &z))
  }


  #[test]
  fn zero_cancellation((x, y) in any::<(F2, F2)>()) {
    prop_assert!(FieldLaws::zero_cancellation(&x, &y))
  }
}


fn main() {}