feat: equation proofs (substitution + transitivity)

3 files changed, 111 insertions, 33 deletions

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<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,8 +15,8 @@ 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
+      IdentityR<B>,           // b = b + 0
+      Sym<Identity<B>>,       // b + 0 = b + 0
       Refl,
     ], this['left']>;
   };
@@ -24,9 +24,9 @@ export namespace addition {
     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)
+      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']>;
   };
@@ -43,9 +43,9 @@ 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
+      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']>;
   };
@@ -53,10 +53,10 @@ export namespace addition {
     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))
+      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>>;
@@ -92,9 +108,9 @@ export namespace multiplication {
     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
+      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']>;
   };
@@ -112,10 +128,10 @@ 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
+      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']>;
   };
@@ -123,9 +139,9 @@ export namespace multiplication {
     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,
@@ -154,10 +170,10 @@ export namespace multiplication {
     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)
+      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']>;
   };
@@ -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 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 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';
 
@@ -6,6 +16,7 @@ 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 {
@@ -15,6 +26,7 @@ export interface Rewrite<left extends Op, right extends Op, Typ extends RwType =
 };
 
 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 RewriteBase> =
   R['type'] extends 'imperative' ? (R & { left: O })['right']
@@ -40,6 +52,7 @@ export type VerifyEquation<Eq extends RewriteBase> =
 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 };