From f42dbda2343fb25c8271c76a7fb0fa52f56fbb33 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 5 Nov 2023 22:02:07 -0600 Subject: [PATCH] wip --- extra-problem-3.typ | 69 ++++++++++++++++++++++++++++++++++++++++++ extraexercises.agda | 54 +++++++++++++++++++++++++++------ hwk1.typ | 9 ++++-- hwk2.agda | 30 ++++++++++++++++++ hwk2.typ | 45 +++++++++++++++++++++++++++ scratch.typ | 74 +++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 268 insertions(+), 13 deletions(-) create mode 100644 extra-problem-3.typ create mode 100644 hwk2.agda create mode 100644 hwk2.typ create mode 100644 scratch.typ diff --git a/extra-problem-3.typ b/extra-problem-3.typ new file mode 100644 index 0000000..f32a0c5 --- /dev/null +++ b/extra-problem-3.typ @@ -0,0 +1,69 @@ +#import "@preview/prooftrees:0.1.0": * +#show math.eq: math.scripts +#let prooftree(..args) = tree( + tree_config: tree_config( + vertical_spacing: 6pt, + ), + ..args +) + += Problem 3 + +Assume that you have Id but not Eq at your disposal, and you can only use rules. Write down an abstraction unitl ("unitl" for "unit left") such that: + +#prooftree( + axi[$ d ∈ [a =_A b] $], + uni[$ "unitl"(a, d) ∈ ["trans"(id(a), d) =_[a =_A b] d] $], +) + +There's a trick here that you may notice if you remember the definition of "trans" and the computation rule for "idpeel": + +$ + "trans"(d,e) ≡ "apply"("idpeel"(d,(x)lambda y.y),e) +$ + +// #tree( +// axi[$a in A$], +// axi[$b in A$], +// axi[$c in "Id"(A, a, b)$], +// axi[$C(x, y, z) "set" [x in A, y in A, z in "Id"(A, x, y)]$], +// axi[$d(x) in C(x, x, "id"(x)) [x in A]$], +// nary(5)[$"idpeel"(c, d) in C(a, b, c)$], +// ) + +#prooftree( + axi[$a in A$], + axi[$C(x,y,z) "set" [x ∈ A, y ∈ A, z ∈ "Id"(A,x,y)]$], + axi[$d(x)∈ C(x,x,id(x)) [x∈A]$], + tri[$"idpeel"(id(a), d) = d(a) ∈ C(a, a, id(a))$], +) + +In our problem, $"trans"(id(a), d)$ exactly matches this format. +This means we can just macro-expand the left side of the definition: + +$ + "trans"(id(a), d) &=_[a =_A b] d \ + "apply"("idpeel"(id(a), (x)lambda y.y), d) &=_[a =_A b] d \ + "apply"(((x)lambda y.y)(a), d) &=_[a =_A b] d \ + "apply"((lambda y.y), d) &=_[a =_A b] d \ + d &=_[a =_A b] d \ +$ + +This means we're really looking for a definition for $"unitl"(a, d) in [d =_[a =_A b] d]$. +This can just be constructed using the canonical element $id(d)$. The full derivation looks like this: + +#prooftree( + axi[$A "set"$], + axi[$a in A$], + axi[$b in A$], + axi[$d in [a =_A b]$], + nary(4, right_label: "Reflexivity")[$d = d in [a =_A b]$], +) + +#prooftree( + axi[$A "set"$], + axi[$a in A$], + axi[$b in A$], + axi[$d in [a =_A b]$], + nary(4, right_label: "Id-introduction")[$id(d) in [d =_[a =_A b] d]$], +) \ No newline at end of file diff --git a/extraexercises.agda b/extraexercises.agda index f885f9d..9ecb9f0 100644 --- a/extraexercises.agda +++ b/extraexercises.agda @@ -10,22 +10,56 @@ J : {A : Set} → (x y : A) → (p : x ≡ y) → C x y p J C c x x refl = c x +-- Translation to PMLTT concepts + +id : {A : Set} (a : A) → a ≡ a +id a = refl + +idpeel : {A : Set} {a b : A} + → (c : a ≡ b) + → {C : (x y : A) → (z : x ≡ y) → Set} + → (d : (x : A) → C x x (id x)) + → C a b c +idpeel {A} {a} {b} c {C} d = J C d a b c + +-- Problem 2 + inv : {A : Set} {a b : A} → (d : a ≡ b) → sym (sym d) ≡ d inv {A} {a} {b} d = - J (λ x y p → sym (sym p) ≡ p ) (λ x → refl) a b d + J (λ x y p → sym (sym p) ≡ p) (λ x → refl) a b d --- Problem 2 +-- assoc : {A : Set} {a b c d : A} +-- → (e : a ≡ b) +-- → (f : b ≡ c) +-- → (g : c ≡ d) +-- → trans (trans e f) g ≡ trans e (trans f g) +-- assoc {a} {b} {c} {d} e f g = +-- let whatever = (λ f → J (λ x y p → trans (trans x f) y ≡ trans x (trans f y)) (λ x → {! !}) {! !} {! !} {! !}) in +-- {! !} -assoc : {A : Set} {a b c d : A} - → (e : a ≡ b) - → (f : b ≡ c) - → (g : c ≡ d) - → trans (trans e f) g ≡ trans e (trans f g) -assoc {a} {b} {c} {d} e f g = - let whatever = J {! !} {! !} {! !} {! !} {! !} in - {! !} +-- Problem 3 + +unitl : {A : Set} + → (a : A) + → {b : A} + → (d : a ≡ b) + → trans (id a) d ≡ d +unitl a d = id d + +-- Problem 4 + +unitr : {A : Set} + → {a : A} + → (b : A) + → (d : a ≡ b) + → trans d (id b) ≡ d +unitr {A} {a} b d = J (λ x y p → trans p (id y) ≡ p) (λ x → id (id x)) a b d + +-- Problem 5 + +-- ap : {A : Set} -- Problem 6 diff --git a/hwk1.typ b/hwk1.typ index 537c520..92bfaa9 100644 --- a/hwk1.typ +++ b/hwk1.typ @@ -94,8 +94,10 @@ First, let me reprint some rules from the textbook here to refer to them more ea I can now form the derivation: $ #tree( + axi[], + uni[$NN "set"$], axi[$0 in NN$], - uni(right_label: "(1)")[$0 = 0 in NN$], + bin(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)$], ) $ @@ -119,8 +121,9 @@ $ #pad(left: -4em, tree( )) $ #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, 11)")[$"natrec"(x, 0, (u, v) "suc"(v)) = x in NN [x in NN]$], + axi[], + uni(right_label: "(11)")[$"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]$], ) diff --git a/hwk2.agda b/hwk2.agda new file mode 100644 index 0000000..55e61ee --- /dev/null +++ b/hwk2.agda @@ -0,0 +1,30 @@ +module hwk2 where + +open import Data.Nat +open import Data.Sum +open import Data.Unit +open import Data.Empty +open import Relation.Binary.PropositionalEquality as Eq hiding (subst) +open Eq.≡-Reasoning + +J : {A : Set} + → (C : (x y : A) → x ≡ y → Set) + → (c : (x : A) → C x x refl) + → (x y : A) → (p : x ≡ y) → C x y p +J C c x x refl = c x + +subst : {A : Set} {a b : A} + → (P : A → Set) + → (c : a ≡ b) + → (p : P a) + → P b +subst {A} {a} {b} P c = J (λ x y p → (P x → P y)) (λ x → (λ a → a)) a b c + +discriminate : {A : Set} {B : Set} → (s : A ⊎ B) → Set +discriminate (inj₁ x) = ⊤ +discriminate (inj₂ y) = ⊥ + +problem2 : {A : Set} {B : Set} + → (a : A) → (b : B) + → inj₁ a ≢ inj₂ b +problem2 a b p = subst discriminate p tt \ No newline at end of file diff --git a/hwk2.typ b/hwk2.typ new file mode 100644 index 0000000..edab7d5 --- /dev/null +++ b/hwk2.typ @@ -0,0 +1,45 @@ +#set document(title: "Homework 2", author: "Michael Zhang ") +#set page("us-letter") +#import "@preview/prooftrees:0.1.0": * +#import emoji: face + += Homework 2 + +Michael Zhang \ + +#let c(body) = { + set text(gray) + body +} + +#c[Assume you have $"Id"$ and $"U"$ but not $"Eq"$ (or $hat("Eq")$). Write down an abstraction $p$ such that + +#tree( + axi[$a in A [Gamma]$], + axi[$b in B [Gamma]$], + bin[$p(a, b) in "Id"(A+B, "inl"(a), "inr"(b)) arrow.r emptyset [Gamma]$] +) + +is derivable. You do not have to prove in your submission that it is derivable.] + +Wait isn't this just the same as the Peano's fourth axiom as given in the book? + +$ + p(a, b) &equiv lambda ((x) "subst"(x, "tt")) \ +$ + +where +- $P(m) = "Set"("when"(m, (x)hat(top), (y)hat({})))$ + +// (Agda implementation #face.smile.slight) + +// ```agda +// discriminate : {A : Set} {B : Set} → (s : A ⊎ B) → Set +// discriminate (inj₁ x) = ⊤ +// discriminate (inj₂ y) = ⊥ + +// problem2 : {A : Set} {B : Set} +// → (a : A) → (b : B) +// → inj₁ a ≢ inj₂ b +// problem2 a b p = subst discriminate p tt +// ``` \ No newline at end of file diff --git a/scratch.typ b/scratch.typ new file mode 100644 index 0000000..00b30d8 --- /dev/null +++ b/scratch.typ @@ -0,0 +1,74 @@ +#import "@preview/prooftrees:0.1.0": * + += 1 + +#tree( + axi[$d in [a =_A b]$], + uni[$"inv"(d) in ["symm"("symm"(d)) =_[a =_A b] d]$], +) + +Defined by: + +$ + "inv"(d) equiv "idpeel"(d, (x) id(id(x))) +$ + +Derivation tree: + +#tree( + axi[], + uni[$A "set"$], +) + += 2 + +``` +d∈[a=A b] e∈[b=A c] +------------------- + trans(d, e) ∈ [a =A c] + +trans(d,e) ≡ apply(idpeel(d,(x)λy.y),e) +``` + +``` +trans (trans e f) g == trans e (trans f g) + +apply(idpeel( + apply(idpeel(e, (x)\y.y), f), + (x)\y.y, +), g) +``` + += 3 + +#tree( + axi[$d in [a =_A b]$], + uni[$"unitl"(a, d) ∈ ["trans"(id(a), d) =_[a =_A b] d]$] +) + +--- + +Simplifying the output type: + +$ + "trans"(id(a), d) &=_[a =_A b] d \ + "apply"("idpeel"(id(a), (x)lambda y.y), d) &=_[a =_A b] d \ + "apply"(((x)lambda y.y)(a), d) &=_[a =_A b] d \ + "apply"((lambda y.y), d) &=_[a =_A b] d \ + d &=_[a =_A b] d \ +$ + +This is just a reflexive equality so can be satisfied by $"id"$: + +$ "unitl"(a, d) equiv id(d) $ + += 4 + +#tree( + axi[$d in [a =_A b]$], + uni[$"unitr"(d, b) in ["trans"(d, id(b)) =_[a =_A b] d]$], +) + +$ + "unitr"(d, b) equiv "idpeel"(d, (x)id(id(x))) \ +$ \ No newline at end of file