Grace/Cumulus/Algebra/Foundation.g17

Open in Workbench Download source

Imports

Set.Relation

Declarations

• call2 def
• AddOperation predicate
• MulOperation predicate
• DivOperation predicate
• NegOperation predicate
• LessOperation predicate
• LessEqualOperation predicate
• OfNat predicate
• IsMagma predicate
• Associative predicate
• Commutative predicate
• Identity predicate
• Inverse predicate
• Distributive predicate
• IsSemigroup predicate
• IsMonoid predicate
• IsCommMonoid predicate
• IsGroup predicate
• IsAbelianGroup predicate
• IsSemiring predicate
• IsRing predicate
• ReflexiveOn predicate
• TransitiveOn predicate
• AntisymmetricOn predicate
• IsPreorder predicate
• IsPartialOrder predicate
• IsMonoid.semigroup theorem derivation
• IsGroup.monoid theorem derivation
• IsSemiring.additive theorem derivation
• IsSemiring.multiplicative theorem derivation
• IsPartialOrder.preorder theorem derivation

Source

1-- Set-theoretic algebraic interfaces2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Foundation8import Set.Relation910namespace Algebra1112-- Algebraic operations are sets of ordered pairs, that is, set-theoretic13-- functions.  A unary operation applies as any function does, inv(x); a14-- binary operation applies to the pair of its arguments, written op(x, y).15def call2 (op x y : Set) : Set := op((x, y))1617-- Type-class interfaces for notation.  These are set-theoretic18-- predicates, separate from the `class` declaration form.  Their checked19-- `instance` theorems let elaboration synthesize the operation or constant20-- from a carrier; the kernel receives only applications and call2 terms.21predicate AddOperation (A op : Set) := FunctionBetween(op, A × A, A)22predicate MulOperation (A op : Set) := FunctionBetween(op, A × A, A)23predicate DivOperation (A op : Set) := FunctionBetween(op, A × A, A)24predicate NegOperation (A op : Set) := FunctionBetween(op, A, A)25predicate LessOperation (A relation : Set) := RelationBetween(relation, A, A)26predicate LessEqualOperation (A relation : Set) := RelationBetween(relation, A, A)27predicate OfNat (A n value : Set) := Nat(n) ∧ value ∈ A2829predicate IsMagma (A op : Set) := FunctionBetween(op, A × A, A)30predicate Associative (A op : Set) := ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, op(op(x, y), z) = op(x, op(y, z))31predicate Commutative (A op : Set) := ∀ x ∈ A, ∀ y ∈ A, op(x, y) = op(y, x)32predicate Identity (A op unit : Set) := unit ∈ A ∧ (∀ x ∈ A, op(unit, x) = x ∧ op(x, unit) = x)33predicate Inverse (A op unit inv : Set) := FunctionBetween(inv, A, A) ∧ (∀ x ∈ A, op(inv(x), x) = unit ∧ op(x, inv(x)) = unit)34predicate 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))3536predicate IsSemigroup (A op : Set) := IsMagma(A, op) ∧ Associative(A, op)37predicate IsMonoid (A op unit : Set) := IsSemigroup(A, op) ∧ Identity(A, op, unit)38predicate IsCommMonoid (A op unit : Set) := IsMonoid(A, op, unit) ∧ Commutative(A, op)39predicate IsGroup (A op unit inv : Set) := IsMonoid(A, op, unit) ∧ Inverse(A, op, unit, inv)40predicate IsAbelianGroup (A op unit inv : Set) := IsGroup(A, op, unit, inv) ∧ Commutative(A, op)4142predicate IsSemiring (A add zero mul one : Set) := IsCommMonoid(A, add, zero) ∧ (IsMonoid(A, mul, one) ∧ Distributive(A, add, mul))43predicate IsRing (A add zero neg mul one : Set) := IsAbelianGroup(A, add, zero, neg) ∧ (IsMonoid(A, mul, one) ∧ Distributive(A, add, mul))4445notation scoped IsRing(R) => IsRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)4647predicate ReflexiveOn (A relation : Set) := ∀ x ∈ A, relates(relation, x, x)48predicate TransitiveOn (A relation : Set) := ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, relates(relation, x, y) → relates(relation, y, z) → relates(relation, x, z)49predicate AntisymmetricOn (A relation : Set) := ∀ x ∈ A, ∀ y ∈ A, relates(relation, x, y) → relates(relation, y, x) → x = y50predicate IsPreorder (A relation : Set) := RelationBetween(relation, A, A) ∧ (ReflexiveOn(A, relation) ∧ TransitiveOn(A, relation))51predicate IsPartialOrder (A relation : Set) := IsPreorder(A, relation) ∧ AntisymmetricOn(A, relation)5253-- These projection lemmas are the certificates that a future instance54-- resolver will insert.  Resolution is elaboration; these are55-- first-order theorems checked by the kernel.56theorem IsMonoid.semigroup (A op unit : Set)57  requires h : IsMonoid(A, op, unit)58  shows IsSemigroup(A, op)59proof60  rcases h with ⟨semigroup, identity⟩61  exact semigroup6263theorem IsGroup.monoid (A op unit inv : Set)64  requires h : IsGroup(A, op, unit, inv)65  shows IsMonoid(A, op, unit)66proof67  rcases h with ⟨monoid, inverse⟩68  exact monoid6970theorem IsSemiring.additive (A add zero mul one : Set)71  requires h : IsSemiring(A, add, zero, mul, one)72  shows IsCommMonoid(A, add, zero)73proof74  rcases h with ⟨additive, rest⟩75  exact additive7677theorem IsSemiring.multiplicative (A add zero mul one : Set)78  requires h : IsSemiring(A, add, zero, mul, one)79  shows IsMonoid(A, mul, one)80proof81  rcases h with ⟨additive, multiplicative, distributive⟩82  exact multiplicative8384theorem IsPartialOrder.preorder (A relation : Set)85  requires h : IsPartialOrder(A, relation)86  shows IsPreorder(A, relation)87proof88  rcases h with ⟨preorder, antisymmetric⟩89  exact preorder9091end Algebra9293export open Grace.Cumulus.Algebra.Foundation.Algebra94