proving stuff in typescript.ts

proving stuff in typescript.ts

// We prove this theorem: forall A,B,C.   A \/ B -> C <-> (A -> C) /\ (B -> C)
// by representing the theorem as a type and showing the type is inhabited.
// To show type inhabitation, we make a value of the type.
// Note: this proof actually demonstrates something practical in programming:
// part of why the visitor pattern can be helpful in OO languages that don't have
// much support for sum types ("or"/algebraic data types) but do have product types ("and"/records).
// https://cs.stackexchange.com/questions/139003/is-there-a-relationship-between-visitor-pattern-and-demorgans-law
type Theorem<A, B, C> = Iff<
                ((either: Or<A, B>) => C),
                And<(a: A) => C, (b: B) => C>
                >;

type Or<T, U> =
    | {tag: 'orLeft', value: T}
    | {tag: 'orRight', value: U};

type And<A, B> = {andLeft: A, andRight: B};
type If<A, B> = (a: A) => B
type Iff<A, B> = And<If<A, B>, If<B, A>>;

// 'forall' is interpreted as a generic function
// uses some helpers below
function proof<A, B, C>(): Theorem<A, B, C> {
    const leftToRight: (fn: (either: Or<A, B>) => C) => And<If<A, C>, If<B, C>>  = 
        (or_to_c) => ({
            andLeft: a => or_to_c(orIntroLeft(a)),
            andRight: b => or_to_c(orIntroRight(b)),
        });
    const rightToLeft:  (and: And<If<A, C>, If<B, C>>) => (either: Or<A, B>) => C = 
        ({andLeft, andRight}) => (or: Or<A, B>): C => {
            switch (or.tag) {
                case 'orLeft':
                    const a: A = or.value;
                    return andLeft(a);
                case 'orRight':
                    const b: B = or.value;
                    return andRight(b);
                default:
                    or satisfies never;
                    return or;

            }
        }
    return {andLeft: leftToRight, andRight: rightToLeft};
}

// helpers to create an `Or` and take apart an `Or`.
// We don't create such helpers for `And`
// because creating and taking apart objects is easy in TypeScript
function orIntroLeft<A, B>(orLeft: A): Or<A, B> {
    return {tag: 'orLeft', value: orLeft};
}
function orIntroRight<A, B>(orRight: B): Or<A, B> {
    return {tag: 'orRight', value: orRight};
}


// We proved a theorem by showing that a type was inhabited.
// This deep connection between logic and type theory
// is the insight of https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
// and https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf.
// The latter is hard to read due to notation, imo. The first chapter of the (free)
// HoTT book I find much more accessible, and better at comparing with set theory.
// https://homotopytypetheory.org/book/ (no topology in the first chapter).

// A bunch more proofs that show the relationships between theorems of classical logic
// and when we have to assume excluded middle/double-negation-elimmination

type Not<T> = (t: T) => never;
type ExcludedMiddle<T> = Or<T, Not<T>>;

const todo = Symbol('todo'); // helpful when proving bit-by-bit, since there is only one value of this type

// not provable (without infinite-looping, throwing, assuming something equivalent, or otherwise cheating)
function proofOfExcludedMiddle<T>(t: T): ExcludedMiddle<T> {
        return todo; // ??
}

type Person = {height: number, punctual: boolean};
const aPerson: Person = {height: 1, punctual: true};

// But of course it would be super weird if we could summon an excluded middle for any type
// out of thin air
function useExcludedMiddleOfPerson(em: ExcludedMiddle<Person>): boolean {
    switch (em.tag) {
        case "orLeft":
            // where could this person come from?
            const person = em.value;
            return person.punctual;
        case "orRight":
            return em.value(aPerson);
        default:
            em satisfies never;
            return em;
    }
}


// "Faustian bargain"
function proofOfNotNotExcludedMiddle<T>(): Not<Not<ExcludedMiddle<T>>> {
    return (notExcludedMiddle) => notExcludedMiddle(orIntroRight((t: T) => notExcludedMiddle(orIntroLeft(t))))
}

