diff --git a/README.md b/README.md index e872aa4..765cd67 100644 --- a/README.md +++ b/README.md @@ -6,4 +6,4 @@ including my progress into research for my master's degree. Links: -- [my current focus](https://git.mzhang.io/school/cubical/projects/2) +- [my current focus](https://git.mzhang.io/michael/type-theory/projects/8) diff --git a/src/CEKCoinductive.agda b/src/CEKCoinductive.agda deleted file mode 100644 index 42cf38f..0000000 --- a/src/CEKCoinductive.agda +++ /dev/null @@ -1,22 +0,0 @@ -{-# OPTIONS --guardedness #-} - -module CEKCoinductive where - -open import Agda.Primitive - -private - variable - l l1 l2 l3 : Level - - E : Set → Set - R : Set - -data ITreeF (ITree : Set) : Set where - Ret : (r : R) → ITreeF ITree - Tau : (t : ITree) → ITreeF ITree - Vis : {A : Set l1} → (e : E A) → (k : A → ITreeF E R) → ITreeF E R - -record ITree : Set where - coinductive - field - _observe : ITreeF ITree \ No newline at end of file diff --git a/src/CubicalHott/Exercise4-6.agda b/src/CubicalHott/Exercise4-6.agda new file mode 100644 index 0000000..9e63f7f --- /dev/null +++ b/src/CubicalHott/Exercise4-6.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.Exercise4-6 where + +open import Cubical.Core.Glue +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Transport + +variable + l : Level + A B : Type + +idtoqinv : A ≡ B → Iso A B +idtoqinv {A} {B} p = iso (transport p) (transport (sym p)) s r where + s : section (transport p) (transport (λ i → p (~ i))) + s b = sym (transportComposite (sym p) p b) ∙ cong (λ p → transport p b) (rCancel (sym p)) ∙ transportRefl b + + r : retract (transport p) (transport (λ i → p (~ i))) + r a = sym (transportComposite p (sym p) a) ∙ cong (λ p → transport p a) (rCancel p) ∙ transportRefl a + +postulate + idtoqinv-← : Iso A B → A ≡ B diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda index 992af06..3302b93 100644 --- a/src/CubicalHott/Theorem7-1-11.agda +++ b/src/CubicalHott/Theorem7-1-11.agda @@ -12,14 +12,7 @@ open import Cubical.Data.Nat open import Data.Unit lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) -lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {! !} where - -- G : A ≡ B - -- G = ua (isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)) - - -- g : PathP (λ i → G i) a b - -- g = {! !} - - -- contr : Acontr ≡ Bcontr +lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where eqv1 : A ≃ B eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) @@ -31,7 +24,11 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , {! !} where g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b contr : (y : G) → g ≡ y - contr y j = {! !} + contr y j = + let p = λ where + (i = i0) → Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j + (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j + in glue p {! b !} -- unglue i {! !} -- (glue (λ { (i = i1) → {! !} }) {! !}) diff --git a/src/Log.lagda.md b/src/Log.lagda.md deleted file mode 100644 index ca40feb..0000000 --- a/src/Log.lagda.md +++ /dev/null @@ -1,60 +0,0 @@ -``` -{-# OPTIONS --cubical #-} - -module Log where - -open import Cubical.Foundations.Prelude -``` - -## 2024-09-12 - -Trying to get hcomp to work - -``` -module log-20240912 where - private - variable - l : Level - A : Type l - x y z w : A - p : x ≡ y - q : y ≡ z - r : z ≡ w - s : w ≡ x - - -- Order of the square is - -- 4 - -- +----->+ - -- ^ ^ - -- 1 | | 2 - -- | | - -- +----->+ - -- 3 - -- In this below case, i is the vertical dimension and j is the horizontal dimension - test-square : Square refl refl p p - test-square {l} {A} {x} {y} {p} i j = p i - - -- Creating the same square with hfill - test-square2 : p ∙ refl ≡ p - test-square2 {l} {A} {x} {y} {p} i j = hfill (λ k → λ where - (j = i0) → x - (j = i1) → y - ) - -- A [ ~ j ∨ j ↦ (λ { (j = i0) → x ; (j = i1) → y }) ] - -- looking for some expression s.t when φ = i1, will equal the thing in the expression - (inS (p j)) - (~ i) - - -- Trying to port over the 1lab filler - -- This fills a square - ∙∙-filler : Square s q p (sym s ∙∙ p ∙∙ q) - ∙∙-filler {l} {A} {x} {y} {z} {w} {p} {q} {s} i j = hfill (λ k → λ where - (j = i0) → {! s (~ i) !} - (j = i1) → {! !} - ) - {! !} {! i !} -``` - -Question: -- How many sides do you need for the hcomp to be correct? -- What direction, semantically, is the last argument to hfill? \ No newline at end of file diff --git a/src/LogRel.agda b/src/LogRel.agda new file mode 100644 index 0000000..8b5e668 --- /dev/null +++ b/src/LogRel.agda @@ -0,0 +1,200 @@ +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