-- Set-theoretic algebraic interfaces
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Foundation
import Set.Relation

namespace Algebra

-- Algebraic operations are sets of ordered pairs, that is, set-theoretic
-- functions.  A unary operation applies as any function does, inv(x); a
-- binary operation applies to the pair of its arguments, written op(x, y).
def call2 (op x y : Set) : Set := op((x, y))

-- Type-class interfaces for notation.  These are set-theoretic
-- predicates, separate from the `class` declaration form.  Their checked
-- `instance` theorems let elaboration synthesize the operation or constant
-- from a carrier; the kernel receives only applications and call2 terms.
predicate AddOperation (A op : Set) := FunctionBetween(op, A × A, A)
predicate MulOperation (A op : Set) := FunctionBetween(op, A × A, A)
predicate DivOperation (A op : Set) := FunctionBetween(op, A × A, A)
predicate NegOperation (A op : Set) := FunctionBetween(op, A, A)
predicate LessOperation (A relation : Set) := RelationBetween(relation, A, A)
predicate LessEqualOperation (A relation : Set) := RelationBetween(relation, A, A)
predicate OfNat (A n value : Set) := Nat(n) ∧ value ∈ A

predicate IsMagma (A op : Set) := FunctionBetween(op, A × A, A)
predicate Associative (A op : Set) := ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, op(op(x, y), z) = op(x, op(y, z))
predicate Commutative (A op : Set) := ∀ x ∈ A, ∀ y ∈ A, op(x, y) = op(y, x)
predicate Identity (A op unit : Set) := unit ∈ A ∧ (∀ x ∈ A, op(unit, x) = x ∧ op(x, unit) = x)
predicate Inverse (A op unit inv : Set) := FunctionBetween(inv, A, A) ∧ (∀ x ∈ A, op(inv(x), x) = unit ∧ op(x, inv(x)) = unit)
predicate Distributive (A add mul : Set) := ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, mul(x, add(y, z)) = add(mul(x, y), mul(x, z)) ∧ mul(add(x, y), z) = add(mul(x, z), mul(y, z))

predicate IsSemigroup (A op : Set) := IsMagma(A, op) ∧ Associative(A, op)
predicate IsMonoid (A op unit : Set) := IsSemigroup(A, op) ∧ Identity(A, op, unit)
predicate IsCommMonoid (A op unit : Set) := IsMonoid(A, op, unit) ∧ Commutative(A, op)
predicate IsGroup (A op unit inv : Set) := IsMonoid(A, op, unit) ∧ Inverse(A, op, unit, inv)
predicate IsAbelianGroup (A op unit inv : Set) := IsGroup(A, op, unit, inv) ∧ Commutative(A, op)

predicate IsSemiring (A add zero mul one : Set) := IsCommMonoid(A, add, zero) ∧ (IsMonoid(A, mul, one) ∧ Distributive(A, add, mul))
predicate IsRing (A add zero neg mul one : Set) := IsAbelianGroup(A, add, zero, neg) ∧ (IsMonoid(A, mul, one) ∧ Distributive(A, add, mul))

notation scoped IsRing(R) => IsRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

predicate ReflexiveOn (A relation : Set) := ∀ x ∈ A, relates(relation, x, x)
predicate TransitiveOn (A relation : Set) := ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, relates(relation, x, y) → relates(relation, y, z) → relates(relation, x, z)
predicate AntisymmetricOn (A relation : Set) := ∀ x ∈ A, ∀ y ∈ A, relates(relation, x, y) → relates(relation, y, x) → x = y
predicate IsPreorder (A relation : Set) := RelationBetween(relation, A, A) ∧ (ReflexiveOn(A, relation) ∧ TransitiveOn(A, relation))
predicate IsPartialOrder (A relation : Set) := IsPreorder(A, relation) ∧ AntisymmetricOn(A, relation)

-- These projection lemmas are the certificates that a future instance
-- resolver will insert.  Resolution is elaboration; these are
-- first-order theorems checked by the kernel.
theorem IsMonoid.semigroup (A op unit : Set)
  requires h : IsMonoid(A, op, unit)
  shows IsSemigroup(A, op)
proof
  rcases h with ⟨semigroup, identity⟩
  exact semigroup

theorem IsGroup.monoid (A op unit inv : Set)
  requires h : IsGroup(A, op, unit, inv)
  shows IsMonoid(A, op, unit)
proof
  rcases h with ⟨monoid, inverse⟩
  exact monoid

theorem IsSemiring.additive (A add zero mul one : Set)
  requires h : IsSemiring(A, add, zero, mul, one)
  shows IsCommMonoid(A, add, zero)
proof
  rcases h with ⟨additive, rest⟩
  exact additive

theorem IsSemiring.multiplicative (A add zero mul one : Set)
  requires h : IsSemiring(A, add, zero, mul, one)
  shows IsMonoid(A, mul, one)
proof
  rcases h with ⟨additive, multiplicative, distributive⟩
  exact multiplicative

theorem IsPartialOrder.preorder (A relation : Set)
  requires h : IsPartialOrder(A, relation)
  shows IsPreorder(A, relation)
proof
  rcases h with ⟨preorder, antisymmetric⟩
  exact preorder

end Algebra

export open Grace.Cumulus.Algebra.Foundation.Algebra