waht the hell
[?]
Oct 19, 2023, 4:27 AM
EZBRGLPMQGBK7JUOGBBDXCV5AEQBDORL7K6F7O53AYQDAIFW5MDACDependencies
- [2]
IJD7EFTXinit
Change contents
- edit in hwk1.typ at line 1
#set page("us-letter") - replacement in hwk1.typ at line 4
#let natrec = text[natrec]#let suc = text[suc]#let c(body) = {set text(gray)body} - replacement in hwk1.typ at line 11
Define `funsplit` in terms of `apply`.#c[Define `funsplit` in terms of `apply`.] - edit in hwk1.typ at line 20
NOTE: Is it "cheating" in some sense, to use the identity abstraction $(x) x$ in the place of the last parameter to $"apply"$? - replacement in hwk1.typ at line 25
Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove:#c[Assuming that you have Eq sets at your disposal, use only rules (without appealing to the One True Language) to prove: - edit in hwk1.typ at line 28
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) - replacement in hwk1.typ at line 45
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.$ #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]$],) - edit in hwk1.typ at line 167
---#pagebreak() - replacement in hwk1.typ at line 171
tree(axi[$C(v) "set" [v in NN]$],axi[$x in NN$],axi[$d in C(0)$],axi[$x in NN$],nary(4)[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],)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]$],) - replacement in hwk1.typ at line 193
tree(axi[],uni[$plus.circle(x, 0) equiv natrec(x, 0, (u, v) suc(v)) [Gamma tack.r x in NN]$],axi[$natrec(x, 0, (u, v) suc(v)) equiv x [Delta tack.r x in NN]$],bin[$plus.circle(x, 0) equiv x in NN [(Gamma, Delta) tack.r 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]$],) - file addition: hwk1.agda[2.2]
module hwk1 whereopen import Data.Natopen import Relation.Binary.PropositionalEquality as Eqopen Eq.≡-Reasoningnatrec : {C : Set} → (a : ℕ) → (d : C) → (e : ℕ → C → C) → Cnatrec zero d e = dnatrec (suc b) d e = e b (natrec b d e)⊕ : ℕ → ℕ → ℕ⊕ x y = natrec x y (λ u v → suc v)problem2-lemma : (x : ℕ) → natrec x 0 (λ u v → suc v) ≡ xproblem2-lemma zero = reflproblem2-lemma (suc x) = cong suc (problem2-lemma x)-- (λ u v → suc v) x (natrec x 0 (λ u v → suc v))-- suc (natrec x 0 (λ u v → suc v))problem2 : (x : ℕ) → ⊕ x 0 ≡ xproblem2 x = problem2-lemma x-- begin-- ⊕ x 0-- ≡⟨⟩-- natrec x 0 (λ u v → suc v)-- ≡⟨ {! !} ⟩-- x-- ∎ - replacement in csci8980-f23.agda-lib at line 1
include: bidirinclude: . bidir - edit in .gitignore at line 3[2.92199]
_build