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)
initial commit
+7
Cargo.lock
+7
Cargo.lock
+6
Cargo.toml
+6
Cargo.toml
+96
flake.lock
+96
flake.lock
···
···
1
+
{
2
+
"nodes": {
3
+
"flake-utils": {
4
+
"inputs": {
5
+
"systems": "systems"
6
+
},
7
+
"locked": {
8
+
"lastModified": 1731533236,
9
+
"narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
10
+
"owner": "numtide",
11
+
"repo": "flake-utils",
12
+
"rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
13
+
"type": "github"
14
+
},
15
+
"original": {
16
+
"owner": "numtide",
17
+
"repo": "flake-utils",
18
+
"type": "github"
19
+
}
20
+
},
21
+
"nixpkgs": {
22
+
"locked": {
23
+
"lastModified": 1756617294,
24
+
"narHash": "sha256-aGnd4AHIYCWQKChAkHPpX+YYCt7pA6y2LFFA/s8q0wQ=",
25
+
"owner": "nixos",
26
+
"repo": "nixpkgs",
27
+
"rev": "b4c2c57c31e68544982226d07e4719a2d86302a8",
28
+
"type": "github"
29
+
},
30
+
"original": {
31
+
"owner": "nixos",
32
+
"ref": "nixos-25.05",
33
+
"repo": "nixpkgs",
34
+
"type": "github"
35
+
}
36
+
},
37
+
"nixpkgs_2": {
38
+
"locked": {
39
+
"lastModified": 1744536153,
40
+
"narHash": "sha256-awS2zRgF4uTwrOKwwiJcByDzDOdo3Q1rPZbiHQg/N38=",
41
+
"owner": "NixOS",
42
+
"repo": "nixpkgs",
43
+
"rev": "18dd725c29603f582cf1900e0d25f9f1063dbf11",
44
+
"type": "github"
45
+
},
46
+
"original": {
47
+
"owner": "NixOS",
48
+
"ref": "nixpkgs-unstable",
49
+
"repo": "nixpkgs",
50
+
"type": "github"
51
+
}
52
+
},
53
+
"root": {
54
+
"inputs": {
55
+
"flake-utils": "flake-utils",
56
+
"nixpkgs": "nixpkgs",
57
+
"rust-overlay": "rust-overlay"
58
+
}
59
+
},
60
+
"rust-overlay": {
61
+
"inputs": {
62
+
"nixpkgs": "nixpkgs_2"
63
+
},
64
+
"locked": {
65
+
"lastModified": 1756694554,
66
+
"narHash": "sha256-z/Iy4qvcMqzhA2IAAg71Sw4BrMwbBHvCS90ZoPLsnIk=",
67
+
"owner": "oxalica",
68
+
"repo": "rust-overlay",
69
+
"rev": "b29e5365120f344fe7161f14fc9e272fcc41ee56",
70
+
"type": "github"
71
+
},
72
+
"original": {
73
+
"owner": "oxalica",
74
+
"repo": "rust-overlay",
75
+
"type": "github"
76
+
}
77
+
},
78
+
"systems": {
79
+
"locked": {
80
+
"lastModified": 1681028828,
81
+
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
82
+
"owner": "nix-systems",
83
+
"repo": "default",
84
+
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
85
+
"type": "github"
86
+
},
87
+
"original": {
88
+
"owner": "nix-systems",
89
+
"repo": "default",
90
+
"type": "github"
91
+
}
92
+
}
93
+
},
94
+
"root": "root",
95
+
"version": 7
96
+
}
+29
flake.nix
+29
flake.nix
···
···
1
+
{
2
+
description = "rspeano";
3
+
4
+
inputs = {
5
+
nixpkgs.url = "github:nixos/nixpkgs/nixos-25.05";
6
+
rust-overlay.url = "github:oxalica/rust-overlay";
7
+
flake-utils.url = "github:numtide/flake-utils";
8
+
};
9
+
10
+
outputs = { self, nixpkgs, rust-overlay, flake-utils, ... }:
11
+
flake-utils.lib.eachDefaultSystem (system:
12
+
let
13
+
overlays = [ (import rust-overlay) ];
14
+
pkgs = import nixpkgs {
15
+
inherit system overlays;
16
+
};
17
+
18
+
# Change version here if needed
19
+
rsTools = pkgs.rust-bin.stable."1.89.0".default;
20
+
in {
21
+
22
+
devShells.default = pkgs.mkShell {
23
+
packages = [
24
+
rsTools
25
+
pkgs.bash ];
26
+
};
27
+
28
+
});
29
+
}
+115
src/lib.rs
+115
src/lib.rs
···
···
1
+
pub trait Nat {}
2
+
pub struct Succ<T>(T);
3
+
4
+
// Inductively define naturals
5
+
pub type _0 = Succ<()>;
6
+
impl Nat for _0 {}
7
+
impl<T: Nat> Nat for Succ<T> {}
8
+
9
+
pub 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
+
19
+
pub use super::{
20
+
Nat,
21
+
Succ,
22
+
_0,
23
+
eq::Eq,
24
+
eq::ProofEq,
25
+
add::Add,
26
+
mul::Times,
27
+
exp::Exp
28
+
};
29
+
}
30
+
31
+
pub mod eq {
32
+
use super::prelude::*;
33
+
34
+
pub trait Eq<A: Nat, B: Nat> {
35
+
fn check() -> () {}
36
+
}
37
+
38
+
pub struct ProofEq<A: Nat, B: Nat>(A, B);
39
+
impl<A: Nat, B: Nat> ProofEq<A, B> {}
40
+
41
+
// Define equality of naturals
42
+
impl<T: Nat> Eq<T, T> for ProofEq<T, T> {}
43
+
}
44
+
45
+
pub mod add {
46
+
use super::prelude::*;
47
+
48
+
pub trait Add<RHS: Nat> {
49
+
type Result: Nat;
50
+
}
51
+
52
+
// Base case
53
+
// N + 0 = N
54
+
impl<T: Nat> Add<_0> for T {
55
+
type Result = T;
56
+
}
57
+
58
+
// Induction
59
+
// A + S(B) = S(A + B)
60
+
impl<A: Nat, B: Nat> Add<Succ<B>> for A
61
+
where
62
+
A: Add<B>
63
+
{
64
+
type Result = Succ<<A as Add<B>>::Result>;
65
+
}
66
+
}
67
+
68
+
pub mod mul {
69
+
use super::prelude::*;
70
+
71
+
pub trait Times<RHS: Nat> {
72
+
type Result: Nat;
73
+
}
74
+
75
+
// Base case
76
+
// N * 0 = 0
77
+
impl<T: Nat> Times<_0> for T {
78
+
type Result = _0;
79
+
}
80
+
81
+
// Induction
82
+
// A * S(B) = A * B + A
83
+
impl<A: Nat, B: Nat> Times<Succ<B>> for A
84
+
where
85
+
A: Times<B>,
86
+
<A as Times<B>>::Result: Add<A>
87
+
{
88
+
type Result = <<A as Times<B>>::Result as Add<A>>::Result;
89
+
}
90
+
}
91
+
92
+
pub mod exp {
93
+
use super::prelude::*;
94
+
95
+
pub trait Exp<Pow: Nat> {
96
+
type Result: Nat;
97
+
}
98
+
99
+
// Base case
100
+
// N ^ 0 = 1
101
+
impl<T: Nat> Exp<_0> for T {
102
+
type Result = _1;
103
+
}
104
+
105
+
// Induction
106
+
// A ^ S(B) = A ^ B * A
107
+
impl<A: Nat, B: Nat> Exp<Succ<B>> for A
108
+
where
109
+
A: Exp<B>,
110
+
<A as Exp<B>>::Result: Times<A>
111
+
{
112
+
type Result =
113
+
<<A as Exp<B>>::Result as Times<A>>::Result;
114
+
}
115
+
}
+65
src/main.rs
+65
src/main.rs
···
···
1
+
use rspeano::prelude::*;
2
+
3
+
fn five_plus_five_is_ten() {
4
+
type Claimed10 = <_5 as Add<_5>>::Result;
5
+
6
+
type Verified10 =
7
+
Succ< // 1
8
+
Succ< // 2
9
+
Succ< // 3
10
+
Succ< // 4
11
+
Succ< // 5
12
+
Succ< // 6
13
+
Succ< // 7
14
+
Succ< // 8
15
+
Succ< // 9
16
+
Succ< // 10
17
+
_0
18
+
>>>>>>>>>>;
19
+
20
+
ProofEq::<Claimed10, Verified10>::check();
21
+
}
22
+
23
+
fn four_times_two_is_eight() {
24
+
type Claimed8 = <_4 as Times<_2>>::Result;
25
+
26
+
type Verified8 =
27
+
Succ< // 1
28
+
Succ< // 2
29
+
Succ< // 3
30
+
Succ< // 4
31
+
Succ< // 5
32
+
Succ< // 6
33
+
Succ< // 7
34
+
Succ< // 8
35
+
_0
36
+
>>>>>>>>;
37
+
38
+
ProofEq::<Claimed8, Verified8>::check();
39
+
}
40
+
41
+
fn two_squared_is_four() {
42
+
type Claimed4 = <_2 as Exp<_2>>::Result;
43
+
44
+
type Verified4 =
45
+
Succ<
46
+
Succ<
47
+
Succ<
48
+
Succ<
49
+
_0
50
+
>>>>;
51
+
52
+
ProofEq::<Claimed4, Verified4>::check();
53
+
}
54
+
55
+
fn main() {
56
+
two_squared_is_four();
57
+
58
+
four_times_two_is_eight();
59
+
60
+
// fails:
61
+
// type M0 = <_8 as Times<_1>>::Result;
62
+
// ProofEq::<M0, _0>::check();
63
+
64
+
five_plus_five_is_ten()
65
+
}