Skip to content

Instantly share code, notes, and snippets.

@yazaldefilimone

yazaldefilimone/proof-that-n-plus-zero-equal-n-in-typescript.ts

Created July 2, 2024 14:50
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save yazaldefilimone/a5e783f1760d66f298029b356f2b851a to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save yazaldefilimone/a5e783f1760d66f298029b356f2b851a to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. yazaldefilimone created this gist Jul 2, 2024.
    29 changes: 29 additions & 0 deletions proof-that-n-plus-zero-equal-n-in-typescript.ts
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,29 @@
    // Nat
    type Nat = { kind: "zero" } | { kind: "suc"; pred: Nat };

    const zero: Nat = { kind: "zero" };
    const suc = (n: Nat): Nat => ({ kind: "suc", pred: n });

    const add = (a: Nat, b: Nat): Nat => {
    if (a.kind === "zero") return b;
    return suc(add(a.pred, b));
    };

    // auxiliar que garant que P seja Nat
    type PredOfNat<N extends Nat> = N extends { kind: "suc"; pred: infer P } ? P : never;

    // Prova n + 0 = n para qualquer n
    type AddZero<A extends Nat> = A extends { kind: "zero" }
    ? A
    : A extends { kind: "suc"; pred: infer P }
    ? { kind: "suc"; pred: AddZero<PredOfNat<A>> }
    : never;

    type Assert<A, B> = A extends B ? (B extends A ? true : false) : false;

    // Testes
    type Test1 = Assert<AddZero<{ kind: "zero" }>, { kind: "zero" }>; // true
    type Test2 = Assert<
    AddZero<{ kind: "suc"; pred: { kind: "zero" } }>,
    { kind: "suc"; pred: { kind: "zero" } }
    >; // true