#set document(title: "Homework 1", author: "Michael Zhang <zhan4854@umn.edu>")

= Homework 1
Michael Zhang \<zhan4854\@umn.edu\>

= Problem 1

$#math.op("f")\(x)$
== Problem 1
$top : "Set"$
$"case"_top$

$ "funsplit"(f, d) &equiv d("apply"(f, (x) x)) $

$ "funsplit"(f, d) &equiv d((x) "apply"(f, x)) $

$ "funsplit"(lambda b, d) &equiv d( "apply"(lambda b, (x) x)) \
&equiv d(((x)x)(b)) \

$ "funsplit"(lambda b, d) &equiv d((x) "apply"(lambda b, x)) \
&equiv d((x) (b(x))) \

NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$?

= Problem 2

== Problem 2

  axi[$x = y in NN [x in NN, y in NN]$],
  uni(right_label: "(3, 6)")[$"suc"(x) = "suc"(y) in NN [x in NN, y in NN]$],

  axi[$x in NN$],
  axi[$y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
  bin(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN$],
  uni(right_label: "(3)")[$"suc"("natrec"(x, 0, (u, v) "suc"(v))) = "suc"(x) in NN$],
  uni(right_label: "natrec")[$"natrec"("suc"(x), 0, (u, v) "suc"(v))) = "suc"(x) in NN$],

$ #tree(

$ #pad(left: -4em, tree(

  uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
) $

  uni(right_label: "(7, 9, 10)")[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
)) $

  uni(right_label: "(5)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],

  uni(right_label: "(5, 11)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],

#pagebreak()

// #pagebreak()

Then, we can use this:

// Then, we can use this:

#set math.equation(numbering: none)

// #set math.equation(numbering: none)

#tree(
  axi[$0 in NN$],
  uni(right_label: "(1)")[$0 = 0 in NN$],
  uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
)

// #tree(
//   axi[$0 in NN$],
//   uni(right_label: "(1)")[$0 = 0 in NN$],
//   uni(right_label: "(3)")[$"eq"_0 in "Eq"(NN, 0, 0)$],
// )

Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:

// Using $C(x) = NN$ and the substitution-in-elements rule, we can prove that suc distributes over equivalence:

#tree(
  axi[$"suc"(x) in C(x) [x in NN]$],
  axi[$x = y in NN$],
  bin[$"suc"(x) = "suc"(y) in NN$],
)

// #tree(
//   axi[$"suc"(x) in C(x) [x in NN]$],
//   axi[$x = y in NN$],
//   bin[$"suc"(x) = "suc"(y) in NN$],
// )

Then, convert this to Eq:

// Then, convert this to Eq:

#tree(
  axi[$"suc"(x) = "suc"(y) in NN$],
  axi[$x = y in NN$],
  bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
)

// #tree(
//   axi[$"suc"(x) = "suc"(y) in NN$],
//   axi[$x = y in NN$],
//   bin[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y))$],
// )

We can form a lambda term over eq objects using $lambda$-introduction:

// We can form a lambda term over eq objects using $lambda$-introduction:

#tree(
  axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
  uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
)

// #tree(
//   axi[$"eq"_"xy-suc" in "Eq"(NN, "suc"(x), "suc"(y)) ["eq"_"xy" in "Eq"(NN, x, y), x in NN, y in NN]$],
//   uni[$lambda(("eq"_"xy") "eq"_"xy-suc") in "Eq"(NN, x, y) arrow.r "Eq"(NN, "suc"(x), "suc"(y))$],
// )

This gives us what we need to perform induction over nats:

// This gives us what we need to perform induction over nats:

#tree(
  axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
  uni[]
)

// #tree(
//   axi[$"natrec"(x, "eq"_0, (u, v) "apply"(lambda(("eq"_"xy") "eq"_"xy-suc"), v)) [x in NN]$],
//   uni[]
// )

#tree(
  axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
  uni[],
)

// #tree(
//   axi[$"i'm fucking stupid" equiv (x) "natrec"(x, 0, (u, v) "suc"(v))$],
//   uni[],
// )

#tree(
  axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
  uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
  uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
)

// #tree(
//   axi[$"eq" in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x) [x in NN]$],
//   uni[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$],
//   uni(right_label: "macro")[$plus.circle(x, 0) = x in NN [x in NN]$],
// )

---
#pagebreak()

// ---
// #pagebreak()

#{
  let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]

// #{
//   let split1 = [$"natrec" (x, 0, (u, v) "suc"(v))$]

  tree(
    axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
    uni[$split1 equiv x in NN [x in NN]$],
  )

//   tree(
//     axi[$"natrec"(x, "refl", (u, v) ("ap" v)) [x in NN]$],
//     uni[$split1 equiv x in NN [x in NN]$],
//   )

  tree(
    // axi[$c in "Eq"(NN, split1, 0), x)$],
    axi[$split1 equiv x in NN [x in NN]$],
    uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )

