ecsolticia.codeberg.page
Compile-time construction of Peano axioms-based natural numbers and addition, multiplication, and exponentiation defined through them within Rust. (Mirrored from Codeberg)
1pub trait Nat {}
2pub struct Succ<T>(T);
3
4// Inductively define naturals
5pub type _0 = ();
6impl Nat for _0 {}
7impl<T: Nat> Nat for Succ<T> {}
8
9pub mod prelude {
10 pub type _1 = Succ<_0>;
11 pub type _2 = Succ<_1>;
12 pub type _3 = Succ<_2>;
13 pub type _4 = Succ<_3>;
14 pub type _5 = Succ<_4>;
15 pub type _6 = Succ<_5>;
16 pub type _7 = Succ<_6>;
17 pub type _8 = Succ<_7>;
18 pub type _9 = Succ<_8>;
19 pub type _10 = Succ<_9>;
20
21 pub use super::{
22 Nat,
23 Succ,
24 _0,
25
26 eq::Eq,
27
28 leq::Leq,
29 geq::Geq,
30
31 add::Add,
32 mul::Mul,
33 exp::Exp,
34
35 parity::Even,
36 parity::Odd
37 };
38}
39
40pub mod eq {
41 use super::prelude::*;
42
43 pub trait Eq<A: Nat> {
44 fn equal() -> () {}
45 }
46
47 // Define equality of naturals
48 impl<A: Nat> Eq<A> for A {}
49}
50
51pub mod leq {
52 use super::prelude::*;
53
54 pub trait Leq<A: Nat> {
55 fn leq() -> () {}
56 }
57
58 // Base case
59 // 0 <= N for every N
60 impl<A: Nat> Leq<A> for _0 {}
61
62 // Induction
63 // A <= B means S(A) <= S(B)
64 impl<A: Nat, B: Nat> Leq<Succ<B>> for Succ<A>
65 where
66 A: Leq<B>
67 {}
68}
69
70pub mod geq {
71 use super::prelude::*;
72
73 pub trait Geq<A: Nat> {
74 fn geq() -> () {}
75 }
76
77 // If A <= B then B => A
78 impl<A: Nat, B: Nat> Geq<A> for B
79 where
80 A: Leq<B>
81 {}
82}
83
84pub mod add {
85 use super::prelude::*;
86
87 pub trait Add<RHS: Nat> {
88 type Sum: Nat;
89 }
90
91 // Base case
92 // N + 0 = N
93 impl<T: Nat> Add<_0> for T {
94 type Sum = T;
95 }
96
97 // Induction
98 // A + S(B) = S(A + B)
99 impl<A: Nat, B: Nat> Add<Succ<B>> for A
100 where
101 A: Add<B>
102 {
103 type Sum = Succ<<A as Add<B>>::Sum>;
104 }
105}
106
107pub mod mul {
108 use super::prelude::*;
109
110 pub trait Mul<RHS: Nat> {
111 type Prod: Nat;
112 }
113
114 // Base case
115 // N * 0 = 0
116 impl<T: Nat> Mul<_0> for T {
117 type Prod = _0;
118 }
119
120 // Induction
121 // A * S(B) = A * B + A
122 impl<A: Nat, B: Nat> Mul<Succ<B>> for A
123 where
124 A: Mul<B>,
125 <A as Mul<B>>::Prod: Add<A>
126 {
127 type Prod = <<A as Mul<B>>::Prod as Add<A>>::Sum;
128 }
129}
130
131pub mod exp {
132 use super::prelude::*;
133
134 pub trait Exp<P: Nat> {
135 type Pow: Nat;
136 }
137
138 // Base case
139 // N ^ 0 = 1
140 impl<T: Nat> Exp<_0> for T {
141 type Pow = _1;
142 }
143
144 // Induction
145 // A ^ S(B) = A ^ B * A
146 impl<A: Nat, B: Nat> Exp<Succ<B>> for A
147 where
148 A: Exp<B>,
149 <A as Exp<B>>::Pow: Mul<A>
150 {
151 type Pow =
152 <<A as Exp<B>>::Pow as Mul<A>>::Prod;
153 }
154}
155
156pub mod parity {
157 use super::prelude::*;
158
159 pub trait Even {
160 fn even() -> () {}
161 }
162
163 pub trait Odd {
164 fn odd() -> () {}
165 }
166
167 impl Even for _0 {}
168 impl<N: Even> Even for Succ<Succ<N>> {}
169
170 impl Odd for _1 {}
171 impl<N: Odd> Odd for Succ<Succ<N>> {}
172}