2 files changed, 88 insertions, 0 deletions
diff --git a/src/tests/nat.spec.ts b/src/tests/nat.spec.ts
new file mode 100644
index 0000000..acade6f
--- /dev/null
+++ b/src/tests/nat.spec.ts
@@ -0,0 +1,60 @@
+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 = [
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', _0>>, addition.Identity<'B'>>,
+      Add<'A', 'B'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<Add<'A', 'B'>, _0>, addition.Identity<Add<'A', 'B'>>>,
+      Add<'A', 'B'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', 'B'>, Sym<addition.Identity<Add<'A', 'B'>>>>,
+      Add<Add<'A', 'B'>, _0>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', Add<'C', _0>>>, addition.Identity<'C'>>,
+      Add<'A', Add<'B', 'C'>>
+    >>,
+  ]
+
+  export type specCommutativity = [
+    assert<Eq<
+      ApplyRewrite<Add<'A', 'B'>, addition.Commutativity<'A', 'B'>>,
+      Add<'B', 'A'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, addition.Commutativity<'A', 'B'>>,
+      Add<Add<'B', 'A'>, 'C'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', 'C'>>, addition.Commutativity<'B', 'C'>>,
+      Add<'A', Add<'C', 'B'>>
+    >>,
+  ]
+}
+
+export namespace multiplication_spec {
+  export type specCommutativity = [
+    assert<Eq<
+      ApplyRewrite<Multiply<Multiply<'A', 'B'>, 'C'>, multiplication.Commutativity<'A', 'B'>>,
+      Multiply<Multiply<'B', 'A'>, 'C'>
+    >>,
+  ]
+  export type specDistributivity = [
+    assert<Eq<
+      Evaluate<multiplication.Distributivity<'A', 'B', 'C'>>,
+      Add<Multiply<'A', 'C'>, Multiply<'B', 'C'>>
+    >>,
+  ]
+  export type specAssociativity = [
+    assert<Eq<
+      Evaluate<multiplication.Associativity<'A', 'B', 'C'>>,
+      Multiply<'A', Multiply<'B', 'C'>>
+    >>,
+  ]
+}
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'>>
+  >>,
+]