From 5cbf679c0c37285fe8f2598fc49367962ca8e58d Mon Sep 17 00:00:00 2001 From: Julius Date: Tue, 21 Apr 2026 20:44:15 +0200 Subject: [PATCH] small work --- SubjectReduction/Confluence.agda | 19 ++++++--- SubjectReduction/ConversionProperties.agda | 49 +++++++++++++++++++--- 2 files changed, 56 insertions(+), 12 deletions(-) diff --git a/SubjectReduction/Confluence.agda b/SubjectReduction/Confluence.agda index 46673de..6ff4e18 100644 --- a/SubjectReduction/Confluence.agda +++ b/SubjectReduction/Confluence.agda @@ -556,6 +556,12 @@ par-triangle (ξ-· (ξ-, l l₁) r) = ξ-· (ξ-, (par-triangle l) (par-triangl par-triangle (ξ-· (ξ-subst t e₁ e₂) r) = ξ-· (par-triangle (ξ-subst t e₁ e₂)) (par-triangle r) par-triangle (ξ-· s@(β-subst l) r) = ξ-· (par-triangle s) (par-triangle r) par-triangle (ξ-· ξ-refl r) = ξ-· ξ-refl (par-triangle r) +par-triangle (ξ-· (ξ-Setω l) r) = ξ-· (ξ-Setω (par-triangle l)) (par-triangle r) +par-triangle (ξ-· (ξ-Setn l) r) = ξ-· (ξ-Setn (par-triangle l)) (par-triangle r) +par-triangle (ξ-· ξ-Level r) = ξ-· ξ-Level (par-triangle r) +par-triangle (ξ-· ξ-lzero r) = ξ-· ξ-lzero (par-triangle r) +par-triangle (ξ-· (ξ-lsuc l) r) = ξ-· (ξ-lsuc (par-triangle l)) (par-triangle r) +par-triangle (ξ-· (ξ-⊔ l l₁) r) = ξ-· (ξ-⊔ (par-triangle l) (par-triangle l₁)) (par-triangle r) par-triangle (β-proj₁ e) = par-triangle e par-triangle (β-proj₂ e) = par-triangle e par-triangle (ξ-proj₁ ξ-`) = ξ-proj₁ ξ-` @@ -607,6 +613,12 @@ par-triangle (ξ-subst e (ξ-, e₁ e₃) e₂) = ξ-subst (par-triangle e) (ξ- par-triangle (ξ-subst e (ξ-subst e₁ e₃ e₄) e₂) = ξ-subst (par-triangle e) (par-triangle (ξ-subst e₁ e₃ e₄)) (par-triangle e₂) par-triangle (ξ-subst e (β-subst e₁) e₂) = ξ-subst (par-triangle e) (par-triangle e₁) (par-triangle e₂) par-triangle (ξ-subst e ξ-refl e₂) = β-subst (par-triangle e₂) +par-triangle (ξ-subst e (ξ-Setω e₁) e₂) = ξ-subst (par-triangle e) (ξ-Setω (par-triangle e₁)) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-Setn e₁) e₂) = ξ-subst (par-triangle e) (ξ-Setn (par-triangle e₁)) (par-triangle e₂) +par-triangle (ξ-subst e ξ-Level e₂) = ξ-subst (par-triangle e) ξ-Level (par-triangle e₂) +par-triangle (ξ-subst e ξ-lzero e₂) = ξ-subst (par-triangle e) ξ-lzero (par-triangle e₂) +par-triangle (ξ-subst e (ξ-lsuc e₁) e₂) = ξ-subst (par-triangle e) (ξ-lsuc (par-triangle e₁)) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-⊔ e₁ e₃) e₂) = ξ-subst (par-triangle e) (ξ-⊔ (par-triangle e₁) (par-triangle e₃)) (par-triangle e₂) par-triangle (ξ-proj₁ (ξ-Setω x)) = ξ-proj₁ (ξ-Setω (par-triangle x)) par-triangle (ξ-proj₁ (ξ-Setn x)) = ξ-proj₁ (ξ-Setn (par-triangle x)) par-triangle (ξ-proj₁ ξ-Level) = ξ-proj₁ ξ-Level @@ -619,18 +631,13 @@ par-triangle (ξ-proj₂ ξ-Level) = ξ-proj₂ ξ-Level par-triangle (ξ-proj₂ ξ-lzero) = ξ-proj₂ (par-triangle ξ-lzero) par-triangle (ξ-proj₂ (ξ-lsuc x)) = ξ-proj₂ (ξ-lsuc (par-triangle x)) par-triangle (ξ-proj₂ (ξ-⊔ x x₁)) = ξ-proj₂ (ξ-⊔ (par-triangle x) (par-triangle x₁)) -par-triangle (ξ-· x x₁) = {! !} -par-triangle (ξ-subst x x₁ x₂) = {! !} +-- New par-triangle (ξ-Setω x) = ξ-Setω (par-triangle x) par-triangle (ξ-Setn x) = ξ-Setn (par-triangle x) par-triangle ξ-Level = ξ-Level par-triangle ξ-lzero = ξ-lzero par-triangle (ξ-lsuc x) = ξ-lsuc (par-triangle x) par-triangle (ξ-⊔ x x₁) = ξ-⊔ (par-triangle x) (par-triangle x₁) --- par-triangle (ξ-proj₁ ξ-Set) = ξ-proj₁ ξ-Set --- par-triangle (ξ-proj₂ ξ-Set) = ξ-proj₂ ξ-Set --- par-triangle (ξ-· ξ-Set r) = ξ-· ξ-Set (par-triangle r) --- par-triangle (ξ-subst e ξ-Set e₂) = ξ-subst (par-triangle e) ξ-Set (par-triangle e₂) 1→* : ∀ {m} {e e' : Term m} → e ↪ₚ e' → (e ↪ₚ* e') 1→* e↪ₚe' = ↪ₚ*-step e↪ₚe' ↪ₚ*-refl diff --git a/SubjectReduction/ConversionProperties.agda b/SubjectReduction/ConversionProperties.agda index 61e6f66..083fcf6 100644 --- a/SubjectReduction/ConversionProperties.agda +++ b/SubjectReduction/ConversionProperties.agda @@ -65,7 +65,6 @@ open import univTypes.Util.Fin → e ↪ₚ* e' --------------- → `proj₂ e ↪ₚ* `proj₂ e' - ξₚ*-proj₂ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₂ (↪ₚ*→↪* e↪ₚ*e')) ξₚ*-· : ∀ {n} {e₁ e₂ e₁' e₂' : Term n} @@ -126,6 +125,15 @@ open import univTypes.Util.Fin ξ-2 = ξ*-subst₃ (↪ₚ*→↪* e₂↪ₚ*e₂') a = ↪*-trans ξ-t ξ-1 b = ↪*-trans a ξ-2 + + +-- New +ξₚ*-Setn : ∀ {n} {e e' : Term n} + → e ↪ₚ* e' + --------------- + → `Setn e ↪ₚ* `Setn e' +ξₚ*-Setn e↪ₚ*e' = {! ↪*→↪ₚ* ? !} +-- ↪*→↪ₚ* (ξ*-Setn (↪ₚ*→↪* e↪ₚ*e')) -------------------------------------------------------------------------------- -- "Substituting two convertible terms into another term, yields again convertible terms." @@ -160,7 +168,6 @@ _≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set ↪ₚ*σ-sub : ∀ {m n} {e : Term m} {σ σ' : Sub m n} → σ ↪ₚ*σ σ' → sub σ e ↪ₚ* sub σ' e -↪ₚ*σ-sub {m} {n} {`Set} {σ} {σ'} σ↪σ' = ↪ₚ*-refl ↪ₚ*σ-sub {m} {n} {`refl} {σ} {σ'} σ↪σ' = ↪ₚ*-refl ↪ₚ*σ-sub {m} {n} {` x} {σ} {σ'} σ↪σ' = σ↪σ' x ↪ₚ*σ-sub {m} {n} {`λ e} {σ} {σ'} σ↪σ' = ξₚ*-λ (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ')) @@ -173,6 +180,12 @@ _≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set ↪ₚ*σ-sub {m} {n} {`proj₂ e} {σ} {σ'} σ↪σ' = ξₚ*-proj₂ (↪ₚ*σ-sub {e = e} (σ↪σ')) ↪ₚ*σ-sub {m} {n} {`subst t e₁ e₂} {σ} {σ'} σ↪σ' = ξₚ*-subst (↪ₚ*σ-sub {e = t} (↪ₚ*σ-ext σ↪σ')) (↪ₚ*σ-sub {e = e₁} σ↪σ') (↪ₚ*σ-sub {e = e₂} σ↪σ') +↪ₚ*σ-sub {m} {n} {`Level} {σ} {σ'} σ↪σ' = ↪ₚ*-refl +↪ₚ*σ-sub {m} {n} {`lzero} {σ} {σ'} σ↪σ' = ↪ₚ*-refl +↪ₚ*σ-sub {m} {n} {`Setω x} {σ} {σ'} σ↪σ' = {! ξₚ*-Setω (↪ₚ*σ-sub {e = e} (σ↪σ') !} +↪ₚ*σ-sub {m} {n} {`Setn x} {σ} {σ'} σ↪σ' = {! !} +↪ₚ*σ-sub {m} {n} {`lsuc x} {σ} {σ'} σ↪σ' = {! !} +↪ₚ*σ-sub {m} {n} {l `⊔ r} {σ} {σ'} σ↪σ' = {! ξₚ*-⊔ (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') !} ↪*σ-sub : ∀ {m n} {e : Term m} {σ σ' : Sub m n} → σ ↪*σ σ' → @@ -190,7 +203,6 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x → σ ≈σ σ' → sub σ e ≈ sub σ' e ≈σ-sub {e = ` x} ≈σ' = ≈σ' x -≈σ-sub {e = `Set} ≈σ' = ≈-refl ≈σ-sub {e = `refl} ≈σ' = ≈-refl ≈σ-sub {e = l · r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ' ... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' @@ -219,6 +231,8 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x | mk-≈ c e₂↪*c e₂'↪*c = mk-≈ (`subst a b c) (↪ₚ*→↪* (ξₚ*-subst (↪*→↪ₚ* t↪*a) (↪*→↪ₚ* e₁↪*b) (↪*→↪ₚ* e₂↪*c))) (↪ₚ*→↪* (ξₚ*-subst (↪*→↪ₚ* t'↪*a) (↪*→↪ₚ* e₁'↪*b) (↪*→↪ₚ* e₂'↪*c))) +≈σ-sub {zero} ≈σ' = {! !} +≈σ-sub {suc e} ≈σ' = {! !} ≈→≈σ : ∀ {n} {e e' : Term n} → e ≈ e' @@ -273,6 +287,12 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x ↪-ren ρ (ξ-subst₁ x) = ξ-subst₁ (↪-ren (extᵣ ρ) x) ↪-ren ρ (ξ-subst₂ x) = ξ-subst₂ (↪-ren ρ x) ↪-ren ρ (ξ-subst₃ x) = ξ-subst₃ (↪-ren ρ x) +-- New +↪-ren ρ (ξ-⊔₁ x) = {! !} +↪-ren ρ (ξ-⊔₂ x) = {! !} +↪-ren ρ (ξ-lsuc x) = {! !} +↪-ren ρ (ξ-Setn x) = {! !} +↪-ren ρ (ξ-Setω x) = {! !} -- Renaming preserves many reduction steps @@ -314,7 +334,13 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x ↪-sub σ (ξ-≡₂ x) = ξ-≡₂ (↪-sub σ x) ↪-sub σ (ξ-subst₁ x) = ξ-subst₁ (↪-sub (extₛ σ) x) ↪-sub σ (ξ-subst₂ x) = ξ-subst₂ (↪-sub σ x) -↪-sub σ (ξ-subst₃ x) = ξ-subst₃ (↪-sub σ x) +-- New +↪-sub σ (ξ-⊔₁ x) = {! !} +↪-sub σ (ξ-⊔₂ x) = {! !} +↪-sub σ (ξ-lsuc x) = {! !} +↪-sub σ (ξ-Setn x) = {! !} +↪-sub σ (ξ-subst₃ x) = {! !} +↪-sub σ (ξ-Setω x) = {! !} -- Substitution preserves many reduction steps @@ -363,19 +389,24 @@ _≈ᶜ_ : ∀ {n} → Context n → Context n → Set ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂) -≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Set = ⊢-Set ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≈ x ⊢e) = ⊢-≈ x (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-proj₁ ⊢e) = ⊢-proj₁ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-proj₂ ⊢e) = ⊢-proj₂ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-refl ⊢e) = ⊢-refl (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e) ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-subst t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁]) = ⊢-subst (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) t'⊢t) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₁) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₂) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢≡) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢t[u₁]) +-- New +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setn = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setω = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-lzero = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-lsuc ⊢x) = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-⊔ ⊢x ⊢x₁) = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Level = {! !} ≈-Γ-⊢₁ : ∀ {n} {Γ : Context n} {t₁ t₂ : Term n} {e t : Term (suc n)} → t₁ ≈ t₂ → Γ , t₁ ⊢ e ⦂ t → Γ , t₂ ⊢ e ⦂ t -≈-Γ-⊢₁ t₁≈t₂ ⊢-Set = ⊢-Set ≈-Γ-⊢₁ t₁≈t₂ (⊢-refl e) = ⊢-refl (≈-Γ-⊢₁ t₁≈t₂ e) ≈-Γ-⊢₁ t₁≈t₂ (⊢-` x refl) = ⊢-≈ (≈-ext (λ _ → ≈-refl) (≈-sym t₁≈t₂) x) (⊢-` x refl ) ≈-Γ-⊢₁ t₄≈t₂ (⊢-λ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-λ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁) ((≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃)) @@ -393,3 +424,9 @@ _≈ᶜ_ : ∀ {n} → Context n → Context n → Set (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₂) (≈-Γ-⊢₁ t₁≈t₂ t₁⊢≡) (≈-Γ-⊢₁ t₁≈t₂ t₁⊢t[u₁]) +≈-Γ-⊢₁ t₁≈t₂ ⊢-Setn = {! !} +≈-Γ-⊢₁ t₁≈t₂ ⊢-Setω = {! !} +≈-Γ-⊢₁ t₁≈t₂ ⊢-lzero = {! !} +≈-Γ-⊢₁ t₁≈t₂ (⊢-lsuc ⊢x) = {! !} +≈-Γ-⊢₁ t₁≈t₂ (⊢-⊔ ⊢x ⊢x₁) = {! !} +≈-Γ-⊢₁ t₁≈t₂ ⊢-Level = {! !}