From 60331b72ab37e581b0fb405c2eff862e16b52ac2 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Sun, 10 Dec 2023 19:24:31 +0530
Subject: cheated for associativity for a=n

---
 src/index.ts |  39 +++++++++++++---
 src/tests.ts | 148 +++++++++++++++++++++++++++++++----------------------------
 2 files changed, 110 insertions(+), 77 deletions(-)

diff --git a/src/index.ts b/src/index.ts
index 5164412..575c446 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,21 +1,41 @@
 import { Op, Rewrite, ChainRewrites, Flip } from './util';
 
 export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B };
+export type Succ<A extends Op> = Add<'1', A>;
 
 export type Identity<A extends Op> = Rewrite<Add<A, '0'>, A>;
 export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
 
 export interface Assoc0<A extends Op, B extends Op> {
   type: 'rewrite',
-  left: Add<Add<'0', A>, B>;
+  left: Add<Add<'0', A>, B>; // (0 + a) + b
   right: ChainRewrites<[
-    Commutativity<'0', A>,
-    Identity<A>,
-    Flip<Identity<Add<A, B>>>,
-    Commutativity<Add<A, B>, '0'>,
+    Commutativity<'0', A>, // = (a + 0) + b
+    Identity<A>, // = a + b
+    Flip<Identity<Add<A, B>>>, // = (a + b) + 0
+    Commutativity<Add<A, B>, '0'>, // = 0 + (a + b)
   ], this['left']>;
 };
 
+export type Assoc1<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>;
+
+export interface Assoc<A extends Op, B extends Op, C extends Op> {
+  type: 'rewrite',
+  left: Add<Add<A, B>, C>; // (a + b) + c
+  right: ChainRewrites<[
+    Rewrite<A, Succ<A>>, // = CHEATING
+    Assoc1<A, B>, // = succ(a + b) + c
+    Assoc1<Add<A, B>, C>, // = succ(a + b + c)
+    Rewrite<A, '0'>, // CHEATING. TODO: figure out recursion
+    Assoc0<B, C>,  // Induction base case
+    Rewrite<'0', A>, // CHEATING
+    Flip<Assoc1<A, Add<B, C>>>, // = succ(a) + (b + c)
+    Rewrite<Succ<A>, A>, // = CHEATING
+  ], this['left']>;
+};
+
+// type _x = ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, AssocN<'A', 'B', 'C'>>
+
 /*
 Assoc: (a + b) + c = a + (b + c)
 
@@ -26,7 +46,12 @@ For a = 0,
 = (b + c) + 0 -- flip id
 = 0 + (b + c) -- comm
 
-For a = succ(),
-
+For a' = succ(a),
+(succ(a) + b) + c
+= succ(a + b) + c
+= succ((a + b) + c)
+----- rec
+= succ(a + (b + c))
+= succ(a) + (b + c)
 */
 
diff --git a/src/tests.ts b/src/tests.ts
index b4fc214..d56cb30 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,77 +1,85 @@
-import { Add, Assoc0, Commutativity, Identity } from './index';
-import { ApplyRewrite, ChainRewrites, Flip } from './util';
+import { Add, Assoc, Assoc0, Assoc1, Commutativity, Identity, Succ } from './index';
+import { ApplyRewrite, ChainRewrites, Flip, Rewrite } 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 _testCases = {
-  Identity: [
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>,
-      Add<'A', 'B'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>,
-      Add<'A', 'B'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>,
-      Add<Add<'A', 'B'>, '0'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>,
-      Add<'A', Add<'B', 'C'>>
-    >>,
-  ],
+export type specIdentity = [
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>,
+    Add<'A', 'B'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>,
+    Add<'A', 'B'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>,
+    Add<Add<'A', 'B'>, '0'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>,
+    Add<'A', Add<'B', 'C'>>
+  >>,
+]
+
+export type specCommutativity = [
+  assert<Eq<
+    ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>,
+    Add<'B', 'A'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>,
+    Add<Add<'B', 'A'>, 'C'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>,
+    Add<'A', Add<'C', 'B'>>
+  >>,
+]
+
+export type specChainRewrites = [
+  assert<Eq<
+    ChainRewrites<
+      [
+        Commutativity<'0', 'B'>,
+        Identity<'B'>,
+      ],
+      Add<Add<'0', 'B'>, 'C'>
+    >,
+    Add<'B', 'C'>
+  >>,
+  assert<Eq<
+    ChainRewrites<
+      [
+        Commutativity<'0', 'B'>,
+        Identity<'B'>,
+        Flip<Identity<Add<'B', 'C'>>>,
+        Commutativity<Add<'B', 'C'>, '0'>,
+      ],
+      Add<Add<'0', 'B'>, 'C'>
+    >,
+    Add<'0', Add<'B', 'C'>>
+  >>,
+]
+
+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'>>
+  >>,
+]
 
-  Commutativity: [
-    assert<Eq<
-      ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>,
-      Add<'B', 'A'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>,
-      Add<Add<'B', 'A'>, 'C'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>,
-      Add<'A', Add<'C', 'B'>>
-    >>,
-  ],
 
-  ChainRewrites: [
-    assert<Eq<
-      ChainRewrites<
-        [
-          Commutativity<'0', 'B'>,
-          Identity<'B'>,
-        ],
-        Add<Add<'0', 'B'>, 'C'>
-      >,
-      Add<'B', 'C'>
-    >>,
-    assert<Eq<
-      ChainRewrites<
-        [
-          Commutativity<'0', 'B'>,
-          Identity<'B'>,
-          Flip<Identity<Add<'B', 'C'>>>,
-          Commutativity<Add<'B', 'C'>, '0'>,
-        ],
-        Add<Add<'0', 'B'>, 'C'>
-      >,
-      Add<'0', Add<'B', 'C'>>
-    >>,
-  ],
 
-  Assoc0: [
-    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'>>
-    >>,
-  ],
-};
-- 
cgit v1.3.1