aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/index.ts52
-rw-r--r--src/nat.ts1
-rw-r--r--src/tests.ts94
-rw-r--r--src/util.ts4
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 };