From 6f31fc62f9a6ee77d71c5f5fe352e027f495ae9a Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Fri, 15 Dec 2023 22:06:30 +0530 Subject: feat: equation proofs (substitution + transitivity) --- src/index.ts | 127 ++++++++++++++++++++++++++++++++++++++++++++--------------- src/nat.ts | 2 +- src/util.ts | 15 ++++++- 3 files changed, 111 insertions(+), 33 deletions(-) (limited to 'src') diff --git a/src/index.ts b/src/index.ts index 75e97be..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 = Rewrite, A>; export type IdentityR = Rewrite, A>; - export type SumSucc = Rewrite, B>, Succ>> - export type SumSuccR = Rewrite>, Succ>> + export type SuccLemma = Rewrite, B>, Succ>> + export type SuccLemmaR = Rewrite>, Succ>> // Commutativity export type Commutativity = Rewrite, Add>; @@ -15,8 +15,8 @@ export namespace addition { type: 'rewrite', left: Equation, Add>; // 0 + b = b + 0 right: ChainRewrites<[ - IdentityR, // b = b + 0 - Sym>, // b + 0 = b + 0 + IdentityR, // b = b + 0 + Sym>, // b + 0 = b + 0 Refl, ], this['left']>; }; @@ -24,9 +24,9 @@ export namespace addition { type: 'rewrite', left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) right: ChainRewrites<[ - SumSucc, // succ(a + b) = b + succ(a) - Commutativity, // succ(b + a) = b + succ(a) - SumSuccR, // succ(b + a) = succ(b + a) + SuccLemma, // succ(a + b) = b + succ(a) + Commutativity, // succ(b + a) = b + succ(a) + SuccLemmaR, // succ(b + a) = succ(b + a) Refl, ], this['left']>; }; @@ -43,9 +43,9 @@ export namespace addition { 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 + Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c) + Identity, // b + c = 0 + (b + c) + IdentityR>, // b + c = b + c Refl, ], this['left']>; }; @@ -53,10 +53,10 @@ export namespace addition { type: 'rewrite', left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) right: ChainRewrites<[ - 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)) + 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']>; }; @@ -67,6 +67,22 @@ export namespace addition { 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 { @@ -74,8 +90,8 @@ export namespace multiplication { export type Identity = Rewrite, A>; export type IdentityR = Rewrite, A>; - export type MulSucc = Rewrite, B>, Add>>; - export type MulSuccR = Rewrite>, Add>>; + export type SuccLemma = Rewrite, B>, Add>>; + export type SuccLemmaR = Rewrite>, Add>>; // Commutativity export type Commutativity = Rewrite, Multiply>; @@ -92,9 +108,9 @@ export namespace multiplication { type: 'rewrite', left: Equation, B>, Multiply>>; // succ(a)*b = b*succ(a) right: ChainRewrites<[ - MulSucc, // b + a*b = b*succ(a) - MulSuccR, // b + a*b = b + b*a - Commutativity, // b + a*b = b + a*b + SuccLemma, // b + a*b = b*succ(a) + SuccLemmaR, // b + a*b = b + b*a + Commutativity, // b + a*b = b + a*b Refl, ], this['left']>; }; @@ -112,10 +128,10 @@ export namespace multiplication { type: 'rewrite', left: Equation, C>, Add, Multiply>>; // (1 + b)*c = 1*c + b*c right: ChainRewrites<[ - 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 + 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']>; }; @@ -123,9 +139,9 @@ export namespace multiplication { type: 'rewrite', left: Equation, B>, C>, Add, C>, Multiply>>; // (succ(a) + b)*c = succ(a)*c + b*c right: ChainRewrites<[ - 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 + 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, @@ -154,10 +170,10 @@ export namespace multiplication { type: 'rewrite', left: Equation, B>, C>, Multiply, Multiply>>; // (succ(a)*b)*c = succ(a)*(b*c) right: ChainRewrites<[ - MulSucc, // (b + a*b)*c = succ(a) * (b*c) - Distributivity, C>, // b*c + (a*b)*c = succ(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) + 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']>; }; @@ -169,3 +185,52 @@ export namespace multiplication { } } +export namespace equation { + type F = { op: '', a: _0, b: X }; + + export type Reflexivity = Rewrite, 'true'>; + + export type Symmetry = Rewrite, Equation>; + + export type Congruence = Rewrite, Equation, F>>; + + export type SubstituteEq + export interface SubstituteEq_Proof { + type: 'rewrite', + known: { + 'a = b': Equation, + }, + left: Equation, F>; // f(a) = f(b) + right: ChainRewrites<[ + Sym>, // a = b + SubstituteEq, // b = b + Reflexivity, + ], this['left']>; + }; + export namespace spec { + export type substitution = [ + assert>>, + ] + } + + export interface Transitivity_Proof { + type: 'rewrite', + known: { + 'a = b': Equation, + 'b = c': Equation, + }, + left: Equation, Equation>; // (a = b) = (b = c) + right: ChainRewrites<[ + SubstituteEq, // (b = b) = (b = c) + SubstituteEq>>, // (b = b) = (c = b) + Reflexivity, // true = (b = b) + Reflexivity, // true = true + Reflexivity<'true'>, + ], this['left']>; + }; + export namespace spec { + export type transitivity = [ + assert>>, + ] + } +} 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 = { op: '+'; a: A; b: B }; export type Multiply = { op: '*'; a: A; b: B }; diff --git a/src/util.ts b/src/util.ts index c78c12c..da6d637 100644 --- a/src/util.ts +++ b/src/util.ts @@ -1,4 +1,14 @@ -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 OpToStr = + 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} ${O['op']} ${b})` + : O extends { op: string, a: infer a extends string, b: infer b extends COp } ? `(${a} ${O['op']} ${OpToStr})` + : O extends { op: string, a: infer a extends COp, b: infer b extends COp } ? `(${OpToStr} ${O['op']} ${OpToStr})` + : never; type RwType = 'rewrite' | 'imperative'; @@ -6,6 +16,7 @@ export interface RewriteBase { type: RwType; left: Op; right: Op; + assume?: Record; } export interface Rewrite extends RewriteBase { @@ -15,6 +26,7 @@ export interface Rewrite = Rewrite; +export type Subst = Rewrite export type ApplyRewrite = R['type'] extends 'imperative' ? (R & { left: O })['right'] @@ -40,6 +52,7 @@ export type VerifyEquation = export type Evaluate = ApplyRewrite; export type assert = T; +export type assertFalse = T; export type Eq = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); export type Equation = { op: '=', a: A, b: B }; -- cgit v1.3.1