TypeScript as a proof assistant

proofscript.ts

// TypeScript can be used just like a proof assistant (for intuitionistic propositional logic)!
//
// Inspired by: https://www.youtube.com/watch?v=i-hRpYiNwBw

// We can encode False as the following recursive type, which can never
// be constructed (e.g. you would need { false: { false: { false: ... }}}).
type False = { false: False };

// True can be encoded as the inhabited singleton type "I", which
// has as its only inhabitant the string "I".
type True = "I";

// A conjunction of A and B can be encoded as an object containing
// the property "left" with A and "right" with B.
type Con<A, B> = { left: A, right: B };

// A disjunction of A and B is the union type of two objects, one
// containing the field "left" with A, and the other containing
// the field "right" with B.
type Dis<A, B> = { left: A } | { right: B };

// Implication is just a function.
type Imp<A, B> = (_: A) => B;

// Bi-implication is the conjunction of the implication in
// both directions.
type Iff<A, B> = Con<Imp<A, B>, Imp<B, A>>;

// A negation is an implication to an unhabited type.
type Not<A> = Imp<A, False>;

// We define the principle of explosion as an axiom.
function contradiction<A>(): Imp<False, A> {
    return (_ : False) => "true" as any as A;
}

<A, B, C>() => {

// We can now prove some basic rules of intuitionistic logic!

// B
// ------
// A -> B
type ImpI = Imp<B, Imp<A, B>>;
const proof_imp_I : ImpI =
    (b : B) =>
    (_: A) => b;

// A    A -> B
// -----------
// B
type ImpE = Imp<A, Imp<Imp<A, B>, B>>;
const proof_imp_E : ImpE =
    (a : A) =>
    (a_imp_b : Imp<A, B>) =>
    a_imp_b(a)

// A    B
// ------
// A /\ B
type ConjI = Imp<A, Imp<B, Con<A, B>>>;
const proof_conj_I : ConjI = 
    (a : A) =>
    (b : B) =>
    ({ left: a, right: b });

// A /\ B
// ------
// A
type ConjEl = Imp<Con<A, B>, A>;
const proof_conj_El : ConjEl =
    (a_and_b : Con<A, B>) =>
    a_and_b.left;

// A /\ B
// ------
// B
type ConjEr = Imp<Con<A, B>, B>;
const proof_conj_Er : ConjEr =
    (a_and_b : Con<A, B>) =>
    a_and_b.right;

// A
// ------
// A \/ B
type DisjIl = Imp<A, Dis<A, B>>;
const proof_disj_Il : DisjIl =
    (a: A) =>
    ({ left: a });

// B
// ------
// A \/ B
type DisjIr = Imp<B, Dis<A, B>>;
const proof_disj_Ir : DisjIr =
    (b: B) => 
    ({ right: b });

// A \/ B    (A -> C)    (B -> C)
// ------------------------------
// C
type DisjE = Imp<Dis<A, B>, Imp<Imp<A, C>, Imp<Imp<B, C>, C>>>;
const proof_disj_E : DisjE =
    (a_or_b : Dis<A, B>) =>
    (a_imp_c : Imp<A, C>) =>
    (b_imp_c : Imp<B, C>) =>
    "left" in a_or_b ?
        a_imp_c(a_or_b.left) :
        b_imp_c(a_or_b.right);

// We can also show some more interesting tautologies!

// (A -> B -> C) -> (A -> B) -> A -> C
type Tauto1 = Imp<Imp<A, Imp<B, C>>, Imp<Imp<A, B>, Imp<A, C>>>;
const proof_tauto1 : Tauto1 =
    (a_imp_b_imp_c : Imp<A, Imp<B, C>>) =>
    (a_imp_b : Imp<A, B>) =>
    (a : A) =>
    a_imp_b_imp_c(a)(a_imp_b(a));

// A -> A -> A
type Tauto2 = Imp<A, Imp<A, A>>;
const proof_tauto2_1 : Tauto2 =
    (a : A) =>
    (_ : A) =>
    a;
const proof_tauto2_2 : Tauto2 =
    (_ : A) =>
    (a : A) =>
    a;

// We can even use negations.

// (A -> B) -> (~B -> ~A)
type Contrapositive = Imp<Imp<A, B>, Imp<Not<B>, Not<A>>>;
const proof_contrapositive : Contrapositive =
    (a_imp_b : Imp<A, B>) =>
    (not_b : Not<B>) => ((a : A) => not_b(a_imp_b(a)));

}