feat: commutativity + identity for multiplication

4 files changed, 100 insertions, 51 deletions

diff --git a/src/index.ts b/src/index.ts
index a161134..4c3f114 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,5 +1,5 @@
-import { Add, Multiply, Succ, _0 } from './nat';
-import { Op, Rewrite, ChainRewrites, Flip, Equation, Refl } from './util';
+import { Add, Multiply, Succ, _0, _1, _3 } from './nat';
+import { Op, Rewrite, ChainRewrites, Flip, Equation, Refl, VerifyEquation, assert } from './util';
 
 export namespace addition {
   export type Identity<A extends Op> = Rewrite<Add<A, _0>, A>;
@@ -53,5 +53,53 @@ export namespace addition {
       Refl<Succ<Add<A, Add<B, C>>>>,   // true
     ], this['left']>;
   };
+
+  export namespace spec {
+    export type commutativity = [
+      assert<VerifyEquation<Comm_Base<'B'>>>,
+      assert<VerifyEquation<Comm_Inductive<'A', 'B'>>>,
+    ]
+
+    export type associativity = [
+      assert<VerifyEquation<Assoc_Base<'A', 'B'>>>,
+      assert<VerifyEquation<Assoc_Inductive<'A', 'B', 'C'>>>,
+    ]
+  }
+}
+
+export namespace multiplication {
+  export type Identity<A extends Op> = Rewrite<Multiply<A, _1>, A>;
+  export type IdentityR<A extends Op> = Rewrite<Multiply<_1, A>, A>;
+
+  export type Mul_Add<A extends Op, B extends Op> = Rewrite<Multiply<Succ<A>, B>, Add<A, Multiply<A, B>>>;
+  export type Mul_AddR<A extends Op, B extends Op> = Rewrite<Multiply<A, Succ<B>>, Add<B, Multiply<A, B>>>;
+
+  export type Commutativity<A extends Op, B extends Op> = Rewrite<Multiply<A, B>, Multiply<B, A>>;
+  export interface Comm_Base<B extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<_1, B>, Multiply<B, _1>>; // 1 * b = b * 1
+    right: ChainRewrites<[
+      IdentityR<B>,    // b = b + 0
+      Identity<B>,     // b = b
+      Refl<B>,         // true
+    ], this['left']>;
+  };
+  export interface Comm_Inductive<A extends Op, B extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<Succ<A>, B>, Multiply<B, Succ<A>>>; // succ(a)*b = b*succ(a)
+    right: ChainRewrites<[
+      Mul_Add<A, B>,                 // a + a*b = b*succ(a)
+      Mul_AddR<B, A>,                // a + a*b = a + b*a
+      Commutativity<B, A>,           // a + a*b = a + a*b
+      Refl<Add<A, Multiply<A, B>>>,  // true
+    ], this['left']>;
+  };
+
+  export namespace spec {
+    export type commutativity = [
+      assert<VerifyEquation<Comm_Base<'B'>>>,
+      assert<VerifyEquation<Comm_Inductive<'A', 'B'>>>,
+    ]
+  }
 }
 
diff --git a/src/nat.ts b/src/nat.ts
index 124c2c6..5c52bdf 100644
--- a/src/nat.ts
+++ b/src/nat.ts
@@ -1,6 +1,7 @@
 import { Op } from "./util";
 
 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 };
 export type Succ<A extends Op> = Add<'1', A>;
 
 export type _0 = '0'
diff --git a/src/tests.ts b/src/tests.ts
index f4530b4..5c066dc 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,47 +1,6 @@
-import { addition } from './index';
-import { Add } from './nat';
-import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation } from './util';
-
-type assert<T extends true> = T;
-
-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'>, Flip<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 type specCommutativityInduction = [
-  assert<VerifyEquation<addition.Comm_Base<'B'>>>,
-  assert<VerifyEquation<addition.Comm_Inductive<'A', 'B'>>>,
-]
+import { addition, multiplication } from './index';
+import { Add, Multiply, Succ } from './nat';
+import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert } from './util';
 
 export type specChainRewrites = [
   assert<Eq<
@@ -68,8 +27,47 @@ export type specChainRewrites = [
   >>,
 ]
 
-export type specAssociativityInduction = [
-  assert<VerifyEquation<addition.Assoc_Base<'B', 'C'>>>,
-  assert<VerifyEquation<addition.Assoc_Inductive<'A', 'B', 'C'>>>,
-]
+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'>, Flip<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'>
+    >>,
+  ]
+}
diff --git a/src/util.ts b/src/util.ts
index f6067ae..97e9335 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -13,7 +13,8 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
   : O extends string ? O
   : O extends { a: Op, b: Op, op: string } ? (
     ApplyRewrite<O['a'], R> extends O['a']
-    ? Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> }
+    ? (ApplyRewrite<O['b'], R> extends O['b'] ? O
+      : Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> })
     : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
   )
   : never;
@@ -33,6 +34,7 @@ export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> =
 export type VerifyEquation<Eq extends Rewrite<Op, Op>> =
   Eq['right'] extends 'true' ? true : false & Eq['right'];
 
+export type assert<T extends true> = T;
 export type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b });
 
 export type Equation<A extends Op, B extends Op> = { op: '=', a: A, b: B };