diff options
Diffstat (limited to '')
| -rw-r--r-- | package.json | 2 | ||||
| -rw-r--r-- | src/equation.ts | 51 | ||||
| -rw-r--r-- | src/natural-numbers.ts (renamed from src/index.ts) | 54 | ||||
| -rw-r--r-- | src/tests/nat.spec.ts (renamed from src/tests.ts) | 31 | ||||
| -rw-r--r-- | src/tests/theorem.spec.ts | 28 | ||||
| -rw-r--r-- | src/utils/nat.ts (renamed from src/nat.ts) | 2 | ||||
| -rw-r--r-- | src/utils/theorem.ts (renamed from src/util.ts) | 0 |
7 files changed, 86 insertions, 82 deletions
diff --git a/package.json b/package.json index 91f7ae3..7691cd2 100644 --- a/package.json +++ b/package.json @@ -7,7 +7,7 @@ "author": "Akshay Nair <phenax5@gmail.com>", "license": "MIT", "scripts": { - "test": "tsc --noEmit ./src/tests.ts" + "test": "tsc --noEmit" }, "dependencies": { "typescript": "^5.3.3" diff --git a/src/equation.ts b/src/equation.ts new file mode 100644 index 0000000..0ec25d6 --- /dev/null +++ b/src/equation.ts @@ -0,0 +1,51 @@ +import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem'; + +export namespace equation { + type F<X extends Op> = { op: 'F', a: 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 Equation<Op, 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/index.ts b/src/natural-numbers.ts index 4a00438..fa8a3ce 100644 --- a/src/index.ts +++ b/src/natural-numbers.ts @@ -1,5 +1,5 @@ -import { Add, Multiply, Succ, _0, _1, _3 } from './nat'; -import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './util'; +import { Add, Multiply, Succ, _0, _1, _3 } from './utils/nat'; +import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem'; export namespace addition { // Identity @@ -184,53 +184,3 @@ export namespace multiplication { ] } } - -export namespace equation { - type F<X extends Op> = { op: 'F', a: 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 Equation<Op, 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/tests.ts b/src/tests/nat.spec.ts index 7f331a6..acade6f 100644 --- a/src/tests.ts +++ b/src/tests/nat.spec.ts @@ -1,31 +1,6 @@ -import { addition, multiplication } from './index'; -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.Identity<'B'>, - ], - Add<Add<_0, 'B'>, 'C'> - >, - Add<'B', 'C'> - >>, - assert<Eq< - ChainRewrites< - [ - addition.Commutativity<_0, 'B'>, - addition.Identity<'B'>, - Sym<addition.Identity<Add<'B', 'C'>>>, - addition.Commutativity<Add<'B', 'C'>, _0>, - ], - Add<Add<_0, 'B'>, 'C'> - >, - Add<_0, Add<'B', 'C'>> - >>, -] +import { addition, multiplication } from '../natural-numbers'; +import { Add, Multiply, _0 } from '../utils/nat'; +import { ApplyRewrite, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem'; export namespace spec_addition { export type specIdentity = [ diff --git a/src/tests/theorem.spec.ts b/src/tests/theorem.spec.ts new file mode 100644 index 0000000..4ab220a --- /dev/null +++ b/src/tests/theorem.spec.ts @@ -0,0 +1,28 @@ +import { addition } from '../natural-numbers'; +import { Add, _0 } from '../utils/nat'; +import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem'; + +export type specChainRewrites = [ + assert<Eq< + ChainRewrites< + [ + addition.Commutativity<_0, 'B'>, + addition.Identity<'B'>, + ], + Add<Add<_0, 'B'>, 'C'> + >, + Add<'B', 'C'> + >>, + assert<Eq< + ChainRewrites< + [ + addition.Commutativity<_0, 'B'>, + addition.Identity<'B'>, + Sym<addition.Identity<Add<'B', 'C'>>>, + addition.Commutativity<Add<'B', 'C'>, _0>, + ], + Add<Add<_0, 'B'>, 'C'> + >, + Add<_0, Add<'B', 'C'>> + >>, +] diff --git a/src/nat.ts b/src/utils/nat.ts index 7491e82..af8f3da 100644 --- a/src/nat.ts +++ b/src/utils/nat.ts @@ -1,4 +1,4 @@ -import { Op } from './util'; +import { Op } from './theorem'; 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/utils/theorem.ts index a4dd2e9..a4dd2e9 100644 --- a/src/util.ts +++ b/src/utils/theorem.ts |