feat: associativity and commutativity for addition

1 files changed, 24 insertions, 34 deletions

diff --git a/src/tests.ts b/src/tests.ts
index d56cb30..f4530b4 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,49 +1,54 @@
-import { Add, Assoc, Assoc0, Assoc1, Commutativity, Identity, Succ } from './index';
-import { ApplyRewrite, ChainRewrites, Flip, Rewrite } from './util';
+import { addition } from './index';
+import { Add } from './nat';
+import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation } from './util';
 
-type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : false & { a: a; b: b });
 type assert<T extends true> = T;
 
 export type specIdentity = [
   assert<Eq<
-    ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>,
+    ApplyRewrite<Add<'A', Add<'B', '0'>>, addition.Identity<'B'>>,
     Add<'A', 'B'>
   >>,
   assert<Eq<
-    ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>,
+    ApplyRewrite<Add<Add<'A', 'B'>, '0'>, addition.Identity<Add<'A', 'B'>>>,
     Add<'A', 'B'>
   >>,
   assert<Eq<
-    ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>,
+    ApplyRewrite<Add<'A', 'B'>, Flip<addition.Identity<Add<'A', 'B'>>>>,
     Add<Add<'A', 'B'>, '0'>
   >>,
   assert<Eq<
-    ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>,
+    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'>, Commutativity<'A', 'B'>>,
+    ApplyRewrite<Add<'A', 'B'>, addition.Commutativity<'A', 'B'>>,
     Add<'B', 'A'>
   >>,
   assert<Eq<
-    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>,
+    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, addition.Commutativity<'A', 'B'>>,
     Add<Add<'B', 'A'>, 'C'>
   >>,
   assert<Eq<
-    ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>,
+    ApplyRewrite<Add<'A', Add<'B', 'C'>>, addition.Commutativity<'B', 'C'>>,
     Add<'A', Add<'C', 'B'>>
   >>,
 ]
 
+export type specCommutativityInduction = [
+  assert<VerifyEquation<addition.Comm_Base<'B'>>>,
+  assert<VerifyEquation<addition.Comm_Inductive<'A', 'B'>>>,
+]
+
 export type specChainRewrites = [
   assert<Eq<
     ChainRewrites<
       [
-        Commutativity<'0', 'B'>,
-        Identity<'B'>,
+        addition.Commutativity<'0', 'B'>,
+        addition.Identity<'B'>,
       ],
       Add<Add<'0', 'B'>, 'C'>
     >,
@@ -52,10 +57,10 @@ export type specChainRewrites = [
   assert<Eq<
     ChainRewrites<
       [
-        Commutativity<'0', 'B'>,
-        Identity<'B'>,
-        Flip<Identity<Add<'B', 'C'>>>,
-        Commutativity<Add<'B', 'C'>, '0'>,
+        addition.Commutativity<'0', 'B'>,
+        addition.Identity<'B'>,
+        Flip<addition.Identity<Add<'B', 'C'>>>,
+        addition.Commutativity<Add<'B', 'C'>, '0'>,
       ],
       Add<Add<'0', 'B'>, 'C'>
     >,
@@ -63,23 +68,8 @@ export type specChainRewrites = [
   >>,
 ]
 
-export type specAssoc0 = [
-  assert<Eq<
-    ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>,
-    Add<'0', Add<'B', 'C'>>
-  >>,
-  assert<Eq<
-    ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>,
-    Add<'0', Add<Add<'A', 'B'>, 'C'>>
-  >>,
-]
-
-export type specAssocN = [
-  assert<Eq<
-    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Assoc<'A', 'B', 'C'>>,
-    Add<'A', Add<'B', 'C'>>
-  >>,
+export type specAssociativityInduction = [
+  assert<VerifyEquation<addition.Assoc_Base<'B', 'C'>>>,
+  assert<VerifyEquation<addition.Assoc_Inductive<'A', 'B', 'C'>>>,
 ]
 
-
-