refactor: moves stuff around

7 files changed, 86 insertions, 82 deletions

diff --git a/package.json b/package.json
index 91f7ae3..7691cd2 100644
--- a/package.json
+++ b/package.json
@@ -7,7 +7,7 @@
   "author": "Akshay Nair <phenax5@gmail.com>",
   "license": "MIT",
   "scripts": {
-    "test": "tsc --noEmit ./src/tests.ts"
+    "test": "tsc --noEmit"
   },
   "dependencies": {
     "typescript": "^5.3.3"
diff --git a/src/equation.ts b/src/equation.ts
new file mode 100644
index 0000000..0ec25d6
--- /dev/null
+++ b/src/equation.ts
@@ -0,0 +1,51 @@
+import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem';
+
+export namespace equation {
+  type F<X extends Op> = { op: 'F', a: X };
+
+  export type Reflexivity<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
+
+  export type Symmetry<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<B, A>>;
+
+  export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>;
+
+  export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']>
+  export interface SubstituteEq_Proof<A extends Op, B extends Op> {
+    type: 'rewrite',
+    known: {
+      'a = b': Equation<A, B>,
+    },
+    left: Equation<F<A>, F<B>>; // f(a) = f(b)
+    right: ChainRewrites<[
+      Sym<Congruence<A, B>>,                   // a = b
+      SubstituteEq<this['known']['a = b']>,    // b = b
+      Reflexivity<B>,
+    ], this['left']>;
+  };
+  export namespace spec {
+    export type substitution = [
+      assert<VerifyEquation<SubstituteEq_Proof<'A', 'B'>>>,
+    ]
+  }
+
+  export interface Transitivity_Proof<A extends Op, B extends Op, C extends Op> {
+    type: 'rewrite',
+    known: {
+      'a = b': Equation<A, B>,
+      'b = c': Equation<B, C>,
+    },
+    left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c)
+    right: ChainRewrites<[
+      SubstituteEq<this['known']['a = b']>,                                 // (b = b) = (b = c)
+      SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>,   // (b = b) = (c = b)
+      Reflexivity<B>,                                                       // true = (b = b)
+      Reflexivity<B>,                                                       // true = true
+      Reflexivity<'true'>,
+    ], this['left']>;
+  };
+  export namespace spec {
+    export type transitivity = [
+      assert<VerifyEquation<Transitivity_Proof<'A', 'B', 'C'>>>,
+    ]
+  }
+}
diff --git a/src/index.ts b/src/natural-numbers.ts
index 4a00438..fa8a3ce 100644
--- a/src/index.ts
+++ b/src/natural-numbers.ts
@@ -1,5 +1,5 @@
-import { Add, Multiply, Succ, _0, _1, _3 } from './nat';
-import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './util';
+import { Add, Multiply, Succ, _0, _1, _3 } from './utils/nat';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem';
 
 export namespace addition {
   // Identity
@@ -184,53 +184,3 @@ export namespace multiplication {
     ]
   }
 }
-
-export namespace equation {
-  type F<X extends Op> = { op: 'F', a: X };
-
-  export type Reflexivity<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
-
-  export type Symmetry<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<B, A>>;
-
-  export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>;
-
-  export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']>
-  export interface SubstituteEq_Proof<A extends Op, B extends Op> {
-    type: 'rewrite',
-    known: {
-      'a = b': Equation<A, B>,
-    },
-    left: Equation<F<A>, F<B>>; // f(a) = f(b)
-    right: ChainRewrites<[
-      Sym<Congruence<A, B>>,                   // a = b
-      SubstituteEq<this['known']['a = b']>,    // b = b
-      Reflexivity<B>,
-    ], this['left']>;
-  };
-  export namespace spec {
-    export type substitution = [
-      assert<VerifyEquation<SubstituteEq_Proof<'A', 'B'>>>,
-    ]
-  }
-
-  export interface Transitivity_Proof<A extends Op, B extends Op, C extends Op> {
-    type: 'rewrite',
-    known: {
-      'a = b': Equation<A, B>,
-      'b = c': Equation<B, C>,
-    },
-    left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c)
-    right: ChainRewrites<[
-      SubstituteEq<this['known']['a = b']>,                                 // (b = b) = (b = c)
-      SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>,   // (b = b) = (c = b)
-      Reflexivity<B>,                                                       // true = (b = b)
-      Reflexivity<B>,                                                       // true = true
-      Reflexivity<'true'>,
-    ], this['left']>;
-  };
-  export namespace spec {
-    export type transitivity = [
-      assert<VerifyEquation<Transitivity_Proof<'A', 'B', 'C'>>>,
-    ]
-  }
-}
diff --git a/src/tests.ts b/src/tests/nat.spec.ts
index 7f331a6..acade6f 100644
--- a/src/tests.ts
+++ b/src/tests/nat.spec.ts
@@ -1,31 +1,6 @@
-import { addition, multiplication } from './index';
-import { Add, Multiply, Succ, _0 } from './nat';
-import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
-
-export type specChainRewrites = [
-  assert<Eq<
-    ChainRewrites<
-      [
-        addition.Commutativity<_0, 'B'>,
-        addition.Identity<'B'>,
-      ],
-      Add<Add<_0, 'B'>, 'C'>
-    >,
-    Add<'B', 'C'>
-  >>,
-  assert<Eq<
-    ChainRewrites<
-      [
-        addition.Commutativity<_0, 'B'>,
-        addition.Identity<'B'>,
-        Sym<addition.Identity<Add<'B', 'C'>>>,
-        addition.Commutativity<Add<'B', 'C'>, _0>,
-      ],
-      Add<Add<_0, 'B'>, 'C'>
-    >,
-    Add<_0, Add<'B', 'C'>>
-  >>,
-]
+import { addition, multiplication } from '../natural-numbers';
+import { Add, Multiply, _0 } from '../utils/nat';
+import { ApplyRewrite, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
 
 export namespace spec_addition {
   export type specIdentity = [
diff --git a/src/tests/theorem.spec.ts b/src/tests/theorem.spec.ts
new file mode 100644
index 0000000..4ab220a
--- /dev/null
+++ b/src/tests/theorem.spec.ts
@@ -0,0 +1,28 @@
+import { addition } from '../natural-numbers';
+import { Add, _0 } from '../utils/nat';
+import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
+
+export type specChainRewrites = [
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<'B', 'C'>
+  >>,
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+        Sym<addition.Identity<Add<'B', 'C'>>>,
+        addition.Commutativity<Add<'B', 'C'>, _0>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<_0, Add<'B', 'C'>>
+  >>,
+]
diff --git a/src/nat.ts b/src/utils/nat.ts
index 7491e82..af8f3da 100644
--- a/src/nat.ts
+++ b/src/utils/nat.ts
@@ -1,4 +1,4 @@
-import { Op } from './util';
+import { Op } from './theorem';
 
 export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B };
 export type Multiply<A extends Op, B extends Op> = { op: '*'; a: A; b: B };
diff --git a/src/util.ts b/src/utils/theorem.ts
index a4dd2e9..a4dd2e9 100644
--- a/src/util.ts
+++ b/src/utils/theorem.ts