From 3d49bb583227b7669b638c4bb3e9853feae07ae2 Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Tue, 12 Dec 2023 23:44:14 +0530 Subject: refactor: refactorification --- src/index.ts | 118 +++++++++++++++++++++++++++++++---------------------------- src/tests.ts | 28 +++++++------- src/util.ts | 2 +- 3 files changed, 77 insertions(+), 71 deletions(-) (limited to 'src') 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 = Rewrite, A>; export type IdentityR = Rewrite, A>; - export type SumSucc1 = Rewrite, B>, Succ>> - export type SumSucc2 = Rewrite>, Succ>> + export type SumSucc = Rewrite, B>, Succ>> + export type SumSuccR = Rewrite>, Succ>> + // Commutativity export type Commutativity = Rewrite, Add>; - export interface Comm_Base { + export interface Comm_Base_Proof { type: 'rewrite', left: Equation, Add>; // 0 + b = b + 0 right: ChainRewrites<[ - IdentityR, // b = b + 0 - Flip>, // b + 0 = b + 0 - Refl>, // true + IdentityR, // b = b + 0 + Sym>, // b + 0 = b + 0 + Refl>, // true ], this['left']>; }; - export interface Comm_Inductive { + export interface Comm_Inductive_Proof { type: 'rewrite', left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) right: ChainRewrites<[ - SumSucc1, // succ(a + b) = b + succ(a) + SumSucc, // succ(a + b) = b + succ(a) Commutativity, // succ(b + a) = b + succ(a) - SumSucc2, // succ(b + a) = succ(b + a) + SumSuccR, // succ(b + a) = succ(b + a) Refl>>, // true ], this['left']>; }; export namespace spec { export type commutativity = [ - assert>>, - assert>>, + assert>>, + assert>>, ] } - + // Associativity export type Associativity = Rewrite, C>, Add>>; - export interface Assoc_Base { + export interface Assoc_Base_Proof { type: 'rewrite', - left: Equation, C>, Add<'0', Add>>; // (0 + b) + c = 0 + (b + c) + left: Equation, C>, Add<_0, Add>>; // (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 + c = 0 + (b + c) IdentityR>, // b + c = b + c Refl>, // true ], this['left']>; }; - export interface Assoc_Inductive { + export interface Assoc_Inductive_Proof { type: 'rewrite', left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) right: ChainRewrites<[ - SumSucc1, // succ(a + b) + c = succ(a) + (b + c) - SumSucc1>, // succ(a + b) + c = succ(a + (b + c)) - SumSucc1, C>, // succ((a + b) + c) = succ(a + (b + c)) + SumSucc, // succ(a + b) + c = succ(a) + (b + c) + SumSucc>, // succ(a + b) + c = succ(a + (b + c)) + SumSucc, C>, // succ((a + b) + c) = succ(a + (b + c)) Associativity, // succ(a + (b + c)) = succ(a + (b + c)) Refl>>>, // true ], this['left']>; @@ -61,66 +63,69 @@ export namespace addition { export namespace spec { export type associativity = [ - assert>>, - assert>>, + assert>>, + assert>>, ] } } export namespace multiplication { + // Identity export type Identity = Rewrite, A>; export type IdentityR = Rewrite, A>; - export type Mul_Add = Rewrite, B>, Add>>; - export type Mul_AddR = Rewrite>, Add>>; + export type MulSucc = Rewrite, B>, Add>>; + export type MulSuccR = Rewrite>, Add>>; + // Commutativity export type Commutativity = Rewrite, Multiply>; - export interface Comm_Base { + export interface Comm_Base_Proof { type: 'rewrite', left: Equation, Multiply>; // 1 * b = b * 1 right: ChainRewrites<[ - IdentityR, // b = b * 1 - Identity, // b = b - Refl, // true + IdentityR, // b = b * 1 + Identity, // b = b + Refl, // true ], this['left']>; }; - export interface Comm_Inductive { + export interface Comm_Inductive_Proof { type: 'rewrite', left: Equation, B>, Multiply>>; // succ(a)*b = b*succ(a) right: ChainRewrites<[ - Mul_Add, // b + a*b = b*succ(a) - Mul_AddR, // b + a*b = b + b*a - Commutativity, // b + a*b = b + a*b - Refl>>, // true + MulSucc, // b + a*b = b*succ(a) + MulSuccR, // b + a*b = b + b*a + Commutativity, // b + a*b = b + a*b + Refl>>, // true ], this['left']>; }; export namespace spec { export type commutativity = [ - assert>>, - assert>>, + assert>>, + assert>>, ] } + // Distributivity export type Distributivity = Rewrite, C>, Add, Multiply>>; - export interface Dist_Base { + export interface Dist_Base_Proof { type: 'rewrite', left: Equation, C>, Add, Multiply>>; // (1 + b)*c = 1*c + b*c right: ChainRewrites<[ - IdentityR, // (1 + b)*c = c + b*c - addition.SumSucc1<_0, B>, // succ(0 + b)*c = c + b*c - addition.IdentityR, // succ(b)*c = c + b*c - Mul_Add, // c + b*c = c + b*c - Refl>>, // true + IdentityR, // (1 + b)*c = c + b*c + addition.SumSucc<_0, B>, // succ(0 + b)*c = c + b*c + addition.IdentityR, // succ(b)*c = c + b*c + MulSucc, // c + b*c = c + b*c + Refl>>, // true ], this['left']>; }; - export interface Dist_Inductive { + export interface Dist_Inductive_Proof { type: 'rewrite', left: Equation, B>, C>, Add, C>, Multiply>>; // (succ(a) + b)*c = succ(a)*c + b*c right: ChainRewrites<[ - addition.SumSucc1, // succ(a + b)*c = succ(a)*c + b*c - Mul_Add, C>, // c + (a + b)*c = succ(a)*c + b*c - Mul_Add, // c + (a + b)*c = (c + a*c) + b*c + addition.SumSucc, // succ(a + b)*c = succ(a)*c + b*c + MulSucc, C>, // c + (a + b)*c = succ(a)*c + b*c + MulSucc, // c + (a + b)*c = (c + a*c) + b*c Distributivity, // c + (a*c + b*c) = (c + a*c) + b*c addition.Associativity, Multiply>, // (c + a*c) + b*c = (c + a*c) + b*c Refl, Multiply>>>, // true @@ -128,37 +133,38 @@ export namespace multiplication { }; export namespace spec { export type distributivity = [ - assert>>, - assert>>, + assert>>, + assert>>, ] } + // Associativity export type Associativity = Rewrite, C>, Multiply>>; - export interface Assoc_Base { + export interface Assoc_Base_Proof { type: 'rewrite', left: Equation, C>, Multiply<_1, Multiply>>; // (1*b)*c = 1*(b*c) right: ChainRewrites<[ - IdentityR, // b*c = 1*(b*c) - IdentityR>, // b*c = b*c - Refl>, // true + IdentityR, // b*c = 1*(b*c) + IdentityR>, // b*c = b*c + Refl>, // true ], this['left']>; }; - export interface Assoc_Inductive { + export interface Assoc_Inductive_Proof { type: 'rewrite', left: Equation, B>, C>, Multiply, Multiply>>; // (succ(a)*b)*c = succ(a)*(b*c) right: ChainRewrites<[ - Mul_Add, // (b + a*b)*c = succ(a) * (b*c) + MulSucc, // (b + a*b)*c = succ(a) * (b*c) Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) - Mul_Add>, // b*c + (a*b)*c = b*c + a*(b*c) + MulSucc>, // b*c + (a*b)*c = b*c + a*(b*c) Associativity, // b*c + a*(b*c) = b*c + a*(b*c) Refl, Multiply>>>, // true ], this['left']>; }; export namespace spec { export type associativity = [ - assert>>, - assert>>, + assert>>, + assert>>, ] } } 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, + addition.Commutativity<_0, 'B'>, addition.Identity<'B'>, ], - Add, 'C'> + Add, 'C'> >, Add<'B', 'C'> >>, assert, + addition.Commutativity<_0, 'B'>, addition.Identity<'B'>, - Flip>>, - addition.Commutativity, '0'>, + Sym>>, + addition.Commutativity, _0>, ], - Add, 'C'> + Add, 'C'> >, - Add<'0', Add<'B', 'C'>> + Add<_0, Add<'B', 'C'>> >>, ] export namespace spec_addition { export type specIdentity = [ assert>, addition.Identity<'B'>>, + ApplyRewrite>, addition.Identity<'B'>>, Add<'A', 'B'> >>, assert, '0'>, addition.Identity>>, + ApplyRewrite, _0>, addition.Identity>>, Add<'A', 'B'> >>, assert, Flip>>>, - Add, '0'> + ApplyRewrite, Sym>>>, + Add, _0> >>, assert>>, addition.Identity<'C'>>, + ApplyRewrite>>, 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 = { right: right; }; -export type Flip> = Rewrite; +export type Sym> = Rewrite; export type ApplyRewrite> = O extends R['left'] ? R['right'] -- cgit v1.3.1