karpal_proof/
property.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4use core::marker::PhantomData;
5
6/// Marker trait for algebraic properties that can be witnessed.
7///
8/// A `Property` names a specific algebraic law. Zero-sized types
9/// implement this trait to declare what law they represent.
10pub trait Property {
11    /// Human-readable name of the property.
12    const NAME: &'static str;
13}
14
15/// Property P implies property Q: if P holds, then Q also holds.
16pub trait Implies<Q> {}
17
18// ---------------------------------------------------------------------------
19// Semigroup / Monoid properties
20// ---------------------------------------------------------------------------
21
22/// The binary operation is associative: `a ∘ (b ∘ c) = (a ∘ b) ∘ c`.
23pub struct IsAssociative;
24impl Property for IsAssociative {
25    const NAME: &'static str = "associativity";
26}
27
28/// There exists a left identity: `e ∘ a = a`.
29pub struct HasLeftIdentity;
30impl Property for HasLeftIdentity {
31    const NAME: &'static str = "left identity";
32}
33
34/// There exists a right identity: `a ∘ e = a`.
35pub struct HasRightIdentity;
36impl Property for HasRightIdentity {
37    const NAME: &'static str = "right identity";
38}
39
40/// The type forms a monoid: associative with two-sided identity.
41pub struct IsMonoid;
42impl Property for IsMonoid {
43    const NAME: &'static str = "monoid";
44}
45
46// IsMonoid implies each constituent property
47impl Implies<IsAssociative> for IsMonoid {}
48impl Implies<HasLeftIdentity> for IsMonoid {}
49impl Implies<HasRightIdentity> for IsMonoid {}
50
51// ---------------------------------------------------------------------------
52// Group properties
53// ---------------------------------------------------------------------------
54
55/// Every element has a left inverse: `a⁻¹ ∘ a = e`.
56pub struct HasLeftInverse;
57impl Property for HasLeftInverse {
58    const NAME: &'static str = "left inverse";
59}
60
61/// Every element has a right inverse: `a ∘ a⁻¹ = e`.
62pub struct HasRightInverse;
63impl Property for HasRightInverse {
64    const NAME: &'static str = "right inverse";
65}
66
67/// The type forms a group: monoid with two-sided inverses.
68pub struct IsGroup;
69impl Property for IsGroup {
70    const NAME: &'static str = "group";
71}
72
73impl Implies<IsMonoid> for IsGroup {}
74impl Implies<IsAssociative> for IsGroup {}
75impl Implies<HasLeftIdentity> for IsGroup {}
76impl Implies<HasRightIdentity> for IsGroup {}
77impl Implies<HasLeftInverse> for IsGroup {}
78impl Implies<HasRightInverse> for IsGroup {}
79
80// ---------------------------------------------------------------------------
81// Commutativity
82// ---------------------------------------------------------------------------
83
84/// The binary operation is commutative: `a ∘ b = b ∘ a`.
85pub struct IsCommutative;
86impl Property for IsCommutative {
87    const NAME: &'static str = "commutativity";
88}
89
90/// The type forms an abelian group: commutative group.
91pub struct IsAbelianGroup;
92impl Property for IsAbelianGroup {
93    const NAME: &'static str = "abelian group";
94}
95
96impl Implies<IsGroup> for IsAbelianGroup {}
97impl Implies<IsMonoid> for IsAbelianGroup {}
98impl Implies<IsAssociative> for IsAbelianGroup {}
99impl Implies<IsCommutative> for IsAbelianGroup {}
100impl Implies<HasLeftInverse> for IsAbelianGroup {}
101impl Implies<HasRightInverse> for IsAbelianGroup {}
102impl Implies<HasLeftIdentity> for IsAbelianGroup {}
103impl Implies<HasRightIdentity> for IsAbelianGroup {}
104
105// ---------------------------------------------------------------------------
106// Semiring / Ring / Field properties
107// ---------------------------------------------------------------------------
108
109/// Addition is commutative.
110pub struct AdditivelyCommutative;
111impl Property for AdditivelyCommutative {
112    const NAME: &'static str = "additively commutative";
113}
114
115/// Multiplication distributes over addition.
116pub struct IsDistributive;
117impl Property for IsDistributive {
118    const NAME: &'static str = "distributive";
119}
120
121/// Zero annihilates: `0 * a = a * 0 = 0`.
122pub struct ZeroAnnihilates;
123impl Property for ZeroAnnihilates {
124    const NAME: &'static str = "zero annihilation";
125}
126
127/// The type forms a semiring.
128pub struct IsSemiring;
129impl Property for IsSemiring {
130    const NAME: &'static str = "semiring";
131}
132
133impl Implies<AdditivelyCommutative> for IsSemiring {}
134impl Implies<IsDistributive> for IsSemiring {}
135impl Implies<ZeroAnnihilates> for IsSemiring {}
136
137/// The type forms a ring: semiring with additive inverses.
138pub struct IsRing;
139impl Property for IsRing {
140    const NAME: &'static str = "ring";
141}
142
143impl Implies<IsSemiring> for IsRing {}
144impl Implies<AdditivelyCommutative> for IsRing {}
145impl Implies<IsDistributive> for IsRing {}
146
147/// The type forms a field: ring with multiplicative inverses (for nonzero).
148pub struct IsField;
149impl Property for IsField {
150    const NAME: &'static str = "field";
151}
152
153impl Implies<IsRing> for IsField {}
154impl Implies<IsSemiring> for IsField {}
155
156// ---------------------------------------------------------------------------
157// Lattice properties
158// ---------------------------------------------------------------------------
159
160/// The operation is idempotent: `a ∘ a = a`.
161pub struct IsIdempotent;
162impl Property for IsIdempotent {
163    const NAME: &'static str = "idempotent";
164}
165
166/// Meet and join satisfy absorption: `a ∧ (a ∨ b) = a`.
167pub struct IsAbsorptive;
168impl Property for IsAbsorptive {
169    const NAME: &'static str = "absorptive";
170}
171
172/// The type forms a lattice.
173pub struct IsLattice;
174impl Property for IsLattice {
175    const NAME: &'static str = "lattice";
176}
177
178impl Implies<IsIdempotent> for IsLattice {}
179impl Implies<IsAbsorptive> for IsLattice {}
180impl Implies<IsCommutative> for IsLattice {}
181impl Implies<IsAssociative> for IsLattice {}
182
183/// The type forms a bounded lattice: lattice with top and bottom.
184pub struct IsBoundedLattice;
185impl Property for IsBoundedLattice {
186    const NAME: &'static str = "bounded lattice";
187}
188
189impl Implies<IsLattice> for IsBoundedLattice {}
190impl Implies<IsIdempotent> for IsBoundedLattice {}
191impl Implies<IsAbsorptive> for IsBoundedLattice {}
192
193// ---------------------------------------------------------------------------
194// Functor / Monad properties
195// ---------------------------------------------------------------------------
196
197/// `fmap(id, fa) == fa`.
198pub struct FunctorIdentity;
199impl Property for FunctorIdentity {
200    const NAME: &'static str = "functor identity";
201}
202
203/// `fmap(g . f, fa) == fmap(g, fmap(f, fa))`.
204pub struct FunctorComposition;
205impl Property for FunctorComposition {
206    const NAME: &'static str = "functor composition";
207}
208
209/// The type is a lawful functor.
210pub struct IsLawfulFunctor;
211impl Property for IsLawfulFunctor {
212    const NAME: &'static str = "lawful functor";
213}
214
215impl Implies<FunctorIdentity> for IsLawfulFunctor {}
216impl Implies<FunctorComposition> for IsLawfulFunctor {}
217
218/// `pure(a) >>= f == f(a)`.
219pub struct MonadLeftIdentity;
220impl Property for MonadLeftIdentity {
221    const NAME: &'static str = "monad left identity";
222}
223
224/// `m >>= pure == m`.
225pub struct MonadRightIdentity;
226impl Property for MonadRightIdentity {
227    const NAME: &'static str = "monad right identity";
228}
229
230/// `(m >>= f) >>= g == m >>= (|x| f(x) >>= g)`.
231pub struct MonadAssociativity;
232impl Property for MonadAssociativity {
233    const NAME: &'static str = "monad associativity";
234}
235
236/// The type is a lawful monad.
237pub struct IsLawfulMonad;
238impl Property for IsLawfulMonad {
239    const NAME: &'static str = "lawful monad";
240}
241
242impl Implies<IsLawfulFunctor> for IsLawfulMonad {}
243impl Implies<MonadLeftIdentity> for IsLawfulMonad {}
244impl Implies<MonadRightIdentity> for IsLawfulMonad {}
245impl Implies<MonadAssociativity> for IsLawfulMonad {}
246
247// ---------------------------------------------------------------------------
248// Compound property: conjunction of two properties
249// ---------------------------------------------------------------------------
250
251/// Both properties P and Q hold simultaneously.
252///
253/// Use `Proven::and()` to combine two witnesses into `Proven<And<P, Q>, T>`,
254/// then `derive()` to extract either constituent via the `Implies` impls.
255///
256/// Note: Due to Rust's coherence rules, only `Implies<P>` (the first
257/// component) is provided as a blanket impl. To extract `Q`, use the
258/// dedicated `Proven<And<P, Q>, T>::derive_second()` method.
259pub struct And<P, Q>(PhantomData<(P, Q)>);
260impl<P: Property, Q: Property> Property for And<P, Q> {
261    const NAME: &'static str = "conjunction";
262}
263
264// Only the first component as a blanket — second would conflict when P=Q.
265impl<P, Q> Implies<P> for And<P, Q> {}
266
267#[cfg(test)]
268mod tests {
269    use super::*;
270
271    #[test]
272    fn property_names() {
273        assert_eq!(IsAssociative::NAME, "associativity");
274        assert_eq!(IsMonoid::NAME, "monoid");
275        assert_eq!(IsGroup::NAME, "group");
276        assert_eq!(IsAbelianGroup::NAME, "abelian group");
277        assert_eq!(IsSemiring::NAME, "semiring");
278        assert_eq!(IsRing::NAME, "ring");
279        assert_eq!(IsField::NAME, "field");
280        assert_eq!(IsLattice::NAME, "lattice");
281        assert_eq!(IsBoundedLattice::NAME, "bounded lattice");
282        assert_eq!(IsLawfulFunctor::NAME, "lawful functor");
283        assert_eq!(IsLawfulMonad::NAME, "lawful monad");
284    }
285
286    // Compile-time test: implication chains
287    fn _assert_implies<P: Implies<Q>, Q>() {}
288
289    #[test]
290    fn implication_lattice_compiles() {
291        _assert_implies::<IsMonoid, IsAssociative>();
292        _assert_implies::<IsMonoid, HasLeftIdentity>();
293        _assert_implies::<IsGroup, IsMonoid>();
294        _assert_implies::<IsGroup, IsAssociative>();
295        _assert_implies::<IsAbelianGroup, IsGroup>();
296        _assert_implies::<IsAbelianGroup, IsCommutative>();
297        _assert_implies::<IsField, IsRing>();
298        _assert_implies::<IsRing, IsSemiring>();
299        _assert_implies::<IsBoundedLattice, IsLattice>();
300        _assert_implies::<IsLawfulMonad, IsLawfulFunctor>();
301        _assert_implies::<And<IsAssociative, IsCommutative>, IsAssociative>();
302        // Second component extracted via Proven::derive_second(), not Implies
303    }
304}
karpal_proof/property.rs

karpal_proof/
property.rs
