// Monoid: a set with an associative binary operation and identity element
//
// This is the simplest algebraic structure with interesting axioms.
// Note: geolog uses postfix function application.

theory Monoid {
  M : Sort;

  // Binary operation: M × M → M
  mul : [x: M, y: M] -> M;

  // Identity element: we use a unary function from M to M that
  // "picks out" the identity (any x maps to e)
  // A cleaner approach would use Unit → M but that needs product support.
  id : M -> M;

  // Left identity: id(x) * y = y (id(x) is always e)
  ax/left_id : forall x : M, y : M.
    |- [x: x id, y: y] mul = y;

  // Right identity: x * id(y) = x
  ax/right_id : forall x : M, y : M.
    |- [x: x, y: y id] mul = x;

  // Associativity: (x * y) * z = x * (y * z)
  ax/assoc : forall x : M, y : M, z : M.
    |- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul;

  // id is constant: id(x) = id(y) for all x, y
  ax/id_const : forall x : M, y : M.
    |- x id = y id;
}

// Trivial monoid: single element, e * e = e
instance Trivial : Monoid = {
  e : M;

  // Multiplication table: e * e = e
  // Using positional syntax: [a, b] maps to [x: a, y: b]
  [e, e] mul = e;

  // Identity: e is the identity element
  e id = e;
}

// Boolean "And" monoid: {T, F} with T as identity
// T and T = T, T and F = F, F and T = F, F and F = F
instance BoolAnd : Monoid = {
  T : M;
  F : M;

  // Identity: T is the identity element
  T id = T;
  F id = T;

  // Multiplication table for "and":
  [x: T, y: T] mul = T;
  [x: T, y: F] mul = F;
  [x: F, y: T] mul = F;
  [x: F, y: F] mul = F;
}

// Boolean "Or" monoid: {T, F} with F as identity
// T or T = T, T or F = T, F or T = T, F or F = F
instance BoolOr : Monoid = {
  T : M;
  F : M;

  // Identity: F is the identity element
  T id = F;
  F id = F;

  // Multiplication table for "or":
  [x: T, y: T] mul = T;
  [x: T, y: F] mul = T;
  [x: F, y: T] mul = T;
  [x: F, y: F] mul = F;
}