From efc0358c1e2b52308d3df68aa713cef5dc6e6bfe Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Fri, 15 Dec 2023 22:36:03 +0530 Subject: refactor: moves stuff around --- src/natural-numbers.ts | 186 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 186 insertions(+) create mode 100644 src/natural-numbers.ts (limited to 'src/natural-numbers.ts') diff --git a/src/natural-numbers.ts b/src/natural-numbers.ts new file mode 100644 index 0000000..fa8a3ce --- /dev/null +++ b/src/natural-numbers.ts @@ -0,0 +1,186 @@ +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 + export type Identity = Rewrite, A>; + export type IdentityR = Rewrite, A>; + + export type SuccLemma = Rewrite, B>, Succ>> + export type SuccLemmaR = Rewrite>, Succ>> + + // Commutativity + export type Commutativity = Rewrite, Add>; + export interface Comm_Base_Proof { + type: 'rewrite', + left: Equation, Add>; // 0 + b = b + 0 + right: ChainRewrites<[ + IdentityR, // b = b + 0 + Sym>, // b + 0 = b + 0 + Refl, + ], this['left']>; + }; + export interface Comm_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) + right: ChainRewrites<[ + SuccLemma, // succ(a + b) = b + succ(a) + Commutativity, // succ(b + a) = b + succ(a) + SuccLemmaR, // succ(b + a) = succ(b + a) + Refl, + ], this['left']>; + }; + export namespace spec { + export type commutativity = [ + assert>>, + assert>>, + ] + } + + // Associativity + export type Associativity = Rewrite, C>, Add>>; + export interface Assoc_Base_Proof { + type: 'rewrite', + left: Equation, C>, Add<_0, Add>>; // (0 + b) + c = 0 + (b + c) + right: ChainRewrites<[ + Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c) + Identity, // b + c = 0 + (b + c) + IdentityR>, // b + c = b + c + Refl, + ], this['left']>; + }; + export interface Assoc_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) + right: ChainRewrites<[ + SuccLemma, // succ(a + b) + c = succ(a) + (b + c) + SuccLemma>, // succ(a + b) + c = succ(a + (b + c)) + SuccLemma, C>, // succ((a + b) + c) = succ(a + (b + c)) + Associativity, // succ(a + (b + c)) = succ(a + (b + c)) + Refl, + ], this['left']>; + }; + + export namespace spec { + export type associativity = [ + assert>>, + assert>>, + ] + } + + // Rearrange + export interface Rearrange_Proof { + type: 'rewrite', + left: Equation, Add>, Add, D>>>; // (a + b) + (c + d) = a + ((b + c) + d) + right: ChainRewrites<[ + Associativity>, // a + (b + (c + d)) = a + ((b + c) + d) + Associativity, // a + (b + (c + d)) = a + (b + (c + d)) + Refl, + ], this['left']>; + }; + export namespace spec { + export type rearrange = [ + assert>>, + ] + } +} + +export namespace multiplication { + // Identity + export type Identity = Rewrite, A>; + export type IdentityR = Rewrite, A>; + + export type SuccLemma = Rewrite, B>, Add>>; + export type SuccLemmaR = Rewrite>, Add>>; + + // Commutativity + export type Commutativity = Rewrite, Multiply>; + export interface Comm_Base_Proof { + type: 'rewrite', + left: Equation, Multiply>; // 1 * b = b * 1 + right: ChainRewrites<[ + IdentityR, // b = b * 1 + Identity, // b = b + Refl, + ], this['left']>; + }; + export interface Comm_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, Multiply>>; // succ(a)*b = b*succ(a) + right: ChainRewrites<[ + SuccLemma, // b + a*b = b*succ(a) + SuccLemmaR, // b + a*b = b + b*a + Commutativity, // b + a*b = b + a*b + Refl, + ], this['left']>; + }; + export namespace spec { + export type commutativity = [ + assert>>, + assert>>, + ] + } + + // Distributivity + export type Distributivity = + Rewrite, C>, Add, Multiply>>; + 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.SuccLemma<_0, B>, // succ(0 + b)*c = c + b*c + addition.IdentityR, // succ(b)*c = c + b*c + SuccLemma, // c + b*c = c + b*c + Refl, + ], this['left']>; + }; + 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.SuccLemma, // succ(a + b)*c = succ(a)*c + b*c + SuccLemma, C>, // c + (a + b)*c = succ(a)*c + b*c + SuccLemma, // 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, + ], this['left']>; + }; + export namespace spec { + export type distributivity = [ + assert>>, + assert>>, + ] + } + + // Associativity + export type Associativity = + Rewrite, C>, Multiply>>; + 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, + ], this['left']>; + }; + export interface Assoc_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, C>, Multiply, Multiply>>; // (succ(a)*b)*c = succ(a)*(b*c) + right: ChainRewrites<[ + SuccLemma, // (b + a*b)*c = succ(a) * (b*c) + Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) + SuccLemma>, // b*c + (a*b)*c = b*c + a*(b*c) + Associativity, // b*c + a*(b*c) = b*c + a*(b*c) + Refl, + ], this['left']>; + }; + export namespace spec { + export type associativity = [ + assert>>, + assert>>, + ] + } +} -- cgit v1.3.1