proof that n + 0 = n in typescript

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

// 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

Ts Playground: https://www.typescriptlang.org/play/?ts=5.6.0-dev.20240702#code/FAehAIDkEMBdlgTwA4FMp3AXnAb3ANYCWAdgCYBc4ARAF6oBOA9teAL7gA+ehplNAZwCuAY2oBucMgap+MWO3HBgIpiQEL6zKvOw9i5KnUYtFKtRvDCRegBQkdcAJSOFWAHzhb+A-2rXqABopGX4Sdiclc3UFaDIyO2hXYIAjVxcMN09cYHBwIgAzL2gAOl9sLBxjZmoncBlYIQZwlKU8hqbw61s4sh6S6VlUp0jgNiiwcGghAA8iABsiaAZwAEchdABzZegSBXX0AAUrVAAraEyEFCPQgHkC+QAeSHBUGdhUcgFMzxwXt4+X30fCMAUkg34pAKjHAxw4AH5YeAqCRUAA3RgTCCHZhoi7hADU4AADHpwsgdmshNB5gcViQrmhwABBeIALRMj2Zr3enzI33kvxZPMB-OBhhoWlMbFy4ERzNlVG5AL53x8IMEogkIVkVChMLhssR6ol-i14NCSvZnJxsnuT2Z7k8MryKPRmOUSCZzIEAkYsC5wQAQkLlbygUG5V5IyqgdzEbAGBtkeACjS-XUqGn5n6seAACqoDRFxnoQsaACMeh9foYAdZZA5zEeJr8UtYbHcwVbRnb7HckkmiY2pYLRdgACZq77-Y9ZQ2m0wW7xTWCdfwe5KTB3+4FZZuzWILbrxW3t+x2MAB+Ah0nUEA