csci8980-f23/hwk1.typ

#set page("us-letter")
#import "@preview/prooftrees:0.1.0": *

#let c(body) = {
  set text(gray)
  body
}

= Problem 1

#c[Define `funsplit` in terms of `apply`.]

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

In the case of $f = lambda b$ the following evaluation occurs:

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

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

#c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:

$ plus.circle(x, 0) = x ∈ NN [x ∈ NN] $

Please be pedantic and explicitly use a rule even for "obvious" steps. You do not have to draw a big derivation tree (which is difficult to typeset), but it should be clear which rule you are using at each step. If you are using an implicit rule that the authors did not explicitly write out, make it clear what it is. If you are not sure what a derivation tree is, whether a particular rule is allowed, or which emoji was just introduced in Emoji 15.1, use the Discord forum immediately.]

#set math.equation(numbering: "(1)")

First, let me reprint some rules from the textbook here to refer to them more easily from here on:

- Reflexivity (pg. 37 in textbook)

  $ #tree(axi[$a in A$], uni[$a = a in A$]) $

- Propositions as sets (pg. 37 in textbook)

  $ #tree(axi[$a∈A$], uni[$A "true"$]) $

- Substitution in elements from chapter 5 (pg. 38 in textbook)

  $ #tree(
    axi[$c(x) in C(x) [x in A]$],
    axi[$a = b in A$],
    bin[$c(a) = c(b) in C(a)$],
  ) $

- Eq-introduction rule (pg. 60 in textbook)

  $ #tree(axi[$a = b in A$], uni[$"eq" in "Eq"(A, a, b)$]) $

- Strong Eq-elimination (pg. 61 in textbook)

  $ #tree(axi[$c ∈ "Eq"(A, a, b)$], uni[$a=b∈A$]) $

- N-introduction (pg. 63 in textbook)

  $ #tree(axi[$a in NN$], uni[$"suc"(a) in NN$]) $

- Nat rec (pg. 64 in textbook)

  $ #tree(
    axi[$a in NN$],
    axi[$C(v) "set" [v in NN]$],
    axi[$d in C(0)$],
    axi[$e(x, y) in C("suc"(x)) [x in NN, y in C(x)]$],
    nary(4)[$"natrec"(a, d, e) in C(a)$],
  ) $


- Peano's 5th axiom (pg. 65 in textbook)

  $ #tree(
    axi[$a ∈ NN$],
    axi[$C(v) "prop" [v ∈ N]$],
    axi[$C(0) "true"$],
    axi[$C("suc"(x)) "true" [C(x) "true"]$],
    nary(4)[$C(a) "true"$]
  ) $

I can now form the derivation:

$ #tree(
  axi[$0 in NN$],
  uni(right_label: "(1)")[$0 = 0 in NN$],
  uni(right_label: "natrec")[$"natrec"(0, 0, (u, v) "suc"(v)) = 0 in NN$],
  uni(right_label: "(4)")[$"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$],
) $

$ #tree(
  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]$],
) $
  
$ #tree(
  axi(pad(bottom: .2em, [
    $x in NN$ \
    $"Eq"(NN, "natrec"(n, 0, (u, v) "suc"(v)), n) "set" [n in NN]$ \
    $"eq"_"0" in "Eq"(NN, "natrec"(0, 0, (u, v) "suc"(v)), 0)$ \
    $"eq"_"suc" (x, y) in "Eq"(NN, "natrec"("suc"(x), 0, (u, v) "suc"(v)), "suc"(x)) [x in NN, y in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)]$ \
  ])),
  uni[$"natrec"(x, "eq"_"0", "eq"_"suc") in "Eq"(NN, "natrec"(x, 0, (u, v) "suc"(v)), x)$],
) $

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

#pagebreak()

Then, we can use this:

#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)$],
)

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$],
)

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))$],
)

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))$],
)

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[$"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]$],
)

---
#pagebreak()

#{
  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[$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[$plus.circle(x, 0) equiv split1 [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]$],
  )
}