const notNotExcludedMiddleOfPerson: Not<Not<ExcludedMiddle<Person>>> = proofOfNotNotExcludedMiddle();
notNotExcludedMiddleOfPerson((em: ExcludedMiddle<Person>): never => {
    switch (em.tag) {
        case "orLeft":
            // it looks like we get a Person value out of nowhere,
            // but really it's the person we provide in the "orRight" case
            const _p: Person = em.value;
            console.log(_p)
            return todo; // ???
        case "orRight":
            const notPerson: Not<Person> = em.value;
            notPerson(aPerson);
        default:
            em satisfies never
            return em;
    }
})

type DoubleNegationIntro<A> = (a: A) => Not<Not<A>>

function proofOfDoubleNegationIntro<A>(): DoubleNegationIntro<A> {
    return (a: A): Not<Not<A>> => (notA: Not<A>): never => notA(a);
}

type DoubleNegationElim<A> = (notNot: Not<Not<A>>) => A;

function proofOfDoubleNegationElim<A>(excludedMiddle: ExcludedMiddle<A>): DoubleNegationElim<A> {
    return (notNot: Not<Not<A>>): A => {
        switch (excludedMiddle.tag) {
            case 'orLeft':
                const a: A = excludedMiddle.value;
                return a;
            case 'orRight':
                const notA: Not<A> = excludedMiddle.value;
                return notNot(notA); // use of exfalso
            default:
                excludedMiddle satisfies never;
                return excludedMiddle;
        }
    }
}

type CounterexamplePrinciple<A, B> = If<Not<If<A, B>>, And<A, Not<B>>>

function proofOfCounterexamplePrinciple<A, B>(excludedMiddle: <T>() => ExcludedMiddle<T>): CounterexamplePrinciple<A, B> {
    return (notIf: Not<If<A, B>>): And<A, Not<B>> => {
            const emA = excludedMiddle<A>();
            const emB = excludedMiddle<B>();
            switch(emA.tag) {
                case "orLeft": {
                    const a: A = emA.value;
                    switch (emB.tag) {
                        case "orLeft": {
                            const b: B = emB.value;
                            return notIf((_) => b);
                        }
                        case "orRight": {
                            const notB: Not<B> = emB.value;
                            return {andLeft: a, andRight: notB};
                        }
                        default:
                            emB satisfies never;
                            return emB;
                    }
                }
                case "orRight": {
                    const notA: Not<A> = emA.value;
                    const aToB = (a: A): never => notA(a);
                    return notIf(aToB); // exfalso
                }
                default:
                    emA satisfies never;
                    return emA;
            }
    }
}

type HalfDeMorgansLaw<A, B> = (or: Or<Not<A>, Not<B>>) => Not<And<A, B>>;
type DeMorgansLaw<A, B> = Iff<Not<And<A, B>>, Or<Not<A>, Not<B>>>

function proofOfHalfDemorgansLaw<A, B>(): HalfDeMorgansLaw<A, B> {
    return (or: Or<Not<A>, Not<B>>): Not<And<A, B>> => {
           switch (or.tag) {
                case "orLeft":
                    const notA: Not<A> = or.value;
                    return (and: And<A, B>) => notA(and.andLeft);
                case "orRight":
                    const notB: Not<B> = or.value;
                    return (and: And<A, B>) => notB(and.andRight);
                default:
                    or satisfies never;
                    return or;
                
           }
    }
}



function proofOfDemorgansLaw<A, B>(excludedMiddle: <T>() => ExcludedMiddle<T>): DeMorgansLaw<A, B> {
    return {
        andLeft: (notBoth: Not<And<A, B>>): Or<Not<A>, Not<B>> => {            
            const emA = excludedMiddle<A>();
            const emB = excludedMiddle<B>();
            switch(emA.tag) {
                case "orLeft": {
                    const a: A = emA.value;
                    switch (emB.tag) {
                        case "orLeft": {
                            const b: B = emB.value;
                            return notBoth({andLeft: a, andRight: b})
                        }
                        case "orRight": {
                            const notB: Not<B> = emB.value;
                            return orIntroRight(notB);
                        }
                        default:
                            emB satisfies never;
                            return emB;
                    }
                }
                case "orRight": {
                    const notA: Not<A> = emA.value;
                    return orIntroLeft(notA);
                }
            }
        },
        andRight: proofOfHalfDemorgansLaw(),
    }
}