//   tree(
//     // axi[$c in "Eq"(NN, split1, 0), x)$],
//     axi[$split1 equiv x in NN [x in NN]$],
//     uni(right_label: "macro")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
//   )

  tree(
    axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
    uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )

//   tree(
//     axi[$c in "Eq"(NN, plus.circle(x, 0), x)$],
//     uni[$plus.circle(x, 0) equiv x in NN [x in NN]$],
//   )

  tree(
    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
  )

//   tree(
//     axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
//   )

  tree(
    axi[$split1 equiv x [x in NN]$],
  )

//   tree(
//     axi[$split1 equiv x [x in NN]$],
//   )

  tree(
    axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
    axi[$split1 equiv x [x in NN]$],
    bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
  )
}

//   tree(
//     axi[$plus.circle(x, 0) equiv split1 [x in NN]$],
//     axi[$split1 equiv x [x in NN]$],
//     bin(right_label: "trans")[$plus.circle(x, 0) equiv x in NN [x in NN]$],
//   )
// }

module extraexercises where
open import Data.Nat
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

/**
 * Terms e ::= x | () | λx. e | e e | (e : A)
 * Types A, B, C ::= 1 | α | ^α | ∀α. A | A → B
 * Monotypes τ, σ ::= 1 | α | ^α | τ → σ
 * Contexts Γ, ∆, Θ ::= · | Γ, α | Γ, x : A
 *                      | Γ, ^α | Γ, ^α = τ | Γ, I^α
 * Complete Contexts Ω ::= · | Ω, α | Ω, x : A
 *                      | Ω, ^α = τ | Ω, I^
 */
export type Term =
  | { kind: "var"; name: string }
  | { kind: "unit" }
  | { kind: "lambda"; name: string; body: Term }
  | { kind: "app"; func: Term; arg: Term }
  | { kind: "annot"; term: Term; type: Type };
export type Type =
  | { kind: "unit" }
  | { kind: "var"; name: string }
  | { kind: "existential"; name: string }
  | { kind: "poly"; name: string; type: Type }
  | { kind: "arrow"; input: Type; output: Type };
export type Monotype =
  | { kind: "unit" }
  | { kind: "var"; name: string }
  | { kind: "existential"; name: string }
  | { kind: "arrow"; input: Monotype; output: Monotype };
export type ContextEntry =
  | { kind: "typeVar"; name: string }
  | { kind: "termAnnot"; name: string; type: Type }
  | { kind: "existentialVar"; name: string }
  | { kind: "existentialSolved"; name: string; type: Monotype }
  | { kind: "marker"; name: string };
export type CompleteContextEntry =
  | { kind: "typeVar"; name: string }
  | { kind: "termAnnot"; name: string; type: Type }
  | { kind: "existentialSolved"; name: string; type: Monotype }
  | { kind: "marker"; name: string };

// Helper functions for dealing with contexts
import { ContextEntry, Type } from "./data";
import { isEqual } from "lodash";
/** Γ |- A (is the given type in this context?) */
export function isTypeInContext(type: Type, ctx: ContextEntry[]): boolean {
  for (const entry of ctx) {
    switch (entry.kind) {
      case "termAnnot":
        if (isEqual(entry.type, type)) return true;
        break;
      default:
        continue;
    }
  }
  return false;
}

import { isTypeInContext } from "./contexts";
import { ContextEntry, Term, Type } from "./data";
function check(
  ctx: ContextEntry[],
  term: Term,
  type: Type
): [boolean, ContextEntry[]] {
  switch (term.kind) {
    case "var":
      break;
    case "unit":
      return [type.kind === "unit", ctx];
    case "lambda": {
      // Get A and B first
      if (type.kind !== "arrow") return [false, ctx];
      const { input: A, output: B } = type;
    }
    case "app":
      break;
    case "annot":
      break;
  }
}
function synthesize(ctx: ContextEntry[], term: Term): [Type, ContextEntry[]] {
  switch (term.kind) {
    case "var": {
      const res = lookupTypeVariable(ctx, term.name);
      if (!res) throw new Error("wtf?");
      return [res, ctx];
    }
    case "unit":
      return [{ kind: "unit" }, ctx];
    case "lambda": {
    }
    case "app":
      break;
    case "annot": {
      // Require that the type exists
      if (!isTypeInContext(term.type, ctx))
        throw new Error("type doesn't exist");
      // Require that the term checks against the type
      const [result, outputCtx] = check(ctx, term.term, term.type);
      if (!result) throw new Error("invalid annotation: term doesn't check");
      return [term.type, outputCtx];
    }
  }
}
function synthesizeApp(
  ctx: ContextEntry[],
  funcType: Type,
  term: Term
): [Type, ContextEntry[]] {}