aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/index.ts118
-rw-r--r--src/tests.ts28
-rw-r--r--src/util.ts2
3 files changed, 77 insertions, 71 deletions
diff --git a/src/index.ts b/src/index.ts
index 2b6f59a..7a3f717 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,59 +1,61 @@
import { Add, Multiply, Succ, _0, _1, _3 } from './nat';
-import { Op, Rewrite, ChainRewrites, Flip, Equation, Refl, VerifyEquation, assert } from './util';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert } from './util';
export namespace addition {
+ // Identity
export type Identity<A extends Op> = Rewrite<Add<A, _0>, A>;
export type IdentityR<A extends Op> = Rewrite<Add<_0, A>, A>;
- 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>>>
+ export type SumSucc<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>
+ export type SumSuccR<A extends Op, B extends Op> = Rewrite<Add<A, Succ<B>>, Succ<Add<A, B>>>
+ // Commutativity
export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
- export interface Comm_Base<B extends Op> {
+ export interface Comm_Base_Proof<B extends Op> {
type: 'rewrite',
left: Equation<Add<_0, B>, Add<B, _0>>; // 0 + b = b + 0
right: ChainRewrites<[
- IdentityR<B>, // b = b + 0
- Flip<Identity<B>>, // b + 0 = b + 0
- Refl<Add<B, _0>>, // true
+ IdentityR<B>, // b = b + 0
+ Sym<Identity<B>>, // b + 0 = b + 0
+ Refl<Add<B, _0>>, // true
], this['left']>;
};
- export interface Comm_Inductive<A extends Op, B extends Op> {
+ export interface Comm_Inductive_Proof<A extends Op, B extends Op> {
type: 'rewrite',
left: Equation<Add<Succ<A>, B>, Add<B, Succ<A>>>; // succ(a) + b = b + succ(a)
right: ChainRewrites<[
- SumSucc1<A, B>, // succ(a + b) = b + succ(a)
+ SumSucc<A, B>, // succ(a + b) = b + succ(a)
Commutativity<A, B>, // succ(b + a) = b + succ(a)
- SumSucc2<B, A>, // succ(b + a) = succ(b + a)
+ SumSuccR<B, A>, // succ(b + a) = succ(b + a)
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'>>>,
+ assert<VerifyEquation<Comm_Base_Proof<'B'>>>,
+ assert<VerifyEquation<Comm_Inductive_Proof<'A', 'B'>>>,
]
}
-
+ // 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> {
+ export interface Assoc_Base_Proof<B extends Op, C extends Op> {
type: 'rewrite',
- left: Equation<Add<Add<'0', B>, C>, Add<'0', Add<B, C>>>; // (0 + b) + c = 0 + (b + c)
+ left: Equation<Add<Add<_0, B>, C>, Add<_0, Add<B, C>>>; // (0 + b) + c = 0 + (b + c)
right: ChainRewrites<[
- Commutativity<'0', B>, // (b + 0) + c = 0 + (b + c)
+ Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c)
Identity<B>, // b + c = 0 + (b + c)
IdentityR<Add<B, C>>, // b + c = b + c
Refl<Add<B, C>>, // true
], this['left']>;
};
- export interface Assoc_Inductive<A extends Op, B extends Op, C extends Op> {
+ export interface Assoc_Inductive_Proof<A extends Op, B extends Op, C extends Op> {
type: 'rewrite',
left: Equation<Add<Add<Succ<A>, B>, C>, Add<Succ<A>, Add<B, C>>>; // (succ(a) + b) + c = succ(a) + (b + c)
right: ChainRewrites<[
- SumSucc1<A, B>, // succ(a + b) + c = succ(a) + (b + c)
- SumSucc1<A, Add<B, C>>, // succ(a + b) + c = succ(a + (b + c))
- SumSucc1<Add<A, B>, C>, // succ((a + b) + c) = succ(a + (b + c))
+ SumSucc<A, B>, // succ(a + b) + c = succ(a) + (b + c)
+ SumSucc<A, Add<B, C>>, // succ(a + b) + c = succ(a + (b + c))
+ SumSucc<Add<A, B>, C>, // succ((a + b) + c) = succ(a + (b + c))
Associativity<A, B, C>, // succ(a + (b + c)) = succ(a + (b + c))
Refl<Succ<Add<A, Add<B, C>>>>, // true
], this['left']>;
@@ -61,66 +63,69 @@ export namespace addition {
export namespace spec {
export type associativity = [
- assert<VerifyEquation<Assoc_Base<'A', 'B'>>>,
- assert<VerifyEquation<Assoc_Inductive<'A', 'B', 'C'>>>,
+ assert<VerifyEquation<Assoc_Base_Proof<'A', 'B'>>>,
+ assert<VerifyEquation<Assoc_Inductive_Proof<'A', 'B', 'C'>>>,
]
}
}
export namespace multiplication {
+ // Identity
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<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 MulSucc<A extends Op, B extends Op> = Rewrite<Multiply<Succ<A>, B>, Add<B, Multiply<A, B>>>;
+ export type MulSuccR<A extends Op, B extends Op> = Rewrite<Multiply<A, Succ<B>>, Add<A, Multiply<A, B>>>;
+ // Commutativity
export type Commutativity<A extends Op, B extends Op> = Rewrite<Multiply<A, B>, Multiply<B, A>>;
- export interface Comm_Base<B extends Op> {
+ export interface Comm_Base_Proof<B extends Op> {
type: 'rewrite',
left: Equation<Multiply<_1, B>, Multiply<B, _1>>; // 1 * b = b * 1
right: ChainRewrites<[
- IdentityR<B>, // b = b * 1
- Identity<B>, // b = b
- Refl<B>, // true
+ IdentityR<B>, // b = b * 1
+ Identity<B>, // b = b
+ Refl<B>, // true
], this['left']>;
};
- export interface Comm_Inductive<A extends Op, B extends Op> {
+ export interface Comm_Inductive_Proof<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>, // 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
+ MulSucc<A, B>, // b + a*b = b*succ(a)
+ MulSuccR<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'>>>,
+ assert<VerifyEquation<Comm_Base_Proof<'B'>>>,
+ assert<VerifyEquation<Comm_Inductive_Proof<'A', 'B'>>>,
]
}
+ // Distributivity
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> {
+ export interface Dist_Base_Proof<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
+ IdentityR<C>, // (1 + b)*c = c + b*c
+ addition.SumSucc<_0, B>, // succ(0 + b)*c = c + b*c
+ addition.IdentityR<B>, // succ(b)*c = c + b*c
+ MulSucc<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> {
+ export interface Dist_Inductive_Proof<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
+ addition.SumSucc<A, B>, // succ(a + b)*c = succ(a)*c + b*c
+ MulSucc<Add<A, B>, C>, // c + (a + b)*c = succ(a)*c + b*c
+ MulSucc<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
@@ -128,37 +133,38 @@ export namespace multiplication {
};
export namespace spec {
export type distributivity = [
- assert<VerifyEquation<Dist_Base<'B', 'C'>>>,
- assert<VerifyEquation<Dist_Inductive<'A', 'B', 'C'>>>,
+ assert<VerifyEquation<Dist_Base_Proof<'B', 'C'>>>,
+ assert<VerifyEquation<Dist_Inductive_Proof<'A', 'B', 'C'>>>,
]
}
+ // Associativity
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> {
+ export interface Assoc_Base_Proof<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
+ 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> {
+ export interface Assoc_Inductive_Proof<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)
+ MulSucc<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)
+ MulSucc<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'>>>,
+ assert<VerifyEquation<Assoc_Base_Proof<'B', 'C'>>>,
+ assert<VerifyEquation<Assoc_Inductive_Proof<'A', 'B', 'C'>>>,
]
}
}
diff --git a/src/tests.ts b/src/tests.ts
index 04a009a..7f331a6 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,48 +1,48 @@
import { addition, multiplication } from './index';
-import { Add, Multiply, Succ } from './nat';
-import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
+import { Add, Multiply, Succ, _0 } from './nat';
+import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
export type specChainRewrites = [
assert<Eq<
ChainRewrites<
[
- addition.Commutativity<'0', 'B'>,
+ addition.Commutativity<_0, 'B'>,
addition.Identity<'B'>,
],
- Add<Add<'0', 'B'>, 'C'>
+ Add<Add<_0, 'B'>, 'C'>
>,
Add<'B', 'C'>
>>,
assert<Eq<
ChainRewrites<
[
- addition.Commutativity<'0', 'B'>,
+ addition.Commutativity<_0, 'B'>,
addition.Identity<'B'>,
- Flip<addition.Identity<Add<'B', 'C'>>>,
- addition.Commutativity<Add<'B', 'C'>, '0'>,
+ Sym<addition.Identity<Add<'B', 'C'>>>,
+ addition.Commutativity<Add<'B', 'C'>, _0>,
],
- Add<Add<'0', 'B'>, 'C'>
+ Add<Add<_0, 'B'>, 'C'>
>,
- Add<'0', Add<'B', 'C'>>
+ Add<_0, Add<'B', 'C'>>
>>,
]
export namespace spec_addition {
export type specIdentity = [
assert<Eq<
- ApplyRewrite<Add<'A', Add<'B', '0'>>, addition.Identity<'B'>>,
+ 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'>>>,
+ 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'>
+ ApplyRewrite<Add<'A', 'B'>, Sym<addition.Identity<Add<'A', 'B'>>>>,
+ Add<Add<'A', 'B'>, _0>
>>,
assert<Eq<
- ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, addition.Identity<'C'>>,
+ ApplyRewrite<Add<'A', Add<'B', Add<'C', _0>>>, addition.Identity<'C'>>,
Add<'A', Add<'B', 'C'>>
>>,
]
diff --git a/src/util.ts b/src/util.ts
index 88e3749..1bed44b 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -6,7 +6,7 @@ export type Rewrite<left extends Op, right extends Op> = {
right: right;
};
-export type Flip<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>;
+export type Sym<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>;
export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
O extends R['left'] ? R['right']