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
|
# Theorem prover in ts types
Experiment to use typescript's type system to make a shitty theorem prover.
### Commutativity of addition in ts types or something?
```typescript
export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
export interface Comm_Base_Proof<B extends Op> {
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
Refl<Add<B, _0>>, // true
], this['left']>;
};
export interface Comm_Inductive_Proof<A extends Op, B extends Op> {
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)
Refl<Succ<Add<B, A>>>, // true
], this['left']>;
};
export namespace spec {
export type commutativity = [
assert<VerifyEquation<Comm_Base_Proof<'B'>>>,
assert<VerifyEquation<Comm_Inductive_Proof<'A', 'B'>>>,
]
}
```
|
