From ce6a6f734ab044715fc0026bb5b6fbd06a1d94e6 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 15 Oct 2024 00:00:27 -0500 Subject: [PATCH] remove existing stuff --- src/LogRel.agda | 202 ------------------ .../HoTT/LongExactSequence.agda | 4 - src/VanDoornDissertation/PropTrunc.agda | 26 --- .../Spectral/Algebra/SpectralSequence.agda | 7 - 4 files changed, 239 deletions(-) delete mode 100644 src/LogRel.agda delete mode 100644 src/VanDoornDissertation/HoTT/LongExactSequence.agda delete mode 100644 src/VanDoornDissertation/PropTrunc.agda delete mode 100644 src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda diff --git a/src/LogRel.agda b/src/LogRel.agda deleted file mode 100644 index 23a1698..0000000 --- a/src/LogRel.agda +++ /dev/null @@ -1,202 +0,0 @@ --- https://www.cs.uoregon.edu/research/summerschool/summer24/lectures/Ahmed.pdf - -module LogRel where - -open import Data.Bool -open import Data.String -open import Data.Sum -open import Data.Empty -open import Data.Nat -open import Data.Maybe -open import Data.Product -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary.Negation -open import Relation.Nullary using (Dec; yes; no) - -_∙_ = trans - -data type : Set where - bool : type - _-→_ : type → type → type - -data term : Set where - `_ : String → term - true : term - false : term - `if_then_else_ : term → term → term → term - `λ[_∶_]_ : String → type → term → term - _`∙_ : term → term → term - -replace : (e : term) → (x : String) → (v : term) → term -replace (` y) x v = if x == y then v else (` y) -replace true x v = true -replace false x v = false -replace (`if e then e₁ else e₂) x v = `if (replace e x v) then replace e₁ x v else replace e₂ x v -replace e @ (`λ[ y ∶ t ] e′) x v = if x == y then e else (`λ[ y ∶ t ] replace e′ x v) -replace (e₁ `∙ e₂) x v = replace e₁ x v `∙ replace e₂ x v - -data value : term → Set where - true : value true - false : value false - `λ[_∶_]_ : (x : String) → (t : type) → (e : term) → value (`λ[ x ∶ t ] e) - -to-value : (t : term) → Maybe (value t) -to-value (` x) = nothing -to-value true = just true -to-value false = just false -to-value (`if t then t₁ else t₂) = nothing -to-value (`λ[ x ∶ t ] e) = just (`λ[ x ∶ t ] e) -to-value (t `∙ t₁) = nothing - -is-value : (t : term) → Set -is-value t = Is-just (to-value t) - -data ectx : Set where - [∙] : ectx - `if_then_else_ : ectx → term → term → ectx - _`∙_ : ectx → term → ectx - _∙`_ : {e : term} → value e → ectx → ectx - -data ctx : Set where - ∅ : ctx - _,_∶_ : ctx → String → type → ctx - -data sub : Set where - ∅ : sub - _,_≔_ : sub → String → term → sub - -evalsub : sub → term → term -evalsub ∅ e = e -evalsub (γ , x ≔ v) e = replace (evalsub γ e) x v - -lookup : ctx → String → Maybe type -lookup ∅ x = nothing -lookup (Γ , y ∶ t) x = if (x == y) then just t else lookup Γ x - --- Some dumb stuff - -lemma1 : ∀ (γ : sub) → evalsub γ true ≡ true -lemma1 ∅ = refl -lemma1 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma1 γ) - -lemma2 : ∀ (γ : sub) → evalsub γ false ≡ false -lemma2 ∅ = refl -lemma2 (γ , x ≔ v) = cong (λ z → replace z x v) (lemma2 γ) - --- Operational semantics - -data _↦_ : term → term → Set where - rule1 : (e1 e2 : term) → (if true then e1 else e2) ↦ e1 - rule2 : (e1 e2 : term) → (if false then e1 else e2) ↦ e2 - rule3 : (x : String) → (t : type) → (e : term) → (v : term) - → ((`λ[ x ∶ t ] e) `∙ v) ↦ replace e x v - -data iter : ℕ → term → term → Set where - iter-zero : ∀ (e : term) → iter zero e e - iter-suc : ∀ (n : ℕ) → (e e′ e′′ : term) → iter n e e′ → (e′ ↦ e′′) → iter (suc n) e′ e′′ - -_↦∙_ : term → term → Set -e ↦∙ e′ = Σ ℕ λ n → iter n e e′ - --- Type judgments - -data _⊢_∶_ : ctx → term → type → Set where - type1 : (Γ : ctx) → Γ ⊢ true ∶ bool - type2 : (Γ : ctx) → Γ ⊢ false ∶ bool - type3 : (Γ : ctx) → (x : String) → (tw : Is-just (lookup Γ x)) → Γ ⊢ ` x ∶ to-witness tw - type4 : (Γ : ctx) → (x : String) → (e : term) → (t₁ t₂ : type) - → ((Γ , x ∶ t₁) ⊢ e ∶ t₂) → Γ ⊢ `λ[ x ∶ t₁ ] e ∶ (t₁ -→ t₂) - type5 : (Γ : ctx) → (e₁ e₂ : term) → (t t₂ : type) - → (Γ ⊢ e₁ ∶ (t₂ -→ t)) → (Γ ⊢ e₂ ∶ t₂) → Γ ⊢ e₁ `∙ e₂ ∶ t - type6 : (Γ : ctx) → (e e₁ e₂ : term) → (t : type) - → (Γ ⊢ e ∶ bool) → (Γ ⊢ e₁ ∶ t) → (Γ ⊢ e₂ ∶ t) - → Γ ⊢ `if e then e₁ else e₂ ∶ t - --- Type soundness - -type-soundness : ∀ {e e′ t} → (∅ ⊢ e ∶ t) → (e ↦∙ e′) → Set -type-soundness {e = e} {e′ = e′} {t = t} prf eval = - (value e) ⊎ Σ term λ e′′ → e′ ↦ e′′ - --- Safety - -safe : term → Set -safe e = ∀ (e′ : term) → e ↦∙ e′ → (value e′) ⊎ Σ term (λ e′′ → (e′ ↦ e′′)) - --- Logical relations - -data V : type → term → Set -data E : type → term → Set - -data V where - bool-true : V bool true - bool-false : V bool false - →-λ : ∀ (x : String) → (e : term) → (t₁ t₂ : type) - → ((v : term) → V t₁ v → E t₂ (replace e x v)) → V (t₁ -→ t₂) (`λ[ x ∶ t₁ ] e) - -irred : (e : term) → Set -irred e = ¬ (Σ term (λ e′ → e ↦ e′)) - -data E where - erel : ∀ (e : term) → (t : type) - → ((e′ : term) → ((e ↦∙ e′) × irred e′) → V t e′) → E t e - -data G : ctx → sub → Set where - nil : G ∅ ∅ - cons : ∀ (Γ : ctx) → (x : String) → (t : type) → (γ : sub) → (v : term) - → (G Γ γ) ⊎ V t v - → G (Γ , x ∶ t) (γ , x ≔ v) - --- Semantically well-typed - -_⊨_∶_ : (Γ : ctx) → (e : term) → (t : type) → Set -Γ ⊨ e ∶ t = ∀ (γ : sub) → G Γ γ → E t (evalsub γ e) - --- Theorem 4.2: fundamental property of logical relations - -theorem42 : ∀ (Γ : ctx) → (e : term) → (t : type) → Γ ⊢ e ∶ t → Γ ⊨ e ∶ t -theorem42 Γ e t (type1 .Γ) γ G[γ] = - subst (E bool) (sym (lemma1 γ)) (erel e bool helper) where - helper : (e′ : term) → (true ↦∙ e′) × irred e′ → V bool e′ - helper e′ ((zero , iter-zero .true) , snd) = bool-true - helper e′ ((suc n , iter-suc .n e .true .true fst (rule1 .true e2)) , snd) = bool-true - helper e′ ((suc n , iter-suc .n e .true .true fst (rule2 e1 .true)) , snd) = bool-true -theorem42 Γ e t (type2 .Γ) γ G[γ] = - subst (E bool) (sym (lemma2 γ)) (erel e bool helper) where - helper : (e′ : term) → (false ↦∙ e′) × irred e′ → V bool e′ - helper e′ ((zero , iter-zero .false) , snd) = bool-false - helper e′ ((suc n , iter-suc .n e .false .false fst (rule1 .false e2)) , snd) = bool-false - helper e′ ((suc n , iter-suc .n e .false .false fst (rule2 e1 .false)) , snd) = bool-false -theorem42 Γ e t (type3 .Γ x tw) γ G[γ] = erel {! !} {! !} {! !} -theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) ∅ G[γ] = erel (`λ[ x ∶ t₁ ] e₁) t helper where - helper : (e′ : term) → ((`λ[ x ∶ t₁ ] e₁) ↦∙ e′) × irred e′ → V (t₁ -→ t₂) e′ - helper e′ ((zero , iter-zero .(`λ[ x ∶ t₁ ] e₁)) , snd) = - →-λ x e₁ t₁ t₂ λ v x₁ → erel {! !} {! !} {! !} - helper e′ ((suc n , fst) , snd) = {! !} -theorem42 Γ e t (type4 .Γ x e₁ t₁ t₂ sts) (γ , x₁ ≔ x₂) G[γ] = - {! !} -theorem42 Γ e t (type5 .Γ e₁ e₂ .t t₂ sts sts₁) = {! !} -theorem42 Γ e t (type6 .Γ e₁ e₂ e₃ .t sts sts₁ sts₂) ∅ G[γ] = - erel (`if e₁ then e₂ else e₃) t helper where - helper : (e′ : term) → ((`if e₁ then e₂ else e₃) ↦∙ e′) × irred e′ → V t e′ - helper e′ ((zero , iter-zero .(`if e₁ then e₂ else e₃)) , snd) = - ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) - helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule1 .(`if e₁ then e₂ else e₃) e2)) , snd) = - ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) - helper e′ ((suc n , iter-suc .n e .(`if e₁ then e₂ else e₃) .(`if e₁ then e₂ else e₃) fst (rule2 e1 .(`if e₁ then e₂ else e₃))) , snd) = - ⊥-elim (snd ((`if e₁ then e₂ else e₃) , rule1 (`if e₁ then e₂ else e₃) e₂)) -theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₁ x₂)) = {! !} -theorem42 Γ e t (type6 .(Γ₁ , x ∶ t₁) e₁ e₂ e₃ .t sts sts₁ sts₂) (γ , x ≔ x₁) (cons Γ₁ .x t₁ .γ .x₁ (inj₂ y)) = {! !} - --- Theorem 4.1: semantic type soundness - -theorem41 : ∀ (e : term) → (t : type) → (∅ ⊢ e ∶ t) → safe e -theorem41 e t ts = goal1 where - swt : ∅ ⊨ e ∶ t - swt = theorem42 ∅ e t ts - - goal2 : E t e - goal2 = swt ∅ nil - - goal1 : safe e - goal1 e′ prf = {! !} \ No newline at end of file diff --git a/src/VanDoornDissertation/HoTT/LongExactSequence.agda b/src/VanDoornDissertation/HoTT/LongExactSequence.agda deleted file mode 100644 index b5c0d2a..0000000 --- a/src/VanDoornDissertation/HoTT/LongExactSequence.agda +++ /dev/null @@ -1,4 +0,0 @@ -{-# OPTIONS --cubical --safe #-} - -module VanDoornDissertation.HoTT.LongExactSequence where - diff --git a/src/VanDoornDissertation/PropTrunc.agda b/src/VanDoornDissertation/PropTrunc.agda deleted file mode 100644 index 55bdba9..0000000 --- a/src/VanDoornDissertation/PropTrunc.agda +++ /dev/null @@ -1,26 +0,0 @@ -{-# OPTIONS --cubical #-} - -module VanDoornDissertation.PropTrunc where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv -open import Cubical.HITs.Truncation -open import Cubical.HITs.PropositionalTruncation - --- Theorem 3.1.8. The map A 7 → {A}∞ satisfies all the properties of the propositional --- truncation ‖−‖, including the universe level and judgmental computation rule on point --- constructors. - -ptrunc-equiv-trunc : {A : Type} → ∥ A ∥₁ ≃ (∥ A ∥ 1) -ptrunc-equiv-trunc {A} = f , record { equiv-proof = eqv } where - f : ∥ A ∥₁ → (∥ A ∥ 1) - f ∣ x ∣₁ = ∣ x ∣ - f (squash₁ x y i) = {! !} - - g : ∥ A ∥ 1 → ∥ A ∥₁ - g ∣ x ∣ = ∣ x ∣₁ - g (hub f₁) = {! !} - g (spoke f₁ x i) = {! !} - - eqv : (y : ∥ A ∥ 1) → isContr (fiber f y) - eqv y = {! !} , {! !} \ No newline at end of file diff --git a/src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda b/src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda deleted file mode 100644 index 8f7d31c..0000000 --- a/src/VanDoornDissertation/Spectral/Algebra/SpectralSequence.agda +++ /dev/null @@ -1,7 +0,0 @@ -{-# OPTIONS --cubical #-} - -module VanDoornDissertation.Spectral.Algebra.SpectralSequence where - -open import Cubical.Foundations.Prelude - -record convergent-spectral-sequence : Type where \ No newline at end of file