From a393765df40744aae68dab943e25bad8175bd5c0 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Tue, 12 Dec 2023 20:21:13 +0530
Subject: feat: associativity + distributivity for multiplication

---
 src/index.ts | 90 ++++++++++++++++++++++++++++++++++++++++++++++++++----------
 src/tests.ts | 14 +++++++++-
 src/util.ts  |  2 ++
 3 files changed, 90 insertions(+), 16 deletions(-)

diff --git a/src/index.ts b/src/index.ts
index 4c3f114..2b6f59a 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -8,7 +8,6 @@ export namespace addition {
   export type SumSucc1<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>
   export type SumSucc2<A extends Op, B extends Op> = Rewrite<Add<A, Succ<B>>, Succ<Add<A, B>>>
 
-  /// Sum commutativity
   export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
   export interface Comm_Base<B extends Op> {
     type: 'rewrite',
@@ -29,8 +28,14 @@ export namespace addition {
       Refl<Succ<Add<B, A>>>,  // true
     ], this['left']>;
   };
+  export namespace spec {
+    export type commutativity = [
+      assert<VerifyEquation<Comm_Base<'B'>>>,
+      assert<VerifyEquation<Comm_Inductive<'A', 'B'>>>,
+    ]
+  }
+
 
-  // Sum associativity
   export type Associativity<A extends Op, B extends Op, C extends Op> = Rewrite<Add<Add<A, B>, C>, Add<A, Add<B, C>>>;
   export interface Assoc_Base<B extends Op, C extends Op> {
     type: 'rewrite',
@@ -55,11 +60,6 @@ export namespace addition {
   };
 
   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'>>>,
@@ -71,15 +71,15 @@ 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 Mul_Add<A extends Op, B extends Op> = Rewrite<Multiply<Succ<A>, B>, Add<B, Multiply<A, B>>>;
+  export type Mul_AddR<A extends Op, B extends Op> = Rewrite<Multiply<A, Succ<B>>, Add<A, 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
+      IdentityR<B>,    // b = b * 1
       Identity<B>,     // b = b
       Refl<B>,         // true
     ], this['left']>;
@@ -88,18 +88,78 @@ export namespace multiplication {
     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
+      Mul_Add<A, B>,                 // b + a*b = b*succ(a)
+      Mul_AddR<B, A>,                // b + a*b = b + b*a
+      Commutativity<B, A>,           // b + a*b = b + a*b
+      Refl<Add<B, Multiply<A, B>>>,  // true
     ], this['left']>;
   };
-
   export namespace spec {
     export type commutativity = [
       assert<VerifyEquation<Comm_Base<'B'>>>,
       assert<VerifyEquation<Comm_Inductive<'A', 'B'>>>,
     ]
   }
+
+  export type Distributivity<A extends Op, B extends Op, C extends Op> =
+    Rewrite<Multiply<Add<A, B>, C>, Add<Multiply<A, C>, Multiply<B, C>>>;
+  export interface Dist_Base<B extends Op, C extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<Add<_1, B>, C>, Add<Multiply<_1, C>, Multiply<B, C>>>; // (1 + b)*c = 1*c + b*c
+    right: ChainRewrites<[
+      IdentityR<C>,                    // (1 + b)*c = c + b*c
+      addition.SumSucc1<_0, B>,        // succ(0 + b)*c = c + b*c
+      addition.IdentityR<B>,           // succ(b)*c = c + b*c
+      Mul_Add<B, C>,                   // c + b*c = c + b*c
+      Refl<Add<C, Multiply<B, C>>>,    // true
+    ], this['left']>;
+  };
+  export interface Dist_Inductive<A extends Op, B extends Op, C extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<Add<Succ<A>, B>, C>, Add<Multiply<Succ<A>, C>, Multiply<B, C>>>; // (succ(a) + b)*c = succ(a)*c + b*c
+    right: ChainRewrites<[
+      addition.SumSucc1<A, B>,                                      // succ(a + b)*c = succ(a)*c + b*c
+      Mul_Add<Add<A, B>, C>,                                        // c + (a + b)*c = succ(a)*c + b*c
+      Mul_Add<A, C>,                                                // c + (a + b)*c = (c + a*c) + b*c
+      Distributivity<A, B, C>,                                      // c + (a*c + b*c) = (c + a*c) + b*c
+      addition.Associativity<C, Multiply<A, C>, Multiply<B, C>>,    // (c + a*c) + b*c = (c + a*c) + b*c
+      Refl<Add<C, Add<Multiply<A, C>, Multiply<B, C>>>>,            // true
+    ], this['left']>;
+  };
+  export namespace spec {
+    export type distributivity = [
+      assert<VerifyEquation<Dist_Base<'B', 'C'>>>,
+      assert<VerifyEquation<Dist_Inductive<'A', 'B', 'C'>>>,
+    ]
+  }
+
+  export type Associativity<A extends Op, B extends Op, C extends Op> =
+    Rewrite<Multiply<Multiply<A, B>, C>, Multiply<A, Multiply<B, C>>>;
+  export interface Assoc_Base<B extends Op, C extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<Multiply<_1, B>, C>, Multiply<_1, Multiply<B, C>>>; // (1*b)*c = 1*(b*c)
+    right: ChainRewrites<[
+      IdentityR<B>,                  // b*c = 1*(b*c)
+      IdentityR<Multiply<B, C>>,     // b*c = b*c
+      Refl<Multiply<B, C>>,          // true
+    ], this['left']>;
+  };
+  export interface Assoc_Inductive<A extends Op, B extends Op, C extends Op> {
+    type: 'rewrite',
+    left: Equation<Multiply<Multiply<Succ<A>, B>, C>, Multiply<Succ<A>, Multiply<B, C>>>; // (succ(a)*b)*c = succ(a)*(b*c)
+    right: ChainRewrites<[
+      Mul_Add<A, B>,                                                   // (b + a*b)*c = succ(a) * (b*c)
+      Distributivity<B, Multiply<A, B>, C>,                            // b*c + (a*b)*c = succ(a) * (b*c)
+      Mul_Add<A, Multiply<B, C>>,                                      // b*c + (a*b)*c = b*c + a*(b*c)
+      Associativity<A, B, C>,                                          // b*c + a*(b*c) = b*c + a*(b*c)
+      Refl<Add<Multiply<B, C>, Multiply<A, Multiply<B, C>>>>,          // true
+    ], this['left']>;
+  };
+  export namespace spec {
+    export type associativity = [
+      assert<VerifyEquation<Assoc_Base<'B', 'C'>>>,
+      assert<VerifyEquation<Assoc_Inductive<'A', 'B', 'C'>>>,
+    ]
+  }
 }
 
diff --git a/src/tests.ts b/src/tests.ts
index 5c066dc..04a009a 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,6 +1,6 @@
 import { addition, multiplication } from './index';
 import { Add, Multiply, Succ } from './nat';
-import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert } from './util';
+import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
 
 export type specChainRewrites = [
   assert<Eq<
@@ -70,4 +70,16 @@ export namespace multiplication_spec {
       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/util.ts b/src/util.ts
index 97e9335..88e3749 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -34,6 +34,8 @@ 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 Evaluate<Eq extends Rewrite<Op, Op>> = ApplyRewrite<Eq['left'], Eq>;
+
 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 });
 
-- 
cgit v1.3.1