1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr, SubstEq } from './utils/theorem';
export type Abs<x extends Op, o extends Op> = { op: '->', a: x, b: o }; // \x. o
export type Ap<F extends Op, x extends Op> = { op: '$', a: F, b: x }; // F(x)
export type Comp<F extends Op, G extends Op> = { op: '.', a: F, b: G }; // F . G
export type Id<x extends Op = 'x'> = Abs<x, x> // \x. x
export type Const<x extends Op = 'x', y extends Op = 'y'> = Abs<x, Abs<y, x>> // \x. \y. x
export type Inv<F extends Op> = { op: 'inv', a: F }
export namespace composition {
export type Abstraction<x extends Op, y extends Op, v extends Op> = Rewrite<Ap<Abs<x, y>, v>, y>;
export type Composition<F extends Op, G extends Op, x extends Op> = Rewrite<Ap<Comp<F, G>, x>, Ap<F, Ap<G, x>>>;
// Identity
export type Identity<x extends Op> = Rewrite<Ap<Id, x>, x>;
export namespace proof {
export interface Identity_Proof<x extends Op> {
type: 'rewrite';
left: Equation<Ap<Id<x>, x>, x>; // id(x) = x
right: ChainRewrites<[
Abstraction<x, x, x>, // x = x
Refl,
], this['left']>;
}
export interface Identity_Composition_Proof<F extends Op, x extends Op> {
type: 'rewrite';
left: Equation<Ap<Comp<F, Id>, x>, Ap<F, x>>; // (f . id)(x) = f(x)
right: ChainRewrites<[
Composition<F, Id, x>, // f(id(x)) = f(x)
Identity<x>, // f(x) = f(x)
Refl,
], this['left']>;
}
export type identity = [
assert<VerifyEquation<Identity_Proof<'x'>>>,
assert<VerifyEquation<Identity_Composition_Proof<'F', 'x'>>>,
]
}
// Associativity
export type Associativity<F extends Op, G extends Op, H extends Op> = Rewrite<
Comp<Comp<F, G>, H>,
Comp<F, Comp<G, H>>
>
export namespace proof {
export interface Assoc_Proof<F extends Op, G extends Op, H extends Op, x extends Op> {
type: 'rewrite';
left: Equation<Ap<Comp<Comp<F, G>, H>, x>, Ap<Comp<F, Comp<G, H>>, x>>; // ((f . g) . h)(x) = (f . (g . h))(x)
right: ChainRewrites<[
Composition<Comp<F, G>, H, x>, // (f . g)(h(x)) = (f . (g . h))(x)
Composition<F, G, Ap<H, x>>, // f(g(h(x))) = (f . (g . h))(x)
Composition<F, Comp<G, H>, x>, // f(g(h(x))) = f((g . h)(x))
Composition<G, H, x>, // f(g(h(x))) = f(g(h(x)))
Refl,
], this['left']>;
}
export type associativity = [
assert<VerifyEquation<Assoc_Proof<'F', 'G', 'H', 'x'>>>,
]
}
// Identity
export type Transitivity<x extends Op, y extends Op, z extends Op> = Rewrite<Comp<Abs<y, z>, Abs<x, y>>, Abs<x, z>>;
export namespace proof {
export interface Transitivity_Proof<x extends Op, y extends Op, z extends Op> {
type: 'rewrite';
left: Equation<Ap<Comp<Abs<y, z>, Abs<x, y>>, x>, Ap<Abs<x, z>, x>>; // ((\y -> z) . (\x -> y))(x) = (\x -> z)(x)
right: ChainRewrites<[
Composition<Abs<y, z>, Abs<x, y>, x>, // (\y -> z) $ (\x -> y)(x) = (\x -> z)(x)
Abstraction<x, y, x>, // (\y -> z) $ y = (\x -> z)(x)
Abstraction<y, z, y>, // z = (\x -> z)(x)
Abstraction<x, z, x>, // z = z
Refl,
], this['left']>;
}
export type transitivity = [
// OpToStr<Evaluate<Transitivity_Proof<'x', 'y', 'z'>>>,
assert<VerifyEquation<Transitivity_Proof<'x', 'y', 'z'>>>,
]
}
// Inverse functions
export type Inverse<x extends Op, y extends Op> = Rewrite<Inv<Abs<x, y>>, Abs<y, x>>;
export namespace proof {
export interface Composition_Inverse_Proof<F extends Op, G extends Op> {
type: 'rewrite',
known: {
'f': Equation<F, Abs<'y', 'z'>>,
'g': Equation<G, Abs<'x', 'y'>>,
},
left: Equation<Inv<Comp<F, G>>, Comp<Inv<G>, Inv<F>>>, // inv(f . g) = inv(g) . inv(f)
right: ChainRewrites<[
SubstEq<this['known']['f']>,
SubstEq<this['known']['f']>, // inv((\y -> z) . g) = inv(g) . inv(\y -> z)
SubstEq<this['known']['g']>,
SubstEq<this['known']['g']>, // inv((\y -> z) . (\x -> y)) = inv(\x -> y) . inv(\y -> z)
Inverse<'x', 'y'>,
Inverse<'y', 'z'>, // inv((\x -> y) . (\y -> z)) = (\z -> y) . (\y -> x)
Transitivity<'x', 'y', 'z'>, // inv(\x -> z) = (\z -> y) . (\y -> x)
Transitivity<'z', 'y', 'x'>, // inv(\x -> z) = \z -> x
Inverse<'x', 'z'>, // \z -> x = \z -> x
Refl
], this['left']>,
}
export type inverse = [
// OpToStr<Evaluate<Composition_Inverse_Proof<'F', 'G'>>>,
assert<VerifyEquation<Composition_Inverse_Proof<'F', 'G'>>>,
]
}
}
|
