9 files changed, 158 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..e5c664e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+node_modules
+*.log
+*.map
+dist/
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..ba5b8af
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2023 Akshay Nair
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..ee7b099
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+# Theorem prover in ts types
+Experiment to use typescript's type system for theorem proving
diff --git a/package.json b/package.json
new file mode 100644
index 0000000..a7d7598
--- /dev/null
+++ b/package.json
@@ -0,0 +1,15 @@
+{
+  "name": "brainfuck-ts-types",
+  "version": "0.0.0",
+  "description": "__",
+  "main": "index.js",
+  "repository": "__",
+  "author": "Akshay Nair <phenax5@gmail.com>",
+  "license": "MIT",
+  "scripts": {
+    "test": "tsc --noEmit ./src/tests.ts"
+  },
+  "dependencies": {
+    "typescript": "^5.3.3"
+  }
+}
diff --git a/src/index.ts b/src/index.ts
new file mode 100644
index 0000000..bd93300
--- /dev/null
+++ b/src/index.ts
@@ -0,0 +1,43 @@
+export type Op = string | { op: string; a: Op; b: Op };
+
+export type Rewrite<left extends Op, right extends Op> = {
+  type: 'rewrite';
+  left: left;
+  right: right;
+};
+export type RewriteKind = Rewrite<Op, Op>;
+
+export type Flip<R extends RewriteKind> = Rewrite<R['right'], R['left']>;
+
+export type ApplyRewrite<O extends Op, R extends RewriteKind> =
+  O extends R['left'] ? R['right']
+  : 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> }
+    : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
+  )
+  : never;
+
+export type Add<a extends Op, b extends Op> = { op: '+'; a: a; b: b };
+
+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>>;
+
+// type _x = ApplyRewrite<Add<'A', '1'>, Identity<'0'>>;
+
+// type Assoc<A extends Op, B extends Op> =
+
+/*
+
+Assoc: (a + b) + c = a + (b + c)
+
+For a = 0,
+(0 + b) + c
+= b + c
+= 0 + (b + c)
+
+For a = succ(),
+
+*/
+
diff --git a/src/nat.ts b/src/nat.ts
new file mode 100644
index 0000000..86bd318
--- /dev/null
+++ b/src/nat.ts
@@ -0,0 +1,16 @@
+declare const prev: unique symbol
+
+export type _nat = number & { [prev]: _nat | null }
+export type Succ<n extends _nat> = number & { [prev]: n }
+export type Pred<n extends _nat> = n extends _0 ? n : n[typeof prev]
+export type Nat = _0 | Succ<_nat>
+
+export type _0 = 0 & { [prev]: null }
+export type _1 = Succ<_0>
+export type _2 = Succ<_1>
+export type _3 = Succ<_2>
+export type _4 = Succ<_3>
+export type _5 = Succ<_4>
+export type _6 = Succ<_5>
+export type _7 = Succ<_6>
+export type _8 = Succ<_7>
diff --git a/src/tests.ts b/src/tests.ts
new file mode 100644
index 0000000..8c379e8
--- /dev/null
+++ b/src/tests.ts
@@ -0,0 +1,39 @@
+import { Add, ApplyRewrite, Commutativity, Flip, Identity } from './index';
+
+type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false) : 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'>>
+    >>,
+  ],
+  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'>>
+    >>,
+  ],
+};
diff --git a/tsconfig.json b/tsconfig.json
new file mode 100644
index 0000000..3ffa57b
--- /dev/null
+++ b/tsconfig.json
@@ -0,0 +1,10 @@
+{
+  "compilerOptions": {
+    "target": "es2016",
+    "module": "commonjs",
+    "esModuleInterop": true,
+    "forceConsistentCasingInFileNames": true,
+    "strict": true,
+    "skipLibCheck": true
+  }
+}
diff --git a/yarn.lock b/yarn.lock
new file mode 100644
index 0000000..cd07bce
--- /dev/null
+++ b/yarn.lock
@@ -0,0 +1,8 @@
+# THIS IS AN AUTOGENERATED FILE. DO NOT EDIT THIS FILE DIRECTLY.
+# yarn lockfile v1
+
+
+typescript@^5.3.3:
+  version "5.3.3"
+  resolved "https://registry.yarnpkg.com/typescript/-/typescript-5.3.3.tgz#b3ce6ba258e72e6305ba66f5c9b452aaee3ffe37"
+  integrity sha512-pXWcraxM0uxAS+tN0AG/BF2TyqmHO014Z070UsJ+pFvYuRSq8KH8DmWpnbXe0pEPDHXZV3FcAbJkijJ5oNEnWw==