aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/index.ts147
-rw-r--r--src/nat.ts2
-rw-r--r--src/util.ts60
3 files changed, 150 insertions, 59 deletions
diff --git a/src/index.ts b/src/index.ts
index 7a3f717..276bbe9 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,13 +1,13 @@
import { Add, Multiply, Succ, _0, _1, _3 } from './nat';
-import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert } from './util';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, RewriteBase, Subst, ApplyRewrite, Evaluate, ReflR, OpToStr } 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 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>>>
+ export type SuccLemma<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>
+ export type SuccLemmaR<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>>;
@@ -15,19 +15,19 @@ export namespace addition {
type: 'rewrite',
left: Equation<Add<_0, B>, Add<B, _0>>; // 0 + b = b + 0
right: ChainRewrites<[
- IdentityR<B>, // b = b + 0
- Sym<Identity<B>>, // b + 0 = b + 0
- Refl<Add<B, _0>>, // true
+ IdentityR<B>, // b = b + 0
+ Sym<Identity<B>>, // b + 0 = b + 0
+ Refl,
], this['left']>;
};
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<[
- SumSucc<A, B>, // succ(a + b) = b + succ(a)
- Commutativity<A, B>, // succ(b + a) = b + succ(a)
- SumSuccR<B, A>, // succ(b + a) = succ(b + a)
- Refl<Succ<Add<B, A>>>, // true
+ SuccLemma<A, B>, // succ(a + b) = b + succ(a)
+ Commutativity<A, B>, // succ(b + a) = b + succ(a)
+ SuccLemmaR<B, A>, // succ(b + a) = succ(b + a)
+ Refl,
], this['left']>;
};
export namespace spec {
@@ -43,21 +43,21 @@ export namespace addition {
type: 'rewrite',
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)
- Identity<B>, // b + c = 0 + (b + c)
- IdentityR<Add<B, C>>, // b + c = b + c
- Refl<Add<B, C>>, // true
+ 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,
], this['left']>;
};
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<[
- 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
+ SuccLemma<A, B>, // succ(a + b) + c = succ(a) + (b + c)
+ SuccLemma<A, Add<B, C>>, // succ(a + b) + c = succ(a + (b + c))
+ SuccLemma<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,
], this['left']>;
};
@@ -67,6 +67,22 @@ export namespace addition {
assert<VerifyEquation<Assoc_Inductive_Proof<'A', 'B', 'C'>>>,
]
}
+
+ // Rearrange
+ export interface Rearrange_Proof<A extends Op, B extends Op, C extends Op, D extends Op> {
+ type: 'rewrite',
+ left: Equation<Add<Add<A, B>, Add<C, D>>, Add<A, Add<Add<B, C>, D>>>; // (a + b) + (c + d) = a + ((b + c) + d)
+ right: ChainRewrites<[
+ Associativity<A, B, Add<C, D>>, // a + (b + (c + d)) = a + ((b + c) + d)
+ Associativity<B, C, D>, // a + (b + (c + d)) = a + (b + (c + d))
+ Refl,
+ ], this['left']>;
+ };
+ export namespace spec {
+ export type rearrange = [
+ assert<VerifyEquation<Rearrange_Proof<'A', 'B', 'C', 'D'>>>,
+ ]
+ }
}
export namespace multiplication {
@@ -74,8 +90,8 @@ 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 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>>>;
+ export type SuccLemma<A extends Op, B extends Op> = Rewrite<Multiply<Succ<A>, B>, Add<B, Multiply<A, B>>>;
+ export type SuccLemmaR<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>>;
@@ -85,17 +101,17 @@ export namespace multiplication {
right: ChainRewrites<[
IdentityR<B>, // b = b * 1
Identity<B>, // b = b
- Refl<B>, // true
+ Refl,
], this['left']>;
};
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<[
- 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
+ SuccLemma<A, B>, // b + a*b = b*succ(a)
+ SuccLemmaR<B, A>, // b + a*b = b + b*a
+ Commutativity<B, A>, // b + a*b = b + a*b
+ Refl,
], this['left']>;
};
export namespace spec {
@@ -112,23 +128,23 @@ export namespace multiplication {
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.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
+ IdentityR<C>, // (1 + b)*c = c + b*c
+ addition.SuccLemma<_0, B>, // succ(0 + b)*c = c + b*c
+ addition.IdentityR<B>, // succ(b)*c = c + b*c
+ SuccLemma<B, C>, // c + b*c = c + b*c
+ Refl,
], this['left']>;
};
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.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
+ addition.SuccLemma<A, B>, // succ(a + b)*c = succ(a)*c + b*c
+ SuccLemma<Add<A, B>, C>, // c + (a + b)*c = succ(a)*c + b*c
+ SuccLemma<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
+ Refl,
], this['left']>;
};
export namespace spec {
@@ -147,18 +163,18 @@ export namespace multiplication {
right: ChainRewrites<[
IdentityR<B>, // b*c = 1*(b*c)
IdentityR<Multiply<B, C>>, // b*c = b*c
- Refl<Multiply<B, C>>, // true
+ Refl,
], this['left']>;
};
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<[
- 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)
- 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
+ SuccLemma<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)
+ SuccLemma<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,
], this['left']>;
};
export namespace spec {
@@ -169,3 +185,52 @@ export namespace multiplication {
}
}
+export namespace equation {
+ type F<X extends Op> = { op: '<F>', a: _0, b: X };
+
+ export type Reflexivity<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
+
+ export type Symmetry<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<B, A>>;
+
+ export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>;
+
+ export type SubstituteEq<O extends { op: '=', a: Op, b: Op }> = Rewrite<O['a'], O['b']>
+ export interface SubstituteEq_Proof<A extends Op, B extends Op> {
+ type: 'rewrite',
+ known: {
+ 'a = b': Equation<A, B>,
+ },
+ left: Equation<F<A>, F<B>>; // f(a) = f(b)
+ right: ChainRewrites<[
+ Sym<Congruence<A, B>>, // a = b
+ SubstituteEq<this['known']['a = b']>, // b = b
+ Reflexivity<B>,
+ ], this['left']>;
+ };
+ export namespace spec {
+ export type substitution = [
+ assert<VerifyEquation<SubstituteEq_Proof<'A', 'B'>>>,
+ ]
+ }
+
+ export interface Transitivity_Proof<A extends Op, B extends Op, C extends Op> {
+ type: 'rewrite',
+ known: {
+ 'a = b': Equation<A, B>,
+ 'b = c': Equation<B, C>,
+ },
+ left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c)
+ right: ChainRewrites<[
+ SubstituteEq<this['known']['a = b']>, // (b = b) = (b = c)
+ SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>, // (b = b) = (c = b)
+ Reflexivity<B>, // true = (b = b)
+ Reflexivity<B>, // true = true
+ Reflexivity<'true'>,
+ ], this['left']>;
+ };
+ export namespace spec {
+ export type transitivity = [
+ assert<VerifyEquation<Transitivity_Proof<'A', 'B', 'C'>>>,
+ ]
+ }
+}
diff --git a/src/nat.ts b/src/nat.ts
index 5c52bdf..0017489 100644
--- a/src/nat.ts
+++ b/src/nat.ts
@@ -1,4 +1,4 @@
-import { Op } from "./util";
+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 };
diff --git a/src/util.ts b/src/util.ts
index 1bed44b..da6d637 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -1,15 +1,36 @@
-export type Op = string | { op: string; a: Op; b: Op };
+type COp = { op: string; a: Op; b: Op }
+export type Op = string | COp;
-export type Rewrite<left extends Op, right extends Op> = {
- type: 'rewrite';
+export type OpToStr<O extends Op> =
+ O extends string
+ ? O
+ : O extends { op: string, a: infer a extends string, b: infer b extends string } ? `(${a} ${O['op']} ${b})`
+ : O extends { op: string, a: infer a extends COp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})`
+ : O extends { op: string, a: infer a extends string, b: infer b extends COp } ? `(${a} ${O['op']} ${OpToStr<b>})`
+ : O extends { op: string, a: infer a extends COp, b: infer b extends COp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})`
+ : never;
+
+type RwType = 'rewrite' | 'imperative';
+
+export interface RewriteBase {
+ type: RwType;
+ left: Op;
+ right: Op;
+ assume?: Record<string, Op | RewriteBase>;
+}
+
+export interface Rewrite<left extends Op, right extends Op, Typ extends RwType = 'rewrite'> extends RewriteBase {
+ type: Typ;
left: left;
right: right;
};
-export type Sym<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>;
+export type Sym<R extends RewriteBase> = Rewrite<R['right'], R['left'], R['type']>;
+export type Subst<A extends Op, B extends Op> = Rewrite<A, B>
-export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
- O extends R['left'] ? R['right']
+export type ApplyRewrite<O extends Op, R extends RewriteBase> =
+ R['type'] extends 'imperative' ? (R & { left: O })['right']
+ : 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']
@@ -19,25 +40,30 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
)
: never;
-export interface Kind<V = unknown, R = unknown> {
- _: V;
- return: R;
-}
-export type Ap<K extends Kind, V> = (K & { _: V })['return'];
-
-export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> =
+export type ChainRewrites<Rws extends RewriteBase[], O extends Op> =
Rws extends [] ? O
- : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]]
+ : Rws extends [infer R extends RewriteBase, ...infer Rs extends RewriteBase[]]
? ChainRewrites<Rs, ApplyRewrite<O, R>>
: never;
-export type VerifyEquation<Eq extends Rewrite<Op, Op>> =
+export type VerifyEquation<Eq extends RewriteBase> =
Eq['right'] extends 'true' ? true : false & Eq['right'];
-export type Evaluate<Eq extends Rewrite<Op, Op>> = ApplyRewrite<Eq['left'], Eq>;
+export type Evaluate<Eq extends RewriteBase> = ApplyRewrite<Eq['left'], Eq>;
export type assert<T extends true> = T;
+export type assertFalse<T extends false> = 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 };
-export type Refl<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
+
+export interface Refl extends RewriteBase {
+ type: 'imperative';
+ left: Op;
+ right: this['left'] extends { op: '=', a: infer a, b: infer b }
+ ? (Eq<a, b> extends true ? 'true' : this['left'])
+ : this['left'];
+};
+
+// Like Refl, but you have to specify the sides of the equation and this one works recursively
+export type ReflR<A extends Op> = Rewrite<Equation<A, A>, 'true'>;