type TarskisFormula<A, B> = Or<A, If<A, B>>;

function proofOfTarskisFormula<A, B>(emA: ExcludedMiddle<A>): TarskisFormula<A, B> {
    switch (emA.tag) {
        case 'orLeft': {
            const a: A = emA.value;
            return orIntroLeft(a);
        }
        case 'orRight': {
            const notA: Not<A> = emA.value;
            return orIntroRight((a: A): B => notA(a) /*exfalso*/);
        }
        default:
            emA satisfies never;
            return emA;
    }
}

type Linearity<A, B, C> = Or<If<A, B>, If<B, C>>;
function proofOfLinearity<A, B, C>(emB: ExcludedMiddle<B>): Linearity<A, B, C> {
    switch (emB.tag) {
        case "orLeft": {
            const b: B = emB.value;
            return orIntroLeft((_: A) => b);
        }
        case "orRight": {
            const notB: Not<B> = emB.value;
            return orIntroRight(notB);
        }
        default:
            emB satisfies never;
            return emB;
    }
}

type ClaviusLaw<A> = If<If<Not<A>, A>, A>;
function proofOfClaviusLaw<A>(emA: ExcludedMiddle<A>): ClaviusLaw<A> {
    return (ifNotAA: If<Not<A>, A>): A => {
        switch (emA.tag) {
            case 'orLeft': {
                const a: A = emA.value;
                return a;
            }
            case 'orRight': {
                const notA: Not<A> = emA.value;
                return ifNotAA(notA);
            }
            default:
                emA satisfies never;
                return emA;
        }
    }
}
function proofOfExcludedMiddleFromDoubleNegationElim<A>(notNotElim: <T>() => DoubleNegationElim<T>): ExcludedMiddle<A> {
    return notNotElim<ExcludedMiddle<A>>()(proofOfNotNotExcludedMiddle<A>());
}

type PiercesLaw<A, B> = If<If<If<A, B>, A>, A>;
function proofOfPiercesLaw<A, B>(emA: ExcludedMiddle<A>): PiercesLaw<A, B> {
    return (ifIfAA: If<If<A, B>, A>): A => {
        switch (emA.tag) {
            case 'orLeft': {
                const a: A = emA.value;
                return a;
            }
            case 'orRight': {
                const notA: Not<A> = emA.value;
                return ifIfAA(notA); // exfalso
            }
            default:
                emA satisfies never;
                return emA;
        }   
    }
}

type WeakExcludedMiddle<A> = Or<Not<A>, Not<Not<A>>>;
function proofOfWeakExcludedMiddle<A>(emA: ExcludedMiddle<A>): WeakExcludedMiddle<A> {
        switch (emA.tag) {
        case 'orLeft': {
            const a: A = emA.value;
            return orIntroRight(proofOfDoubleNegationIntro<A>()(a));
        }
        case 'orRight': {
            const notA: Not<A> = emA.value;
            return orIntroLeft(notA);
        }
        default:
            emA satisfies never;
            return emA;
    }   
}

type NotNotDoubleNegationElim<A> = If<Not<Not<Not<Not<A>>>>, Not<Not<A>>>;
function proofOfNotNotDoubleNegationElim<A>(): NotNotDoubleNegationElim<A> {
   return (fourNot: Not<Not<Not<Not<A>>>>): Not<Not<A>> =>
        (notA: Not<A>): never =>  {
            const threeNot: Not<Not<Not<A>>> = proofOfDoubleNegationIntro<Not<A>>()(notA);
            return fourNot(threeNot);
        }
}