karpal_proof/
property.rs

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

karpal_proof/
property.rs
