diff --git a/SubjectReduction/Composition.agda b/SubjectReduction/Composition.agda new file mode 100644 index 0000000..aa52584 --- /dev/null +++ b/SubjectReduction/Composition.agda @@ -0,0 +1,287 @@ +module univTypes.SubjectReduction.Composition where + +open import Data.Product +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning) +open import Data.Fin using (zero; suc) renaming (Fin to 𝔽) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.SubjectReduction.Specification +open import univTypes.Util.Fin + +-------------------------------------------------------------------------------- + +-- Composition of two renamings + +_∘ᵣᵣ_ : ∀ {n₁ n₂ n₃} → Ren n₂ n₃ → Ren n₁ n₂ → Ren n₁ n₃ +(ρ₁ ∘ᵣᵣ ρ₂) x = ρ₁ (ρ₂ x) + +ext-dist-∘ᵣᵣ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (ρ₂ : Ren n₁ n₂) + → extᵣ (ρ₁ ∘ᵣᵣ ρ₂) ≡ (extᵣ ρ₁) ∘ᵣᵣ (extᵣ ρ₂) +ext-dist-∘ᵣᵣ ρ₁ ρ₂ = fun-ext eq + where + eq : ∀ {n₁ n₂ n₃} {ρ₁ : Ren n₂ n₃} {ρ₂ : Ren n₁ n₂} + → (x : Fin (suc n₁)) → extᵣ (ρ₁ ∘ᵣᵣ ρ₂) x ≡ (extᵣ ρ₁ ∘ᵣᵣ extᵣ ρ₂) x + eq zero = refl + eq (suc x) = refl + + +fusion-∘ᵣᵣ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁) + → ren ρ₁ (ren ρ₂ e) ≡ ren (ρ₁ ∘ᵣᵣ ρ₂) e +fusion-∘ᵣᵣ ρ₁ ρ₂ (` x) = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ `Set = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ `refl = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (∀[x⦂ x ] e) + rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ x | (fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e) | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (l · r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`λ e) rewrite fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (∃[x⦂ x ] e) + rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ x | fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (l `, r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`proj₁ e) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ e = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`proj₂ e) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ e = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (l `≡ r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`subst t e₁ e₂) + rewrite fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) t | fusion-∘ᵣᵣ ρ₁ ρ₂ e₁ | fusion-∘ᵣᵣ ρ₁ ρ₂ e₂ | ext-dist-∘ᵣᵣ ρ₁ ρ₂ + = refl + +wk-extᵣ : ∀ {m n} (ρ : Ren m n) + → wk ∘ᵣᵣ ρ ≡ extᵣ ρ ∘ᵣᵣ wk +wk-extᵣ ρ = refl +open import Relation.Binary.PropositionalEquality using (trans) +wk-extᵣ-fusion : ∀ {m n} (ρ : Ren m n) (e : Term m) + → ren wk (ren ρ e) ≡ ren (extᵣ ρ) (ren wk e) +wk-extᵣ-fusion ρ e = trans (fusion-∘ᵣᵣ wk ρ e) (trans (cong (λ x → ren x e ) (wk-extᵣ ρ)) (sym (fusion-∘ᵣᵣ (extᵣ ρ) wk e))) + +-------------------------------------------------------------------------------- + +-- Composition of a substitution and a renaming + +_∘ₛᵣ_ : ∀ {n₁ n₂ n₃} → Sub n₂ n₃ → Ren n₁ n₂ → Sub n₁ n₃ +(σ₁ ∘ₛᵣ ρ₂) x = σ₁ (ρ₂ x) + +ext-dist-∘ₛᵣ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (ρ₂ : Ren n₁ n₂) + → extₛ (σ₁ ∘ₛᵣ ρ₂) ≡ (extₛ σ₁) ∘ₛᵣ (extᵣ ρ₂) +ext-dist-∘ₛᵣ _ _ = fun-ext λ{zero → refl; (suc x) → refl } + +fusion-∘ₛᵣ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁) + → sub σ₁ (ren ρ₂ e) ≡ sub (σ₁ ∘ₛᵣ ρ₂) e +fusion-∘ₛᵣ σ ρ (` x) = refl +fusion-∘ₛᵣ σ ρ `Set = refl +fusion-∘ₛᵣ σ ρ `refl = refl +fusion-∘ₛᵣ σ ρ (`λ e) rewrite fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e | ext-dist-∘ₛᵣ σ ρ = refl +fusion-∘ₛᵣ σ ρ (l · r) rewrite fusion-∘ₛᵣ σ ρ l | fusion-∘ₛᵣ σ ρ r = refl +fusion-∘ₛᵣ σ ρ (∀[x⦂ x ] e) rewrite fusion-∘ₛᵣ σ ρ x + | fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e + | ext-dist-∘ₛᵣ σ ρ = refl +fusion-∘ₛᵣ σ ρ (∃[x⦂ x ] e) rewrite fusion-∘ₛᵣ σ ρ x + | fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e + | ext-dist-∘ₛᵣ σ ρ = refl +fusion-∘ₛᵣ σ ρ (l `, r) rewrite fusion-∘ₛᵣ σ ρ l | fusion-∘ₛᵣ σ ρ r = refl +fusion-∘ₛᵣ σ ρ (l `≡ r) rewrite fusion-∘ₛᵣ σ ρ l | fusion-∘ₛᵣ σ ρ r = refl +fusion-∘ₛᵣ σ ρ (`proj₁ e) rewrite fusion-∘ₛᵣ σ ρ e = refl +fusion-∘ₛᵣ σ ρ (`proj₂ e) rewrite fusion-∘ₛᵣ σ ρ e = refl +fusion-∘ₛᵣ σ ρ (`subst t e₁ e₂) + rewrite fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) t | fusion-∘ₛᵣ σ ρ e₁ + | fusion-∘ₛᵣ σ ρ e₂ | ext-dist-∘ₛᵣ σ ρ + = refl +-------------------------------------------------------------------------------- + +-- Composition of a renaming and a substitution + +_∘ᵣₛ_ : ∀ {n₁ n₂ n₃} → Ren n₂ n₃ → Sub n₁ n₂ → Sub n₁ n₃ +(ρ₁ ∘ᵣₛ σ₂) x = ren ρ₁ (σ₂ x) + +suc' : ∀ {n} → (x : Fin n) → Fin (suc n) +suc' x = suc x + +fun-ext-aux₁ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) (x : Fin (suc n₁)) + + → extₛ (ρ₁ ∘ᵣₛ σ₂) x ≡ (extᵣ ρ₁ ∘ᵣₛ extₛ σ₂) x +fun-ext-aux₁ ρ σ zero = refl +fun-ext-aux₁ ρ σ (suc x) = + extₛ (ρ ∘ᵣₛ σ) (suc x) + ≡⟨ refl ⟩ + ren suc' (ren ρ (σ x)) + ≡⟨ fusion-∘ᵣᵣ suc' ρ (σ x) ⟩ + ren (suc' ∘ᵣᵣ ρ) (σ x) + ≡⟨ refl ⟩ + ren (extᵣ ρ ∘ᵣᵣ suc') (σ x) + ≡⟨ sym (fusion-∘ᵣᵣ (extᵣ ρ) suc' (σ x)) ⟩ + ren (extᵣ ρ) (ren suc' (σ x)) + ≡⟨ refl ⟩ + ((extᵣ ρ ∘ᵣₛ extₛ σ) (suc x)) ∎ + where open ≡-Reasoning + +ext-dist-∘ᵣₛ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) + → extₛ (ρ₁ ∘ᵣₛ σ₂) ≡ (extᵣ ρ₁) ∘ᵣₛ (extₛ σ₂) +ext-dist-∘ᵣₛ ρ σ = fun-ext (fun-ext-aux₁ ρ σ) + +fusion-∘ᵣₛ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁) + → ren ρ₁ (sub σ₂ e) ≡ sub (ρ₁ ∘ᵣₛ σ₂) e +fusion-∘ᵣₛ ρ σ (` x) = refl +fusion-∘ᵣₛ ρ σ `Set = refl +fusion-∘ᵣₛ ρ σ `refl = refl +fusion-∘ᵣₛ ρ σ (`λ e) rewrite fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e + | ext-dist-∘ᵣₛ ρ σ = refl +fusion-∘ᵣₛ ρ σ (l · r) rewrite fusion-∘ᵣₛ ρ σ l + | fusion-∘ᵣₛ ρ σ r = refl +fusion-∘ᵣₛ ρ σ (∀[x⦂ x ] e) rewrite fusion-∘ᵣₛ ρ σ x + | fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e + | ext-dist-∘ᵣₛ ρ σ = refl +fusion-∘ᵣₛ ρ σ (∃[x⦂ x ] e) rewrite fusion-∘ᵣₛ ρ σ x + | fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e + | ext-dist-∘ᵣₛ ρ σ = refl +fusion-∘ᵣₛ ρ σ (l `, r) rewrite fusion-∘ᵣₛ ρ σ l + | fusion-∘ᵣₛ ρ σ r = refl +fusion-∘ᵣₛ ρ σ (l `≡ r) rewrite fusion-∘ᵣₛ ρ σ l + | fusion-∘ᵣₛ ρ σ r = refl +fusion-∘ᵣₛ ρ σ (`proj₁ e) rewrite fusion-∘ᵣₛ ρ σ e = refl +fusion-∘ᵣₛ ρ σ (`proj₂ e) rewrite fusion-∘ᵣₛ ρ σ e = refl +fusion-∘ᵣₛ ρ σ (`subst t e₁ e₂) rewrite fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) t + | fusion-∘ᵣₛ ρ σ e₁ | fusion-∘ᵣₛ ρ σ e₂ + | ext-dist-∘ᵣₛ ρ σ = refl + +wk-extₛ : ∀ {m n} (σ : Sub m n) + → wk ∘ᵣₛ σ ≡ extₛ σ ∘ₛᵣ wk +wk-extₛ σ = refl + +wk-extₛ-fusion : ∀ {m n} (σ : Sub m n) (e : Term m) + → ren wk (sub σ e) ≡ sub (extₛ σ) (ren wk e) +wk-extₛ-fusion σ e = trans (fusion-∘ᵣₛ wk σ e) (trans (cong (λ x → sub x e) (wk-extₛ σ)) (sym (fusion-∘ₛᵣ (extₛ σ) wk e))) +-------------------------------------------------------------------------------- + +-- Composition of two substitutions + +_∘ₛₛ_ : ∀ {n₁ n₂ n₃} → Sub n₂ n₃ → Sub n₁ n₂ → Sub n₁ n₃ +(σ₁ ∘ₛₛ σ₂) x = sub σ₁ (σ₂ x) + + +fun-ext-aux₂ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) (x : Fin (suc n₁)) + → extₛ (σ₁ ∘ₛₛ σ₂) x ≡ (extₛ σ₁ ∘ₛₛ extₛ σ₂) x +fun-ext-aux₂ _ _ zero = refl +fun-ext-aux₂ σ₁ σ₂ (suc x) = + ren suc' (sub σ₁ (σ₂ x)) + ≡⟨ fusion-∘ᵣₛ suc' σ₁ (σ₂ x) ⟩ + sub (suc' ∘ᵣₛ σ₁) (σ₂ x) + ≡⟨ sym (fusion-∘ᵣₛ suc' σ₁ (σ₂ x)) ⟩ + ren wk (sub σ₁ (σ₂ x)) + ≡⟨ wk-extₛ-fusion σ₁ (σ₂ x) ⟩ + sub (extₛ σ₁) (ren wk (σ₂ x)) ≡⟨ refl ⟩ + (sub (extₛ σ₁) (ren suc' (σ₂ x))) ∎ + where open ≡-Reasoning + +ext-dist-∘ₛₛ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) + → extₛ (σ₁ ∘ₛₛ σ₂) ≡ (extₛ σ₁) ∘ₛₛ (extₛ σ₂) +ext-dist-∘ₛₛ σ₁ σ₂ = fun-ext (fun-ext-aux₂ σ₁ σ₂) + +fusion-∘ₛₛ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁) + → sub σ₁ (sub σ₂ e) ≡ sub (σ₁ ∘ₛₛ σ₂) e +fusion-∘ₛₛ σ₁ σ₂ (` x) = refl +fusion-∘ₛₛ σ₁ σ₂ `Set = refl +fusion-∘ₛₛ σ₁ σ₂ `refl = refl +fusion-∘ₛₛ σ₁ σ₂ (`λ e) rewrite fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) e | ext-dist-∘ₛₛ σ₁ σ₂ = refl +fusion-∘ₛₛ σ₁ σ₂ (l · r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl +fusion-∘ₛₛ σ₁ σ₂ (l `≡ r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl +fusion-∘ₛₛ σ₁ σ₂ (l `, r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl +fusion-∘ₛₛ σ₁ σ₂ (∀[x⦂ x ] t) rewrite fusion-∘ₛₛ σ₁ σ₂ x | fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t | ext-dist-∘ₛₛ σ₁ σ₂ = refl +fusion-∘ₛₛ σ₁ σ₂ (∃[x⦂ x ] t) rewrite fusion-∘ₛₛ σ₁ σ₂ x | fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t | ext-dist-∘ₛₛ σ₁ σ₂ = refl +fusion-∘ₛₛ σ₁ σ₂ (`proj₁ e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl +fusion-∘ₛₛ σ₁ σ₂ (`proj₂ e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl +fusion-∘ₛₛ σ₁ σ₂ (`subst t e₁ e₂) rewrite fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) t + | fusion-∘ₛₛ σ₁ σ₂ e₁ + | fusion-∘ₛₛ σ₁ σ₂ e₂ + | ext-dist-∘ₛₛ σ₁ σ₂ = refl + +-----{! !}-------------------------------------------------------------------------- + +-- Identity substitution does nothing + +idₛ : ∀ {n} → Sub n n +idₛ x = ` x + +extₛ-idₛ : ∀ {n} → + extₛ (idₛ {n}) ≡ idₛ {suc n} +extₛ-idₛ {n} = fun-ext λ{zero → refl; (suc x) → refl} + +sub-id : ∀ {n} (e : Term n) + → sub idₛ e ≡ e +sub-id (` x) = refl +sub-id `Set = refl +sub-id `refl = refl +sub-id (`λ e) = cong (λ a → `λ a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e)) +sub-id (`proj₁ e) = cong (λ a → `proj₁ a) (trans (cong (λ a → sub a e) refl) (sub-id e)) +sub-id (`proj₂ e) = cong (λ a → `proj₂ a) (trans (cong (λ a → sub a e) refl) (sub-id e)) +sub-id (l · r) rewrite sub-id l | sub-id r = refl +sub-id (l `≡ r) rewrite sub-id l | sub-id r = refl +sub-id (l `, r) rewrite sub-id l | sub-id r = refl +sub-id (∀[x⦂ x ] e) rewrite sub-id x = cong (λ a → ∀[x⦂ x ] a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e)) +sub-id (∃[x⦂ x ] e) rewrite sub-id x = cong (λ a → ∃[x⦂ x ] a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e)) +sub-id (`subst t e₁ e₂) rewrite sub-id e₁ | sub-id e₂ + = cong (λ a → `subst a e₁ e₂) (trans (cong (λ a → sub a t) extₛ-idₛ) (sub-id t)) + +-------------------------------------------------------------------------------- + +-- Weakening cancels singleton-substitution + +wk-0↦ : ∀ {n} (e : Term n) + → 0↦ e ∘ₛᵣ wk ≡ idₛ +wk-0↦ e = refl + +wk-0↦-fusion : ∀ {n} (e : Term n) (e' : Term n) + → sub (0↦ e) (ren wk e') ≡ e' +wk-0↦-fusion e e' = trans (fusion-∘ₛᵣ (0↦ e) wk e') (trans (cong (λ a → sub a e') (wk-0↦ e)) (sub-id e')) + +-------------------------------------------------------------------------------- + +-- Swap singleton-substitution with renaming + +swap-0↦-extᵣ : ∀ {m n} (ρ : Ren m n) (e : Term m) + → (0↦ (ren ρ e)) ∘ₛᵣ (extᵣ ρ) ≡ ρ ∘ᵣₛ (0↦ e) +swap-0↦-extᵣ ρ e = fun-ext λ{zero → refl; (suc x) → refl} + +swap-0↦-extᵣ-fusion : ∀ {m n} (ρ : Ren m n) (e : Term m) (e' : Term (suc m)) + → sub (0↦ (ren ρ e)) (ren (extᵣ ρ) e') ≡ ren ρ (sub (0↦ e) e') +swap-0↦-extᵣ-fusion ρ e e' = trans (fusion-∘ₛᵣ (0↦ (ren ρ e)) (extᵣ ρ) e') + (trans (cong (λ a → sub a e') (swap-0↦-extᵣ ρ e)) + (sym (fusion-∘ᵣₛ ρ (0↦ e) e'))) + +-- Swap singleton-substitution with substitution + +fun-ext-aux₃ : ∀ {m n} (σ : Sub m n) (e : Term m) (x : _) + → ((0↦ (sub σ e)) ∘ₛₛ (extₛ σ)) x ≡ (σ ∘ₛₛ (0↦ e)) x +fun-ext-aux₃ σ e zero = refl +fun-ext-aux₃ σ e (suc x) = + sub (0↦ (sub σ e)) (ren suc' (σ x)) + ≡⟨ cong (sub (0↦ (sub σ e))) (sym (sub-id (ren suc' (σ x)))) ⟩ + sub (0↦ (sub σ e)) (sub idₛ (ren suc' (σ x))) + ≡⟨ fusion-∘ₛₛ (0↦ (sub σ e)) idₛ (ren suc' (σ x)) ⟩ + sub (0↦ (sub σ e) ∘ₛₛ idₛ) (ren suc' (σ x)) + ≡⟨ refl ⟩ + sub (0↦ (sub σ e)) (ren suc' (σ x)) + ≡⟨ fusion-∘ₛᵣ (0↦ (sub σ e)) suc' (σ x) ⟩ + sub ((0↦ (sub σ e)) ∘ₛᵣ suc') (σ x) + ≡⟨ refl ⟩ + sub idₛ (σ x) + ≡⟨ sub-id _ ⟩ + (σ x) ∎ + where open ≡-Reasoning + +swap-0↦-extₛ : ∀ {m n} (σ : Sub m n) (e : Term m) + → (0↦ (sub σ e)) ∘ₛₛ (extₛ σ) ≡ σ ∘ₛₛ (0↦ e) +swap-0↦-extₛ σ e = fun-ext (fun-ext-aux₃ σ e) + +swap-0↦-extₛ-fusion : ∀ {m n} (σ : Sub m n) (e : Term m) (e' : Term (suc m)) + → sub (0↦ (sub σ e)) (sub (extₛ σ) e') ≡ sub σ (sub (0↦ e) e') +swap-0↦-extₛ-fusion σ e e' = + sub (0↦ (sub σ e)) (sub (extₛ σ) e') + ≡⟨ fusion-∘ₛₛ (0↦ (sub σ e)) (extₛ σ) e' ⟩ + sub (0↦ (sub σ e) ∘ₛₛ extₛ σ) e' + ≡⟨ cong (λ a → sub a e') (swap-0↦-extₛ σ e) ⟩ + sub (σ ∘ₛₛ 0↦ e) e' + ≡⟨ sym (fusion-∘ₛₛ σ (0↦ e) e') ⟩ + sub σ (sub (0↦ e) e') ∎ + where open ≡-Reasoning diff --git a/SubjectReduction/Confluence.agda b/SubjectReduction/Confluence.agda new file mode 100644 index 0000000..ac29565 --- /dev/null +++ b/SubjectReduction/Confluence.agda @@ -0,0 +1,569 @@ +module univTypes.SubjectReduction.Confluence where + +open import Data.Product renaming (_,_ to ⟨_,_⟩) +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning; trans) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.SubjectReduction.Specification +open import univTypes.SubjectReduction.Composition using (swap-0↦-extᵣ-fusion; swap-0↦-extₛ-fusion) +open import univTypes.Util.Fin using (Fin; zero; suc) + +-------------------------------------------------------------------------------- + +-- Congruency rules, but using ↪* instead of ↪ + +ξ*-λ : ∀ {n} {e e' : Term (suc n)} + → e ↪* e' + --------------- + → `λ e ↪* `λ e' +ξ*-λ ↪*-refl = ↪*-refl +ξ*-λ (↪*-step x e↪*e') = ↪*-step (ξ-λ x) (ξ*-λ e↪*e') + +ξ*-·₁ : ∀ {n} {e₁ e₂ e₁' : Term n} + → e₁ ↪* e₁' + --------------------- + → e₁ · e₂ ↪* e₁' · e₂ +ξ*-·₁ ↪*-refl = ↪*-refl +ξ*-·₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-·₁ ↪) (ξ*-·₁ ↪*) + +ξ*-·₂ : ∀ {n} {e₁ e₂ e₂' : Term n} + → e₂ ↪* e₂' + --------------------- + → e₁ · e₂ ↪* e₁ · e₂' +ξ*-·₂ ↪*-refl = ↪*-refl +ξ*-·₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-·₂ ↪) (ξ*-·₂ ↪*) + +ξ*-≡₁ : ∀ {n} {e₁ e₂ e₁' : Term n} + → e₁ ↪* e₁' + --------------------- + → e₁ `≡ e₂ ↪* e₁' `≡ e₂ +ξ*-≡₁ ↪*-refl = ↪*-refl +ξ*-≡₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-≡₁ ↪) (ξ*-≡₁ ↪*) + +ξ*-≡₂ : ∀ {n} {e₁ e₂ e₂' : Term n} + → e₂ ↪* e₂' + --------------------- + → e₁ `≡ e₂ ↪* e₁ `≡ e₂' +ξ*-≡₂ ↪*-refl = ↪*-refl +ξ*-≡₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-≡₂ ↪) (ξ*-≡₂ ↪*) + +ξ*-,₁ : ∀ {n} {e₁ e₂ e₁' : Term n} + → e₁ ↪* e₁' + --------------------- + → e₁ `, e₂ ↪* e₁' `, e₂ +ξ*-,₁ ↪*-refl = ↪*-refl +ξ*-,₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-,₁ ↪) (ξ*-,₁ ↪*) + +ξ*-,₂ : ∀ {n} {e₁ e₂ e₂' : Term n} + → e₂ ↪* e₂' + --------------------- + → e₁ `, e₂ ↪* e₁ `, e₂' +ξ*-,₂ ↪*-refl = ↪*-refl +ξ*-,₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-,₂ ↪) (ξ*-,₂ ↪*) + + +ξ*-∀₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)} + → t₁ ↪* t₁' + ------------------------------- + → ∀[x⦂ t₁ ] t₂ ↪* ∀[x⦂ t₁' ] t₂ +ξ*-∀₁ ↪*-refl = ↪*-refl +ξ*-∀₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-∀₁ ↪) (ξ*-∀₁ ↪*) + +ξ*-∀₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)} + → t₂ ↪* t₂' + ------------------------------- + → ∀[x⦂ t₁ ] t₂ ↪* ∀[x⦂ t₁ ] t₂' +ξ*-∀₂ ↪*-refl = ↪*-refl +ξ*-∀₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-∀₂ ↪) (ξ*-∀₂ ↪*) + +ξ*-∃₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)} + → t₁ ↪* t₁' + ------------------------------- + → ∃[x⦂ t₁ ] t₂ ↪* ∃[x⦂ t₁' ] t₂ +ξ*-∃₁ ↪*-refl = ↪*-refl +ξ*-∃₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-∃₁ ↪) (ξ*-∃₁ ↪*) + +ξ*-∃₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)} + → t₂ ↪* t₂' + ------------------------------- + → ∃[x⦂ t₁ ] t₂ ↪* ∃[x⦂ t₁ ] t₂' +ξ*-∃₂ ↪*-refl = ↪*-refl +ξ*-∃₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-∃₂ ↪) (ξ*-∃₂ ↪*) + +ξ*-proj₁ : ∀ {n} {x x' : Term n} + → x ↪* x' + ------------------------------- + → `proj₁ x ↪* `proj₁ x' +ξ*-proj₁ ↪*-refl = ↪*-refl +ξ*-proj₁ (↪*-step x ↪*) = ↪*-step (ξ-proj₁ x) (ξ*-proj₁ ↪*) + +ξ*-proj₂ : ∀ {n} {x x' : Term n} + → x ↪* x' + ------------------------------- + → `proj₂ x ↪* `proj₂ x' +ξ*-proj₂ ↪*-refl = ↪*-refl +ξ*-proj₂ (↪*-step x ↪*) = ↪*-step (ξ-proj₂ x) (ξ*-proj₂ ↪*) + +ξ*-subst₁ : ∀ {n} {t t' : Term (suc n)} {e₁ e₂ : Term n} + → t ↪* t' + ------------------------------- + → `subst t e₁ e₂ ↪* `subst t' e₁ e₂ +ξ*-subst₁ ↪*-refl = ↪*-refl +ξ*-subst₁ (↪*-step ↪ ↪*) = ↪*-step (ξ-subst₁ ↪) (ξ*-subst₁ ↪* ) + +ξ*-subst₂ : ∀ {n} {t : Term (suc n)} {e₁ e₁' e₂ : Term n} + → e₁ ↪* e₁' + ------------------------------- + → `subst t e₁ e₂ ↪* `subst t e₁' e₂ +ξ*-subst₂ ↪*-refl = ↪*-refl +ξ*-subst₂ (↪*-step ↪ ↪*) = ↪*-step (ξ-subst₂ ↪) (ξ*-subst₂ ↪* ) + +ξ*-subst₃ : ∀ {n} {t : Term (suc n)} {e₁ e₂ e₂' : Term n} + → e₂ ↪* e₂' + ------------------------------- + → `subst t e₁ e₂ ↪* `subst t e₁ e₂' +ξ*-subst₃ ↪*-refl = ↪*-refl +ξ*-subst₃ (↪*-step ↪ ↪*) = ↪*-step (ξ-subst₃ ↪) (ξ*-subst₃ ↪* ) +-------------------------------------------------------------------------------- +-- Parallel Reduction + +infix 3 _↪ₚ_ +data _↪ₚ_ : ∀ {n} → Term n → Term n → Set where + ξ-` : ∀ {n} {x : Fin n} → + ` x ↪ₚ ` x + β-proj₁ : ∀ {n} {x x' a : Term n} → + x ↪ₚ x' → + `proj₁ ( x `, a ) ↪ₚ x' + β-proj₂ : ∀ {n} {x x' a : Term n} → + x ↪ₚ x' → + `proj₂ ( a `, x ) ↪ₚ x' + ξ-proj₁ : ∀ {n} {x x' : Term n} → + x ↪ₚ x' → + `proj₁ x ↪ₚ `proj₁ x' + ξ-proj₂ : ∀ {n} {x x' : Term n} → + x ↪ₚ x' → + `proj₂ x ↪ₚ `proj₂ x' + β-λ : ∀ {n} {e₁ e₁' : Term (suc n)} {e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + (`λ e₁) · e₂ ↪ₚ e₁' [ e₂' ] + ξ-λ : ∀ {n} {e e' : Term (suc n)} → + e ↪ₚ e' → + `λ e ↪ₚ `λ e' + ξ-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} → + t₁ ↪ₚ t₁' → + t₂ ↪ₚ t₂' → + ∀[x⦂ t₁ ] t₂ ↪ₚ ∀[x⦂ t₁' ] t₂' + ξ-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} → + t₁ ↪ₚ t₁' → + t₂ ↪ₚ t₂' → + ∃[x⦂ t₁ ] t₂ ↪ₚ ∃[x⦂ t₁' ] t₂' + ξ-· : ∀ {n} {e₁ e₁' e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + e₁ · e₂ ↪ₚ e₁' · e₂' + ξ-≡ : ∀ {n} {e₁ e₁' e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + e₁ `≡ e₂ ↪ₚ e₁' `≡ e₂' + ξ-, : ∀ {n} {e₁ e₁' e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + e₁ `, e₂ ↪ₚ e₁' `, e₂' + ξ-subst : ∀ {n} {e₁ e₁' e₂ e₂' : Term n} {t t' : Term (suc n)} → + t ↪ₚ t' → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + `subst t e₁ e₂ ↪ₚ `subst t' e₁' e₂' + β-subst : ∀ {n} {t : Term (suc n)} {e e' : Term n} + → e ↪ₚ e' + → `subst t `refl e ↪ₚ e' + ξ-Set : ∀ {n} → + `Set ↪ₚ (`Set {n = n}) + ξ-refl : ∀ {n} → + `refl ↪ₚ (`refl {n = n}) + +↪ₚ₁ : ∀ {n} {fst snd : Term n} → (fst ↪ₚ snd) → Term n +↪ₚ₁ {n} {fst} {snd} _ = fst + +↪ₚ₂ : ∀ {n} {fst snd : Term n} → (fst ↪ₚ snd) → Term n +↪ₚ₂ {n} {fst} {snd} _ = snd +-------------------------------------------------------------------------------- + +-- Reflexive, transitive closure of parallel reduction + +infix 3 _↪ₚ*_ +data _↪ₚ*_ : ∀ {n} → Term n → Term n → Set where + ↪ₚ*-refl : ∀ {n} {e : Term n} + → e ↪ₚ* e + ↪ₚ*-step : ∀ {n} {e₁ e₂ e₃ : Term n} + → e₁ ↪ₚ e₂ + → e₂ ↪ₚ* e₃ + → e₁ ↪ₚ* e₃ + +↪ₚ*-trans : ∀ {n} {e₁ e₂ e₃ : Term n} + → e₁ ↪ₚ* e₂ + → e₂ ↪ₚ* e₃ + → e₁ ↪ₚ* e₃ +↪ₚ*-trans ↪ₚ*-refl ↪* = ↪* +↪ₚ*-trans (↪ₚ*-step e₁↪ ↪*₁) ↪*₂ = ↪ₚ*-step e₁↪ (↪ₚ*-trans ↪*₁ ↪*₂) + +module ↪ₚ*-Reasoning where + infix 1 begin_ + infixr 2 _↪ₚ⟨_⟩_ _↪ₚ*⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_ + infix 3 _∎ + + begin_ : ∀ {n} {e₁ e₂ : Term n} → e₁ ↪ₚ* e₂ → e₁ ↪ₚ* e₂ + begin p = p + + _↪ₚ⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ₚ e₂ → e₂ ↪ₚ* e₃ → e₁ ↪ₚ* e₃ + _ ↪ₚ⟨ p ⟩ q = ↪ₚ*-step p q + + _↪ₚ*⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ₚ* e₂ → e₂ ↪ₚ* e₃ → e₁ ↪ₚ* e₃ + _ ↪ₚ*⟨ p ⟩ q = ↪ₚ*-trans p q + + _≡⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ≡ e₂ → e₂ ↪ₚ* e₃ → e₁ ↪ₚ* e₃ + _ ≡⟨ refl ⟩ q = q + + _≡⟨⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ₚ* e₂ → e₁ ↪ₚ* e₂ + _ ≡⟨⟩ q = q + + _∎ : ∀ {n} (e : Term n) → e ↪ₚ* e + _ ∎ = ↪ₚ*-refl + +-------------------------------------------------------------------------------- + +-- Parallel reduction is reflexive + +↪ₚ-refl : ∀ {n} {t : Term n} + → t ↪ₚ t +↪ₚ-refl {n} {`refl} = ξ-refl +↪ₚ-refl {n} {` x} = ξ-` +↪ₚ-refl {n} {`proj₁ t} = ξ-proj₁ ↪ₚ-refl +↪ₚ-refl {n} {`proj₂ t} = ξ-proj₂ ↪ₚ-refl +↪ₚ-refl {n} {`Set} = ξ-Set +↪ₚ-refl {n} {`λ t} = ξ-λ ↪ₚ-refl +↪ₚ-refl {n} {t · t₁} = ξ-· ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {∀[x⦂ t ] t₁} = ξ-∀ ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {∃[x⦂ t ] t₁} = ξ-∃ ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {t `, t₁} = ξ-, ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {t `≡ t₁} = ξ-≡ ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {`subst t t₁ t₂} = ξ-subst ↪ₚ-refl ↪ₚ-refl ↪ₚ-refl + +-------------------------------------------------------------------------------- + +-- Regular reduction implies parallel reduction + +↪→↪ₚ : ∀ {n} {t t' : Term n} + → t ↪ t' + → t ↪ₚ t' +↪→↪ₚ β-λ = β-λ ↪ₚ-refl ↪ₚ-refl +↪→↪ₚ (ξ-λ t↪t') = ξ-λ (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-·₁ t↪t') = ξ-· (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-·₂ t↪t') = ξ-· ↪ₚ-refl (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-∀₁ t↪t') = ξ-∀ (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-∀₂ t↪t') = ξ-∀ ↪ₚ-refl (↪→↪ₚ t↪t') +↪→↪ₚ β-subst = β-subst ↪ₚ-refl +↪→↪ₚ (ξ-∃₁ t↪t') = ξ-∃ (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-∃₂ t↪t') = ξ-∃ ↪ₚ-refl (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-proj₁ t↪t') = ξ-proj₁ (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-proj₂ t↪t') = ξ-proj₂ (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-,₁ t↪t') = ξ-, (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-,₂ t↪t') = ξ-, ↪ₚ-refl (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-≡₁ t↪t') = ξ-≡ (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-≡₂ t↪t') = ξ-≡ ↪ₚ-refl (↪→↪ₚ t↪t') +↪→↪ₚ (ξ-subst₁ t↪t') = ξ-subst (↪→↪ₚ t↪t') ↪ₚ-refl ↪ₚ-refl +↪→↪ₚ (ξ-subst₂ t↪t') = ξ-subst ↪ₚ-refl (↪→↪ₚ t↪t') ↪ₚ-refl +↪→↪ₚ (ξ-subst₃ t↪t') = ξ-subst ↪ₚ-refl ↪ₚ-refl(↪→↪ₚ t↪t') +↪→↪ₚ β-proj₁ = β-proj₁ ↪ₚ-refl +↪→↪ₚ β-proj₂ = β-proj₂ ↪ₚ-refl + +↪*→↪ₚ* : ∀ {n} {t t' : Term n} + → t ↪* t' + → t ↪ₚ* t' +↪*→↪ₚ* ↪*-refl = ↪ₚ*-refl +↪*→↪ₚ* (↪*-step t↪x x↪*t') = ↪ₚ*-step (↪→↪ₚ t↪x) (↪*→↪ₚ* x↪*t') + +-------------------------------------------------------------------------------- + +-- Parallel reduction implies regular reduction +↪ₚ→↪* : ∀ {n} {t t' : Term n} + → t ↪ₚ t' + → t ↪* t' +↪ₚ→↪* ξ-` = ↪*-refl +↪ₚ→↪* ξ-Set = ↪*-refl +↪ₚ→↪* (ξ-λ ↪₁) = ξ*-λ (↪ₚ→↪* ↪₁) +↪ₚ→↪* (ξ-∀ ↪₁ ↪₂) = b + where + a = ξ*-∀₁ (↪ₚ→↪* ↪₁) + b = ↪*-trans a (ξ*-∀₂ (↪ₚ→↪* ↪₂)) +↪ₚ→↪* (ξ-∃ ↪₁ ↪₂) = b + where + a = ξ*-∃₁ (↪ₚ→↪* ↪₁) + b = ↪*-trans a (ξ*-∃₂ (↪ₚ→↪* ↪₂)) +↪ₚ→↪* (ξ-· ↪₁ ↪₂) = b + where + a = ξ*-·₁ (↪ₚ→↪* ↪₁) + b = ↪*-trans a (ξ*-·₂ (↪ₚ→↪* ↪₂)) +↪ₚ→↪* (ξ-≡ ↪₁ ↪₂) = b + where + a = ξ*-≡₁ (↪ₚ→↪* ↪₁) + b = ↪*-trans a (ξ*-≡₂ (↪ₚ→↪* ↪₂)) +↪ₚ→↪* (ξ-, ↪₁ ↪₂) = b + where + a = ξ*-,₁ (↪ₚ→↪* ↪₁) + b = ↪*-trans a (ξ*-,₂ (↪ₚ→↪* ↪₂)) +↪ₚ→↪* (β-λ ↪₁ ↪₂ ) = d + where + a = ξ*-·₁ (ξ*-λ (↪ₚ→↪* ↪₁)) + b = ξ*-·₂ (↪ₚ→↪* (↪₂) ) + c = ↪*-trans a b + d = ↪*-trans c (↪*-step β-λ ↪*-refl) +↪ₚ→↪* (β-subst e↪e') = ↪*-step β-subst (↪ₚ→↪* e↪e') +↪ₚ→↪* ξ-refl = ↪*-refl +↪ₚ→↪* (ξ-proj₁ ↪) = ξ*-proj₁ (↪ₚ→↪* ↪) +↪ₚ→↪* (ξ-proj₂ ↪) = ξ*-proj₂ (↪ₚ→↪* ↪) +↪ₚ→↪* (ξ-subst t↪ e₁↪ e₂↪) = e + where + a = ξ*-subst₁ (↪ₚ→↪* t↪) + b = ξ*-subst₂ (↪ₚ→↪* e₁↪) + c = ξ*-subst₃ (↪ₚ→↪* e₂↪) + d = ↪*-trans a b + e = ↪*-trans c d +↪ₚ→↪* (β-proj₁ x↪x') = ↪*-step β-proj₁ (↪ₚ→↪* x↪x') +↪ₚ→↪* (β-proj₂ x↪x') = ↪*-step β-proj₂ (↪ₚ→↪* x↪x') + +↪ₚ*→↪* : ∀ {n} {t t' : Term n} + → t ↪ₚ* t' + → t ↪* t' +↪ₚ*→↪* ↪ₚ*-refl = ↪*-refl +↪ₚ*→↪* (↪ₚ*-step ↪ₚ ↪ₚ*) = ↪*-trans (↪ₚ→↪* ↪ₚ) (↪ₚ*→↪* ↪ₚ*) + +-------------------------------------------------------------------------------- + +↪ₚ-≡ : ∀ {m} {a b b' : Term m} → a ↪ₚ b → b ≡ b' → a ↪ₚ b' +↪ₚ-≡ a↪ₚb b≡b' rewrite b≡b' = a↪ₚb + +-- Parallel reduction is preserved under renaming +↪ₚ-ren : + ∀ {m n} {t t' : Term m} (ρ : Ren m n) → + t ↪ₚ t' → + ren ρ t ↪ₚ ren ρ t' +↪ₚ-ren ρ ξ-` = ξ-` +↪ₚ-ren ρ (β-λ ↪₁ ↪₂) = ↪ₚ-≡ (β-λ a b) (swap-0↦-extᵣ-fusion ρ (↪ₚ₂ ↪₂) (↪ₚ₂ ↪₁)) + where + a = ↪ₚ-ren (extᵣ ρ) ↪₁ + b = (↪ₚ-ren ρ ↪₂) +↪ₚ-ren ρ (ξ-λ ↪) = ξ-λ (↪ₚ-ren (extᵣ ρ) ↪) +↪ₚ-ren ρ (ξ-∀ ↪₁ ↪₂) = ξ-∀ (↪ₚ-ren ρ ↪₁) (↪ₚ-ren (extᵣ ρ) ↪₂) +↪ₚ-ren ρ (ξ-· ↪₁ ↪₂) = ξ-· (↪ₚ-ren ρ ↪₁) (↪ₚ-ren ρ ↪₂) +↪ₚ-ren ρ ξ-Set = ξ-Set +↪ₚ-ren ρ (ξ-proj₁ t↪t') = ξ-proj₁ (↪ₚ-ren ρ t↪t') +↪ₚ-ren ρ (ξ-proj₂ t↪t') = ξ-proj₂ (↪ₚ-ren ρ t↪t') +↪ₚ-ren ρ (ξ-∃ t↪t' t↪t'') = ξ-∃ (↪ₚ-ren ρ t↪t') (↪ₚ-ren (extᵣ ρ) t↪t'') +↪ₚ-ren ρ (ξ-≡ t↪t' t↪t'') = ξ-≡ (↪ₚ-ren ρ t↪t') (↪ₚ-ren ρ t↪t'') +↪ₚ-ren ρ (ξ-, t↪t' t↪t'') = ξ-, (↪ₚ-ren ρ t↪t') (↪ₚ-ren ρ t↪t'') +↪ₚ-ren ρ (ξ-subst t↪t' e₁↪e₁' e₂↪e₂') = ξ-subst (↪ₚ-ren (extᵣ ρ) t↪t') (↪ₚ-ren ρ e₁↪e₁') (↪ₚ-ren ρ e₂↪e₂') +↪ₚ-ren ρ (β-subst e↪e') = β-subst (↪ₚ-ren ρ e↪e') +↪ₚ-ren ρ ξ-refl = ξ-refl +↪ₚ-ren ρ (β-proj₁ x↪x') = β-proj₁ (↪ₚ-ren ρ x↪x') +↪ₚ-ren ρ (β-proj₂ x↪x') = β-proj₂ (↪ₚ-ren ρ x↪x') + +-------{! !}----------------------------------------------------------------------- + +-- A substitution σ₁ reduces to σ₂, if each term of σ₁ reduces to the +-- corresponding term of σ₂. +_↪ₚσ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set +σ₁ ↪ₚσ σ₂ = ∀ x → σ₁ x ↪ₚ σ₂ x + +↪ₚσ-refl : ∀ {m n} {σ : Sub m n} → + σ ↪ₚσ σ +↪ₚσ-refl x = ↪ₚ-refl + +↪ₚσ-ext : ∀ {m n} {σ σ' : Sub m n} + → σ ↪ₚσ σ' + → extₛ σ ↪ₚσ extₛ σ' +↪ₚσ-ext ↪σ zero = ξ-` +↪ₚσ-ext ↪σ (suc x) = ↪ₚ-ren wk (↪σ x) + +↪ₚσ-sub : ∀ {m n} {e e' : Term m} {σ σ' : Sub m n} → + σ ↪ₚσ σ' → + e ↪ₚ e' → + sub σ e ↪ₚ sub σ' e' +↪ₚσ-sub ↪σ ξ-refl = ξ-refl +↪ₚσ-sub ↪σ ξ-` = ↪σ _ +↪ₚσ-sub ↪σ (ξ-λ e↪ₚe') = ξ-λ (↪ₚσ-sub (↪ₚσ-ext ↪σ) e↪ₚe') +↪ₚσ-sub ↪σ (ξ-∀ x↪ₚx' e↪ₚe') = ξ-∀ (↪ₚσ-sub ↪σ x↪ₚx') (↪ₚσ-sub (↪ₚσ-ext ↪σ) e↪ₚe') +↪ₚσ-sub ↪σ (ξ-∃ x↪ₚx' e↪ₚe') = ξ-∃ (↪ₚσ-sub ↪σ x↪ₚx') (↪ₚσ-sub (↪ₚσ-ext ↪σ) e↪ₚe') +↪ₚσ-sub ↪σ (ξ-· l↪ₚl' r↪ₚr') = ξ-· (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') +↪ₚσ-sub ↪σ (ξ-≡ l↪ₚl' r↪ₚr') = ξ-≡ (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') +↪ₚσ-sub ↪σ (ξ-, l↪ₚl' r↪ₚr') = ξ-, (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') +↪ₚσ-sub ↪σ ξ-Set = ξ-Set +↪ₚσ-sub {σ' = σ'} ↪σ (β-λ ₁↪ₚ ₂↪ₚ) + = ↪ₚ-≡ (β-λ (↪ₚσ-sub (↪ₚσ-ext ↪σ) ₁↪ₚ) (↪ₚσ-sub ↪σ ₂↪ₚ)) (swap-0↦-extₛ-fusion σ' (↪ₚ₂ ₂↪ₚ) (↪ₚ₂ ₁↪ₚ)) +↪ₚσ-sub ↪σ (ξ-proj₁ e↪ₚe') = ξ-proj₁ (↪ₚσ-sub ↪σ e↪ₚe') +↪ₚσ-sub ↪σ (ξ-proj₂ e↪ₚe') = ξ-proj₂ (↪ₚσ-sub ↪σ e↪ₚe') +↪ₚσ-sub ↪σ (ξ-subst t↪ₚt' e₁↪ₚe₁' e₂↪ₚe₂) = ξ-subst (↪ₚσ-sub (↪ₚσ-ext ↪σ) t↪ₚt') (↪ₚσ-sub ↪σ e₁↪ₚe₁') (↪ₚσ-sub ↪σ e₂↪ₚe₂) +↪ₚσ-sub ↪σ (β-subst e↪e') = β-subst (↪ₚσ-sub ↪σ e↪e') +↪ₚσ-sub ↪σ (β-proj₁ x) = β-proj₁ (↪ₚσ-sub ↪σ x) +↪ₚσ-sub ↪σ (β-proj₂ x) = β-proj₂ (↪ₚσ-sub ↪σ x) + +↪ₚσ-0↦ : ∀ {n} {e₁ e₂ : Term n} → + e₁ ↪ₚ e₂ → + (0↦ e₁) ↪ₚσ (0↦ e₂) +↪ₚσ-0↦ ↪ₚ zero = ↪ₚ +↪ₚσ-0↦ _ (suc x) = ξ-` + +↪ₚσ-[] : ∀ {n} {e₁ e₁' : Term (suc n)} {e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + e₁ [ e₂ ] ↪ₚ e₁' [ e₂' ] +↪ₚσ-[] ₁↪ₚ ₂↪ₚ = ↪ₚσ-sub (↪ₚσ-0↦ ₂↪ₚ) ₁↪ₚ + +-------------------------------------------------------------------------------- + +_⁺ : ∀ {n} → Term n → Term n +(` x) ⁺ = ` x +(`λ e) ⁺ = `λ (e ⁺) +((`λ e₁) · e₂) ⁺ = e₁ ⁺ [ e₂ ⁺ ] +(e₁ · e₂) ⁺ = e₁ ⁺ · (e₂ ⁺) +(e₁ `, e₂) ⁺ = (e₁ ⁺) `, (e₂ ⁺) +(e₁ `≡ e₂) ⁺ = (e₁ ⁺) `≡ (e₂ ⁺) +(∀[x⦂ t₁ ] t₂) ⁺ = ∀[x⦂ (t₁ ⁺) ] (t₂ ⁺) +(∃[x⦂ t₁ ] t₂) ⁺ = ∃[x⦂ (t₁ ⁺) ] (t₂ ⁺) +`Set ⁺ = `Set +`refl ⁺ = `refl +`proj₁ (e `, _) ⁺ = (e ⁺) +`proj₂ (_ `, e) ⁺ = (e ⁺) +`proj₁ e ⁺ = `proj₁ (e ⁺) +`proj₂ e ⁺ = `proj₂ (e ⁺) +(`subst t `refl e) ⁺ = (e ⁺) +(`subst t e₁ e₂) ⁺ = `subst (t ⁺) (e₁ ⁺) (e₂ ⁺) + +-- Note, in part 4, this proof might have *many* cases. That's to be +-- expected, and most of them are actually very similar. + +par-triangle : ∀ {n} {e e' : Term n} + → e ↪ₚ e' + ------- + → e' ↪ₚ (e ⁺) +par-triangle ξ-` = ξ-` +par-triangle ξ-Set = ξ-Set +par-triangle ξ-refl = ξ-refl +par-triangle (β-λ ₁↪ₚ ₂↪ₚ) = ↪ₚσ-[] (par-triangle ₁↪ₚ) (par-triangle ₂↪ₚ) +par-triangle (ξ-λ x) = ξ-λ (par-triangle x) +par-triangle (ξ-∀ x e) = ξ-∀ (par-triangle x) (par-triangle e) +par-triangle (ξ-· (β-λ ll lr) r) = ξ-· (↪ₚσ-[] (par-triangle ll) (par-triangle lr)) (par-triangle r) +par-triangle (ξ-· (ξ-∀ ll lr) r) = ξ-· (ξ-∀ (par-triangle ll) (par-triangle lr)) (par-triangle r) +par-triangle (ξ-· ξ-` r) = ξ-· ξ-` (par-triangle r) +par-triangle (ξ-· (ξ-λ l) r) = β-λ (par-triangle l) (par-triangle r) +par-triangle (ξ-· (ξ-· ll lr) r) = ξ-· (par-triangle (ξ-· ll lr)) (par-triangle r) +par-triangle (ξ-· ξ-Set r) = ξ-· ξ-Set (par-triangle r) +par-triangle (ξ-· p@(β-proj₁ l) r) = ξ-· (par-triangle p) (par-triangle r) +par-triangle (ξ-· p@(β-proj₂ l) r) = ξ-· (par-triangle p) (par-triangle r) +par-triangle (ξ-· (ξ-proj₁ l) r) = ξ-· (par-triangle (ξ-proj₁ l)) (par-triangle r) +par-triangle (ξ-· (ξ-proj₂ l) r) = ξ-· (par-triangle (ξ-proj₂ l)) (par-triangle r) +par-triangle (ξ-· (ξ-∃ l l₁) r) = ξ-· (ξ-∃ (par-triangle l) (par-triangle l₁)) (par-triangle r) +par-triangle (ξ-· (ξ-≡ l l₁) r) = ξ-· (ξ-≡ (par-triangle l) (par-triangle l₁)) (par-triangle r) +par-triangle (ξ-· (ξ-, l l₁) r) = ξ-· (ξ-, (par-triangle l) (par-triangle l₁)) (par-triangle r) +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 (β-proj₁ e) = par-triangle e +par-triangle (β-proj₂ e) = par-triangle e +par-triangle (ξ-proj₁ ξ-`) = ξ-proj₁ ξ-` +par-triangle (ξ-proj₁ (β-proj₁ e)) = ξ-proj₁ (par-triangle e) +par-triangle (ξ-proj₁ (β-proj₂ e)) = ξ-proj₁ (par-triangle e) +par-triangle (ξ-proj₁ (ξ-proj₁ e)) = ξ-proj₁ (par-triangle (ξ-proj₁ e)) +par-triangle (ξ-proj₁ (ξ-proj₂ e)) = ξ-proj₁ (par-triangle (ξ-proj₂ e)) +par-triangle (ξ-proj₁ `λ@(β-λ x e)) = ξ-proj₁ (par-triangle `λ) +par-triangle (ξ-proj₁ (ξ-λ e)) = ξ-proj₁ (ξ-λ (par-triangle e)) +par-triangle (ξ-proj₁ (ξ-∀ e e₁)) = ξ-proj₁ (ξ-∀ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₁ (ξ-∃ e e₁)) = ξ-proj₁ (ξ-∃ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₁ (ξ-· e e₁)) = ξ-proj₁ (par-triangle (ξ-· e e₁)) +par-triangle (ξ-proj₁ (ξ-≡ e e₁)) = ξ-proj₁ (ξ-≡ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₁ (ξ-, e e₁)) = β-proj₁ (par-triangle e) +par-triangle (ξ-proj₁ (ξ-subst e e₁ e₂)) = ξ-proj₁ (par-triangle (ξ-subst e e₁ e₂)) +par-triangle (ξ-proj₁ (β-subst e)) = ξ-proj₁ (par-triangle e) +par-triangle (ξ-proj₁ ξ-Set) = ξ-proj₁ ξ-Set +par-triangle (ξ-proj₁ ξ-refl) = ξ-proj₁ ξ-refl +par-triangle (ξ-proj₂ ξ-`) = ξ-proj₂ ξ-` +par-triangle (ξ-proj₂ (β-proj₁ e)) = ξ-proj₂ (par-triangle e) +par-triangle (ξ-proj₂ (β-proj₂ e)) = ξ-proj₂ (par-triangle e) +par-triangle (ξ-proj₂ (ξ-proj₁ e)) = ξ-proj₂ (par-triangle (ξ-proj₁ e)) +par-triangle (ξ-proj₂ (ξ-proj₂ e)) = ξ-proj₂ (par-triangle (ξ-proj₂ e)) +par-triangle (ξ-proj₂ `λ@(β-λ e e₁)) = ξ-proj₂ (par-triangle `λ) +par-triangle (ξ-proj₂ (ξ-λ e)) = ξ-proj₂ (ξ-λ (par-triangle e)) +par-triangle (ξ-proj₂ (ξ-∀ e e₁)) = ξ-proj₂ (ξ-∀ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₂ (ξ-∃ e e₁)) = ξ-proj₂ (ξ-∃ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₂ (ξ-· e e₁)) = ξ-proj₂ (par-triangle (ξ-· e e₁)) +par-triangle (ξ-proj₂ (ξ-≡ e e₁)) = ξ-proj₂ (ξ-≡ (par-triangle e) (par-triangle e₁)) +par-triangle (ξ-proj₂ (ξ-, e e₁)) = β-proj₂ (par-triangle e₁) +par-triangle (ξ-proj₂ (ξ-subst e e₁ e₂)) = ξ-proj₂ (par-triangle (ξ-subst e e₁ e₂)) +par-triangle (ξ-proj₂ (β-subst e)) = ξ-proj₂ (par-triangle e) +par-triangle (ξ-proj₂ ξ-Set) = ξ-proj₂ ξ-Set +par-triangle (ξ-proj₂ ξ-refl) = ξ-proj₂ ξ-refl +par-triangle (ξ-∃ e e₁) = ξ-∃ (par-triangle e) (par-triangle e₁) +par-triangle (ξ-≡ e e₁) = ξ-≡ (par-triangle e) (par-triangle e₁) +par-triangle (ξ-, e e₁) = ξ-, (par-triangle e) (par-triangle e₁) +par-triangle (β-subst e) = par-triangle e +par-triangle (ξ-subst e ξ-` e₂) = ξ-subst (par-triangle e) ξ-` (par-triangle e₂) +par-triangle (ξ-subst e (β-proj₁ e₁) e₂) = ξ-subst (par-triangle e) (par-triangle e₁) (par-triangle e₂) +par-triangle (ξ-subst e (β-proj₂ e₁) e₂) = ξ-subst (par-triangle e) (par-triangle e₁) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-proj₁ e₁) e₂) = ξ-subst (par-triangle e) (par-triangle (ξ-proj₁ e₁)) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-proj₂ e₁) e₂) = ξ-subst (par-triangle e) (par-triangle (ξ-proj₂ e₁)) (par-triangle e₂) +par-triangle (ξ-subst e `λ@(β-λ e₁ e₃) e₂) = ξ-subst (par-triangle e) (par-triangle `λ) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-λ e₁) e₂) = ξ-subst (par-triangle e) (ξ-λ (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 (ξ-subst e (ξ-∃ e₁ e₃) e₂) = ξ-subst (par-triangle e) (ξ-∃ (par-triangle e₁) (par-triangle e₃)) (par-triangle e₂) +par-triangle (ξ-subst e (ξ-· e₁ e₃) e₂) = ξ-subst (par-triangle e) (par-triangle (ξ-· e₁ 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 (ξ-subst e (ξ-, e₁ e₃) e₂) = ξ-subst (par-triangle e) (ξ-, (par-triangle e₁) (par-triangle e₃)) (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 ξ-Set e₂) = ξ-subst (par-triangle e) ξ-Set (par-triangle e₂) +par-triangle (ξ-subst e ξ-refl e₂) = β-subst (par-triangle e₂) + +1→* : ∀ {m} {e e' : Term m} → e ↪ₚ e' → (e ↪ₚ* e') +1→* e↪ₚe' = ↪ₚ*-step e↪ₚe' ↪ₚ*-refl + +strip' : ∀ {n} {e e₁ e₂ : Term n} + → e ↪ₚ e₁ + → e ↪ₚ e₂ + → ∃[ e' ] (e₁ ↪ₚ e') × (e₂ ↪ₚ e') +strip' e↪ₚe₁ e↪ₚe₂ = ⟨ _ , ⟨ par-triangle e↪ₚe₁ , par-triangle e↪ₚe₂ ⟩ ⟩ + +strip : ∀ {n} {e e₁ e₂ : Term n} + → e ↪ₚ e₁ + → e ↪ₚ* e₂ + → ∃[ e' ] (e₁ ↪ₚ* e') × (e₂ ↪ₚ e') +strip e↪ₚe₁ ↪ₚ*-refl = ⟨ _ , ⟨ ↪ₚ*-refl , e↪ₚe₁ ⟩ ⟩ +strip e↪ₚe₁ (↪ₚ*-step e↪ₚe₃ e₃↪ₚ*e₂) with strip' e↪ₚe₁ e↪ₚe₃ +... | ⟨ e* , ⟨ e₁↪ₚe* , e₃↪ₚe* ⟩ ⟩ with strip e₃↪ₚe* e₃↪ₚ*e₂ +... | ⟨ e' , ⟨ e*↪ₚ*e' , e₂↪ₚe' ⟩ ⟩ = ⟨ e' , ⟨ ↪ₚ*-step e₁↪ₚe* e*↪ₚ*e' , e₂↪ₚe' ⟩ ⟩ + +-- Confluence for parallel reduction. + +confluenceₚ : ∀ {n} {e e₁ e₂ : Term n} + → e ↪ₚ* e₁ + → e ↪ₚ* e₂ + → ∃[ e' ] (e₁ ↪ₚ* e') × (e₂ ↪ₚ* e') +confluenceₚ ↪ₚ*-refl e↪ₚ*e₂ = ⟨ _ , ⟨ e↪ₚ*e₂ , ↪ₚ*-refl ⟩ ⟩ +confluenceₚ (↪ₚ*-step e↪ₚx x↪ₚ*e₁) e↪ₚ*e₂ with strip e↪ₚx e↪ₚ*e₂ +... | ⟨ e* , ⟨ x↪ₚ*e* , e₂↪ₚe* ⟩ ⟩ with confluenceₚ x↪ₚ*e₁ x↪ₚ*e* +... | ⟨ e' , ⟨ e₁↪ₚ*e' , e*↪ₚ*e' ⟩ ⟩ = ⟨ e' , ⟨ e₁↪ₚ*e' , ↪ₚ*-step e₂↪ₚe* e*↪ₚ*e' ⟩ ⟩ + +-- Confluence for our regular reduction. This is what we actually want. + +confluence : ∀ {n} {e e₁ e₂ : Term n} + → e ↪* e₁ + → e ↪* e₂ + → ∃[ e' ] + e₁ ↪* e' × + e₂ ↪* e' +confluence e↪*e₁ e↪*e₂ with confluenceₚ (↪*→↪ₚ* e↪*e₁) (↪*→↪ₚ* e↪*e₂) +... | ⟨ e' , ⟨ e₁↪ₚ*e' , e₂↪ₚ*e' ⟩ ⟩ = ⟨ e' , ⟨ (↪ₚ*→↪* e₁↪ₚ*e') , (↪ₚ*→↪* e₂↪ₚ*e') ⟩ ⟩ diff --git a/SubjectReduction/ConversionProperties.agda b/SubjectReduction/ConversionProperties.agda new file mode 100644 index 0000000..61e6f66 --- /dev/null +++ b/SubjectReduction/ConversionProperties.agda @@ -0,0 +1,395 @@ +module univTypes.SubjectReduction.ConversionProperties where + +open import Data.Product renaming (_,_ to ⟨_,_⟩) +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning) +open import Data.Fin using (zero; suc) renaming (Fin to 𝔽) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.SubjectReduction.Specification +open import univTypes.SubjectReduction.Confluence using (↪ₚ*-trans; ξ*-λ; ξ*-·₁; ξ*-·₂; ξ*-∀₁; ξ*-∀₂; ξ*-subst₁; ξ*-subst₂; ξ*-subst₃) +open import univTypes.SubjectReduction.Confluence using (ξ*-∃₁; ξ*-∃₂; ξ*-,₁; ξ*-,₂; ξ*-≡₁; ξ*-≡₂; ξ*-proj₁; ξ*-proj₂) +open import univTypes.SubjectReduction.Confluence using (confluence; _↪ₚ_; _↪ₚ*_; ↪ₚ-refl; ↪ₚ-ren; ↪ₚ*→↪*; ↪*→↪ₚ*); open _↪ₚ*_; open _↪ₚ_ +open import univTypes.SubjectReduction.Composition using (swap-0↦-extᵣ-fusion; swap-0↦-extₛ-fusion) +open import univTypes.Util.Fin + +-------------------------------------------------------------------------------- + +-- Conversion is an equivalence relation + +≈-refl : ∀ {n} {e : Term n} + → e ≈ e +≈-refl = mk-≈ _ ↪*-refl ↪*-refl + +≈-sym : ∀ {n} {e₁ e₂ : Term n} + → e₁ ≈ e₂ + → e₂ ≈ e₁ +≈-sym (mk-≈ x y z) = mk-≈ x z y + +≈-trans : ∀ {n} {e₁ e₂ e₃ : Term n} + → e₁ ≈ e₂ + → e₂ ≈ e₃ + → e₁ ≈ e₃ +≈-trans (mk-≈ x e₁↪*x e₂↪*x) (mk-≈ y e₂↪*y e₃↪*y) with confluence e₂↪*x e₂↪*y +... | ⟨ e' , ⟨ x↪*e' , y↪*e' ⟩ ⟩ = mk-≈ e' (↪*-trans e₁↪*x x↪*e') (↪*-trans e₃↪*y y↪*e') + +---------------------------------------------------------------------------- + +-- Reduction implies conversion + +↪→≈ : ∀ {n} {e₁ e₂ : Term n} + → e₁ ↪ e₂ + → e₁ ≈ e₂ +↪→≈ e↪e' = mk-≈ _ (↪*-step e↪e' ↪*-refl) ↪*-refl + +-------------------------------------------------------------------------------- + +-- Congruency rules from parallel reduction, but using ↪* instead of ↪ + +ξₚ*-λ : ∀ {n} {e e' : Term (suc n)} + → e ↪ₚ* e' + --------------- + → `λ e ↪ₚ* `λ e' +ξₚ*-λ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-λ (↪ₚ*→↪* e↪ₚ*e')) + +ξₚ*-proj₁ : ∀ {n} {e e' : Term n} + → e ↪ₚ* e' + --------------- + → `proj₁ e ↪ₚ* `proj₁ e' +ξₚ*-proj₁ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₁ (↪ₚ*→↪* e↪ₚ*e')) + +ξₚ*-proj₂ : ∀ {n} {e e' : Term n} + → e ↪ₚ* e' + --------------- + → `proj₂ e ↪ₚ* `proj₂ e' + +ξₚ*-proj₂ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₂ (↪ₚ*→↪* e↪ₚ*e')) + +ξₚ*-· : ∀ {n} {e₁ e₂ e₁' e₂' : Term n} + → e₁ ↪ₚ* e₁' + → e₂ ↪ₚ* e₂' + --------------------- + → e₁ · e₂ ↪ₚ* e₁' · e₂' +ξₚ*-· e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans + (↪*→↪ₚ* (ξ*-·₁ (↪ₚ*→↪* e₁↪ₚ*e₁'))) + (↪*→↪ₚ* (ξ*-·₂ (↪ₚ*→↪* e₂↪ₚ*e₂'))) + +ξₚ*-, : ∀ {n} {e₁ e₂ e₁' e₂' : Term n} + → e₁ ↪ₚ* e₁' + → e₂ ↪ₚ* e₂' + --------------------- + → e₁ `, e₂ ↪ₚ* e₁' `, e₂' +ξₚ*-, e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans + (↪*→↪ₚ* (ξ*-,₁ (↪ₚ*→↪* e₁↪ₚ*e₁'))) + (↪*→↪ₚ* (ξ*-,₂ (↪ₚ*→↪* e₂↪ₚ*e₂'))) + +ξₚ*-≡ : ∀ {n} {e₁ e₂ e₁' e₂' : Term n} + → e₁ ↪ₚ* e₁' + → e₂ ↪ₚ* e₂' + --------------------- + → e₁ `≡ e₂ ↪ₚ* e₁' `≡ e₂' +ξₚ*-≡ e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans + (↪*→↪ₚ* (ξ*-≡₁ (↪ₚ*→↪* e₁↪ₚ*e₁'))) + (↪*→↪ₚ* (ξ*-≡₂ (↪ₚ*→↪* e₂↪ₚ*e₂'))) + +ξₚ*-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} + → t₁ ↪ₚ* t₁' + → t₂ ↪ₚ* t₂' + ------------------------------- + → ∀[x⦂ t₁ ] t₂ ↪ₚ* ∀[x⦂ t₁' ] t₂' +ξₚ*-∀ x↪ₚ*x' t↪ₚ*t' = ↪ₚ*-trans + (↪*→↪ₚ* (ξ*-∀₁ (↪ₚ*→↪* x↪ₚ*x'))) + (↪*→↪ₚ* (ξ*-∀₂ (↪ₚ*→↪* t↪ₚ*t'))) + +ξₚ*-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} + → t₁ ↪ₚ* t₁' + → t₂ ↪ₚ* t₂' + ------------------------------- + → ∃[x⦂ t₁ ] t₂ ↪ₚ* ∃[x⦂ t₁' ] t₂' +ξₚ*-∃ x↪ₚ*x' t↪ₚ*t' = ↪ₚ*-trans + (↪*→↪ₚ* (ξ*-∃₁ (↪ₚ*→↪* x↪ₚ*x'))) + (↪*→↪ₚ* (ξ*-∃₂ (↪ₚ*→↪* t↪ₚ*t'))) + +ξₚ*-subst : ∀ {n} {t t' : Term (suc n)} {e₁ e₁' e₂ e₂' : Term n} + → t ↪ₚ* t' + → e₁ ↪ₚ* e₁' + → e₂ ↪ₚ* e₂' + ------------------------------- + → `subst t e₁ e₂ ↪ₚ* `subst t' e₁' e₂' +ξₚ*-subst t↪ₚ*t' e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪*→↪ₚ* b + where + ξ-t = ξ*-subst₁ (↪ₚ*→↪* t↪ₚ*t') + ξ-1 = ξ*-subst₂ (↪ₚ*→↪* e₁↪ₚ*e₁') + ξ-2 = ξ*-subst₃ (↪ₚ*→↪* e₂↪ₚ*e₂') + a = ↪*-trans ξ-t ξ-1 + b = ↪*-trans a ξ-2 +-------------------------------------------------------------------------------- +-- "Substituting two convertible terms into another term, yields again convertible terms." + +-- A substitution σ₁ parallel-reduces in many steps to σ₂, if each +-- term of σ₁ parallel-reduces in many steps to the corresponding term of σ₂ +_↪ₚ*σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set +σ₁ ↪ₚ*σ σ₂ = ∀ x → σ₁ x ↪ₚ* σ₂ x + +-- A substitution σ₁ reduces in many steps to σ₂, if each +-- term of σ₁ reduces in many steps to the corresponding term of σ₂ +_↪*σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set +σ₁ ↪*σ σ₂ = ∀ x → σ₁ x ↪* σ₂ x + +-- A substitution σ₁ is convertible to a σ₂, if each +-- term of σ₁ is convertible to the corresponding term of σ₂ +_≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set +σ₁ ≈σ σ₂ = ∀ x → σ₁ x ≈ σ₂ x + +↪ₚ*-ren : + ∀ {m n} {t t' : Term m} (ρ : Ren m n) → + t ↪ₚ* t' → + ren ρ t ↪ₚ* ren ρ t' +↪ₚ*-ren ρ ↪ₚ*-refl = ↪ₚ*-refl +↪ₚ*-ren ρ (↪ₚ*-step t↪ₚt* t*↪ₚ*t') = ↪ₚ*-step (↪ₚ-ren ρ t↪ₚt*) (↪ₚ*-ren ρ t*↪ₚ*t') + +↪ₚ*σ-ext : ∀ {m n} {σ σ' : Sub m n} + → σ ↪ₚ*σ σ' + → extₛ σ ↪ₚ*σ extₛ σ' +↪ₚ*σ-ext σ↪σ' zero = ↪ₚ*-refl +↪ₚ*σ-ext σ↪σ' (suc x) = ↪ₚ*-ren wk (σ↪σ' x) + +↪ₚ*σ-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 σ↪σ')) +↪ₚ*σ-sub {m} {n} {l · r} {σ} {σ'} σ↪σ' = ξₚ*-· (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') +↪ₚ*σ-sub {m} {n} {l `, r} {σ} {σ'} σ↪σ' = ξₚ*-, (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') +↪ₚ*σ-sub {m} {n} {l `≡ r} {σ} {σ'} σ↪σ' = ξₚ*-≡ (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') +↪ₚ*σ-sub {m} {n} {∀[x⦂ x ] e} {σ} {σ'} σ↪σ' = ξₚ*-∀ (↪ₚ*σ-sub {e = x} σ↪σ') (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ')) +↪ₚ*σ-sub {m} {n} {∃[x⦂ x ] e} {σ} {σ'} σ↪σ' = ξₚ*-∃ (↪ₚ*σ-sub {e = x} σ↪σ') (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ')) +↪ₚ*σ-sub {m} {n} {`proj₁ e} {σ} {σ'} σ↪σ' = ξₚ*-proj₁ (↪ₚ*σ-sub {e = e} (σ↪σ')) +↪ₚ*σ-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} {e : Term m} {σ σ' : Sub m n} → + σ ↪*σ σ' → + sub σ e ↪* sub σ' e +↪*σ-sub {m} {n} {e} {σ} {σ'} σ↪σ' = ↪ₚ*→↪* (↪ₚ*σ-sub {m} {n} {e} {σ} {σ'} λ x → ↪*→↪ₚ* (σ↪σ' x)) + +ext-≈σ : ∀ {m n} {σ σ' : Sub m n} + → σ ≈σ σ' + → extₛ σ ≈σ extₛ σ' +ext-≈σ ≈ₛ zero = mk-≈ (` zero) ↪*-refl ↪*-refl +ext-≈σ ≈ₛ (suc x) with ≈ₛ x +... | mk-≈ a σx↪*a σ'x↪*a = mk-≈ (ren suc a) (↪ₚ*→↪* (↪ₚ*-ren suc (↪*→↪ₚ* σx↪*a))) ((↪ₚ*→↪* (↪ₚ*-ren suc (↪*→↪ₚ* σ'x↪*a)))) + +≈σ-sub : ∀ {m n} {σ σ' : Sub m n} {e : Term m} + → σ ≈σ σ' + → 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' + = mk-≈ (l' · r') (↪*-trans (ξ*-·₁ σl↪*l') ((ξ*-·₂ σr↪*r'))) ((↪*-trans (ξ*-·₁ σ'l↪*l') ((ξ*-·₂ σ'r↪*r')))) +≈σ-sub {e = l `≡ r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ' +... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' + = mk-≈ (l' `≡ r') (↪*-trans (ξ*-≡₁ σl↪*l') ((ξ*-≡₂ σr↪*r'))) ((↪*-trans (ξ*-≡₁ σ'l↪*l') ((ξ*-≡₂ σ'r↪*r')))) +≈σ-sub {e = l `, r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ' +... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' + = mk-≈ (l' `, r') (↪*-trans (ξ*-,₁ σl↪*l') ((ξ*-,₂ σr↪*r'))) ((↪*-trans (ξ*-,₁ σ'l↪*l') ((ξ*-,₂ σ'r↪*r')))) +≈σ-sub {e = `λ e} ≈σ' with ≈σ-sub {e = e} (ext-≈σ ≈σ') +... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`λ c) (ξ*-λ eσx↪*a) (ξ*-λ eσ'x↪*a) +≈σ-sub {e = `proj₁ e} ≈σ' with ≈σ-sub {e = e} ≈σ' +... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`proj₁ c) (ξ*-proj₁ eσx↪*a) (ξ*-proj₁ eσ'x↪*a) +≈σ-sub {e = `proj₂ e} ≈σ' with ≈σ-sub {e = e} ≈σ' +... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`proj₂ c) (ξ*-proj₂ eσx↪*a) (ξ*-proj₂ eσ'x↪*a) +≈σ-sub {e = ∀[x⦂ x ] e} ≈σ' with ≈σ-sub {e = x} ≈σ' | ≈σ-sub {e = e} (ext-≈σ ≈σ') +... | mk-≈ a x↪*a x'↪*a | mk-≈ b e↪*b e'↪*b + = mk-≈ (∀[x⦂ a ] b) (↪ₚ*→↪* (ξₚ*-∀ (↪*→↪ₚ* x↪*a) (↪*→↪ₚ* e↪*b))) (↪ₚ*→↪* (ξₚ*-∀ (↪*→↪ₚ* x'↪*a) (↪*→↪ₚ* e'↪*b))) +≈σ-sub {e = ∃[x⦂ x ] e} ≈σ' with ≈σ-sub {e = x} ≈σ' | ≈σ-sub {e = e} (ext-≈σ ≈σ') +... | mk-≈ a x↪*a x'↪*a | mk-≈ b e↪*b e'↪*b + = mk-≈ (∃[x⦂ a ] b) (↪ₚ*→↪* (ξₚ*-∃ (↪*→↪ₚ* x↪*a) (↪*→↪ₚ* e↪*b))) (↪ₚ*→↪* (ξₚ*-∃ (↪*→↪ₚ* x'↪*a) (↪*→↪ₚ* e'↪*b))) +≈σ-sub {e = `subst t e₁ e₂} ≈σ' with ≈σ-sub {e = t} (ext-≈σ ≈σ') | ≈σ-sub {e = e₁} ≈σ' | ≈σ-sub {e = e₂} ≈σ' +... | mk-≈ a t↪*a t'↪*a + | mk-≈ b e₁↪*b e₁'↪*b + | 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))) + +≈→≈σ : ∀ {n} {e e' : Term n} + → e ≈ e' + → 0↦ e ≈σ 0↦ e' +≈→≈σ e≈e' zero = e≈e' +≈→≈σ e≈e' (suc x) = mk-≈ (` x) ↪*-refl ↪*-refl + +≈σ-sub₁ : ∀ {n} {e : Term (suc n)} {e₁ e₂ : Term n} + → e₁ ≈ e₂ + → e [ e₁ ] ≈ e [ e₂ ] +≈σ-sub₁ {n} {e} {e₁} {e₂} e₁≈e₂ = ≈σ-sub {e = e} (≈→≈σ e₁≈e₂) + +≈σ-refl : ∀ {m n} {σ : Sub m n} → + σ ≈σ σ +≈σ-refl x = mk-≈ _ ↪*-refl ↪*-refl + +-------------------------------------------------------------------------------- +-- "Applying a substitution to two convertible terms, yields again convertible terms" + +-- Renaming preserves reduction + + +β-λ₁ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n} + → (`λ e₁) · e₂ ↪ e₁ [ e₂ ] → Term (suc n) +β-λ₁ {e₁ = e₁} _ = e₁ + +β-λ₂ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n} + → (`λ e₁) · e₂ ↪ e₁ [ e₂ ] → Term n +β-λ₂ {e₂ = e₂} _ = e₂ + +↪-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n) + → e ↪ e' + → ren ρ e ↪ ren ρ e' +-- HINT: can also be solved with eq chains instead of subst +↪-ren ρ x@β-λ rewrite sym (swap-0↦-extᵣ-fusion ρ (β-λ₂ x) (β-λ₁ x)) = β-λ +↪-ren ρ (ξ-λ x) = ξ-λ (↪-ren (extᵣ ρ) x) +↪-ren ρ (ξ-proj₁ x) = ξ-proj₁ (↪-ren ρ x) +↪-ren ρ (ξ-proj₂ x) = ξ-proj₂ (↪-ren ρ x) +↪-ren ρ (ξ-·₁ x) = ξ-·₁ (↪-ren ρ x) +↪-ren ρ (ξ-·₂ x) = ξ-·₂ (↪-ren ρ x) +↪-ren ρ (ξ-≡₁ x) = ξ-≡₁ (↪-ren ρ x) +↪-ren ρ (ξ-≡₂ x) = ξ-≡₂ (↪-ren ρ x) +↪-ren ρ (ξ-,₁ x) = ξ-,₁ (↪-ren ρ x) +↪-ren ρ (ξ-,₂ x) = ξ-,₂ (↪-ren ρ x) +↪-ren ρ (ξ-∀₁ x) = ξ-∀₁ (↪-ren ρ x) +↪-ren ρ (ξ-∀₂ x) = ξ-∀₂ (↪-ren (extᵣ ρ) x) +↪-ren ρ β-proj₁ = β-proj₁ +↪-ren ρ β-proj₂ = β-proj₂ +↪-ren ρ β-subst = β-subst +↪-ren ρ (ξ-∃₁ x) = ξ-∃₁ (↪-ren ρ x) +↪-ren ρ (ξ-∃₂ x) = ξ-∃₂ (↪-ren (extᵣ ρ) x) +↪-ren ρ (ξ-subst₁ x) = ξ-subst₁ (↪-ren (extᵣ ρ) x) +↪-ren ρ (ξ-subst₂ x) = ξ-subst₂ (↪-ren ρ x) +↪-ren ρ (ξ-subst₃ x) = ξ-subst₃ (↪-ren ρ x) + +-- Renaming preserves many reduction steps + +↪*-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n) + → e ↪* e' + → ren ρ e ↪* ren ρ e' +↪*-ren ρ x = ↪ₚ*→↪* (↪ₚ*-ren ρ (↪*→↪ₚ* x)) + +-- Renaming preserves convertibility + +≈-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n) + → e ≈ e' + → ren ρ e ≈ ren ρ e' +≈-ren ρ (mk-≈ c e↪*c e'↪*c) + = mk-≈ (ren ρ c) (↪*-ren ρ e↪*c) (↪*-ren ρ e'↪*c) + +-- Substitution preserves reduction + +↪-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n) + → e ↪ e' + → sub σ e ↪ sub σ e' +-- HINT: can also be solved with eq chains instead of subst +↪-sub σ x@β-λ rewrite sym (swap-0↦-extₛ-fusion σ (β-λ₂ x) (β-λ₁ x)) = β-λ +↪-sub σ (ξ-λ x) = ξ-λ (↪-sub (extₛ σ) x) +↪-sub σ (ξ-·₁ x) = ξ-·₁ (↪-sub σ x) +↪-sub σ (ξ-·₂ x) = ξ-·₂ (↪-sub σ x) +↪-sub σ (ξ-,₁ x) = ξ-,₁ (↪-sub σ x) +↪-sub σ (ξ-,₂ x) = ξ-,₂ (↪-sub σ x) +↪-sub σ (ξ-∀₁ x) = ξ-∀₁ (↪-sub σ x) +↪-sub σ (ξ-∀₂ x) = ξ-∀₂ (↪-sub (extₛ σ) x) +↪-sub σ (ξ-∃₁ x) = ξ-∃₁ (↪-sub σ x) +↪-sub σ (ξ-∃₂ x) = ξ-∃₂ (↪-sub (extₛ σ) x) +↪-sub σ β-proj₁ = β-proj₁ +↪-sub σ β-proj₂ = β-proj₂ +↪-sub σ β-subst = β-subst +↪-sub σ (ξ-proj₁ x) = ξ-proj₁ (↪-sub σ x) +↪-sub σ (ξ-proj₂ x) = ξ-proj₂ (↪-sub σ x) +↪-sub σ (ξ-≡₁ x) = ξ-≡₁ (↪-sub σ x) +↪-sub σ (ξ-≡₂ x) = ξ-≡₂ (↪-sub σ x) +↪-sub σ (ξ-subst₁ x) = ξ-subst₁ (↪-sub (extₛ σ) x) +↪-sub σ (ξ-subst₂ x) = ξ-subst₂ (↪-sub σ x) +↪-sub σ (ξ-subst₃ x) = ξ-subst₃ (↪-sub σ x) + +-- Substitution preserves many reduction steps + +↪*-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n) + → e ↪* e' + → sub σ e ↪* sub σ e' +↪*-sub σ ↪*-refl = ↪*-refl +↪*-sub σ (↪*-step x x₁) = ↪*-step (↪-sub σ x) (↪*-sub σ x₁) + +-- Substitution preserves convertibility + +≈-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n) + → e ≈ e' + → sub σ e ≈ sub σ e' +≈-sub σ (mk-≈ x e↪*x e'↪*x) + = mk-≈ (sub σ x) (↪*-sub σ e↪*x) (↪*-sub σ e'↪*x) + +-------------------------------------------------------------------------------- +-- "Typing is preserved along convertible types in the context" + +-- Two contexts Γ₁ and Γ₂ are convertible, if each type in Γ₁ is +-- convertible to the corresponding type in Γ₂. + +_≈ᶜ_ : ∀ {n} → Context n → Context n → Set +Γ₁ ≈ᶜ Γ₂ = ∀ x → lookup Γ₁ x ≈ lookup Γ₂ x + +≈ᶜ-refl : ∀ {n} {Γ : Context n} + → Γ ≈ᶜ Γ +≈ᶜ-refl x = ≈-refl + +≈-ext : ∀ {n} {Γ₁ Γ₂ : Context n} {t₁ t₂ : Term n} + → Γ₁ ≈ᶜ Γ₂ + → t₁ ≈ t₂ + → (Γ₁ , t₁) ≈ᶜ (Γ₂ , t₂) +≈-ext Γ₁≈Γ₂ t₁≈t₂ zero = ≈-ren wk t₁≈t₂ +≈-ext Γ₁≈Γ₂ t₁≈t₂ (suc x) = ≈-ren wk (Γ₁≈Γ₂ x) + +≈-Γ-⊢ : ∀ {n} {Γ₁ Γ₂ : Context n} {e t : Term n} + → Γ₁ ≈ᶜ Γ₂ + → Γ₁ ⊢ e ⦂ t + → Γ₂ ⊢ e ⦂ t +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-` x refl) = ⊢-≈ (≈-sym (Γ₁≈Γ₂ x)) (⊢-` x refl) +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-λ ⊢e₁ ⊢e₂) = ⊢-λ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂) +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-· ⊢l ⊢r) = ⊢-· (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r) +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-, ⊢l ⊢r) = ⊢-, (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r) +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≡ ⊢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₁]) + +≈-Γ-⊢₁ : ∀ {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₃)) +≈-Γ-⊢₁ t₁≈t₂ (⊢-proj₁ e) = ⊢-proj₁ (≈-Γ-⊢₁ t₁≈t₂ e) +≈-Γ-⊢₁ t₁≈t₂ (⊢-proj₂ e) = ⊢-proj₂ (≈-Γ-⊢₁ t₁≈t₂ e) +≈-Γ-⊢₁ t₁≈t₂ (⊢-· t⊢e t⊢e₁) = ⊢-· (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁) +≈-Γ-⊢₁ t₁≈t₂ (⊢-≡ t⊢e t⊢e₁) = ⊢-≡ (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁) +≈-Γ-⊢₁ t₁≈t₂ (⊢-, t⊢e t⊢e₁) = ⊢-, (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁) +≈-Γ-⊢₁ t₄≈t₂ (⊢-∀ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-∀ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁) (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃) +≈-Γ-⊢₁ t₄≈t₂ (⊢-∃ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-∃ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁) (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃) +≈-Γ-⊢₁ t₁≈t₂ (⊢-≈ x t⊢e) = ⊢-≈ x (≈-Γ-⊢₁ t₁≈t₂ t⊢e) +≈-Γ-⊢₁ t₁≈t₂ (⊢-subst t₁,t'⊢t t₁⊢u₁ t₁⊢u₂ t₁⊢≡ t₁⊢t[u₁]) + = ⊢-subst (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₁≈t₂) ≈-refl) t₁,t'⊢t) + (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₁) + (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₂) + (≈-Γ-⊢₁ t₁≈t₂ t₁⊢≡) + (≈-Γ-⊢₁ t₁≈t₂ t₁⊢t[u₁]) diff --git a/SubjectReduction/Inversion.agda b/SubjectReduction/Inversion.agda new file mode 100644 index 0000000..5ba2808 --- /dev/null +++ b/SubjectReduction/Inversion.agda @@ -0,0 +1,157 @@ +module univTypes.SubjectReduction.Inversion where + +open import Data.Product renaming (_,_ to ⟨_,_⟩) +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning) +open import Data.Fin using (zero; suc) renaming (Fin to 𝔽) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.SubjectReduction.Specification +open import univTypes.SubjectReduction.ConversionProperties using (≈-refl; ≈-trans; ≈-sym; ≈-sub) + +-------------------------------------------------------------------------------- + +-- Inversion for lambda terms + +↪-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} → + ∀[x⦂ t₁ ] t₂ ↪ t → + ∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂') +↪-∀-shape (ξ-∀₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪-∀-shape (ξ-∀₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩ + +↪*-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} → + (∀[x⦂ t₁ ] t₂) ↪* t → + ∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂') +↪*-∀-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪*-∀-shape (↪*-step ∀↪z z↪*t) with ↪-∀-shape ∀↪z +... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∀-shape z↪*t +... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ + = ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ + +invert-≈-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} → + (∀[x⦂ t₁ ] t₂) ≈ (∀[x⦂ t₁' ] t₂') → + t₁ ≈ t₁' × t₂ ≈ t₂' +invert-≈-∀ (mk-≈ x ∀₁↪*x ∀₂↪*x) with ↪*-∀-shape ∀₁↪*x | ↪*-∀-shape ∀₂↪*x +... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩ + | ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩ + = ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩ + +invert-⊢λ' : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t : Term n} → + Γ ⊢ `λ e ⦂ t → + ∃[ t₁ ] ∃[ t₂ ] + t ≈ (∀[x⦂ t₁ ] t₂) × + Γ ⊢ t₁ ⦂ `Set × + Γ , t₁ ⊢ e ⦂ t₂ +invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩ +invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁ +... | ⟨ X , ⟨ E , ⟨ t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ + = ⟨ X , ⟨ E , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ + +invert-⊢λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂ + → ∃[ t₁' ] ∃[ t₂' ] + t₁ ≈ t₁' × + t₂ ≈ t₂' × + Γ ⊢ t₁' ⦂ `Set × + Γ , t₁' ⊢ e ⦂ t₂' +invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩ +invert-⊢λ (⊢-≈ t≈∀ ⊢λ) with invert-⊢λ' ⊢λ +... | ⟨ X , ⟨ E , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀') +... | ⟨ ≈₁ , ≈₂ ⟩ + = ⟨ X , ⟨ E , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ + + +-- Inversion for pairs + +↪-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} → + ∃[x⦂ t₁ ] t₂ ↪ t → + ∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂') +↪-∃-shape (ξ-∃₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪-∃-shape (ξ-∃₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩ + +↪*-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} → + (∃[x⦂ t₁ ] t₂) ↪* t → + ∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂') +↪*-∃-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪*-∃-shape (↪*-step ∀↪z z↪*t) with ↪-∃-shape ∀↪z +... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∃-shape z↪*t +... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ + = ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩ + +invert-≈-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} → + (∃[x⦂ t₁ ] t₂) ≈ (∃[x⦂ t₁' ] t₂') → + t₁ ≈ t₁' × t₂ ≈ t₂' +invert-≈-∃ (mk-≈ x ∃₁↪*x ∃₂↪*x) with ↪*-∃-shape ∃₁↪*x | ↪*-∃-shape ∃₂↪*x +... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩ + | ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩ + = ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩ + +invert-⊢,' : ∀ {n} {Γ : Context n} {l r t : Term n} → + Γ ⊢ l `, r ⦂ t → + ∃[ t₁ ] ∃[ t₂ ] + t ≈ (∃[x⦂ t₁ ] t₂) × + Γ ⊢ l ⦂ t₁ × + Γ ⊢ r ⦂ t₂ [ l ] +invert-⊢,' (⊢-≈ t₁≈t ⊢lr) with invert-⊢,' ⊢lr +... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃ , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ + = ⟨ x₁ , ⟨ x₂ , ⟨ ≈-sym (≈-trans (≈-sym t≈∃) t₁≈t) , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ +invert-⊢,' (⊢-, {n} {Γ} {e₁} {e₂} {t₁} {t₂} ⊢l ⊢r) = ⟨ t₁ , ⟨ t₂ , ⟨ ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ + +invert-⊢, : ∀ {n} {Γ : Context n} {l r : Term n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ l `, r ⦂ ∃[x⦂ t₁ ] t₂ + → ∃[ t₁' ] ∃[ t₂' ] + t₁ ≈ t₁' × + t₂ ≈ t₂' × + Γ ⊢ l ⦂ t₁ × + Γ ⊢ r ⦂ t₂ [ l ] +invert-⊢, (⊢-≈ t≈∃ ⊢lr) with invert-⊢,' ⊢lr +... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃' , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ with invert-≈-∃ (≈-trans (≈-sym t≈∃) t≈∃') +... | ⟨ ≈₁ , ≈₂ ⟩ + = ⟨ x₁ , ⟨ x₂ , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ ⊢-≈ (≈-sym ≈₁) ⊢l , ⊢-≈ (≈-sub _ (≈-sym ≈₂)) ⊢r ⟩ ⟩ ⟩ ⟩ ⟩ +invert-⊢, (⊢-, ⊢l ⊢r) + = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ ⟩ + +↪-≡-shape : ∀ {n} {t u₁ u₂ : Term n} → + u₁ `≡ u₂ ↪ t → + ∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂') +↪-≡-shape (ξ-≡₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪-≡-shape (ξ-≡₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩ + +↪*-≡-shape : ∀ {n} {t u₁ u₂ : Term n} → + (u₁ `≡ u₂) ↪* t → + ∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂') +↪*-≡-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩ +↪*-≡-shape (↪*-step ≡↪x x↪*t) with ↪-≡-shape ≡↪x +... | ⟨ a , ⟨ b , ⟨ refl , ⟨ u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape x↪*t +... | ⟨ x , ⟨ y , ⟨ refl , ⟨ a↪*x , b↪*y ⟩ ⟩ ⟩ ⟩ + = ⟨ x , ⟨ y , ⟨ refl , ⟨ ↪*-trans u₁↪*a a↪*x , ↪*-trans u₂↪*b b↪*y ⟩ ⟩ ⟩ ⟩ + +invert-≈-≡ : ∀ {n} {u₁ u₁' u₂ u₂' : Term n} → + (u₁ `≡ u₂) ≈ (u₁' `≡ u₂') → + u₁ ≈ u₁' × u₂ ≈ u₂' +invert-≈-≡ (mk-≈ x ≡↪*x ≡'↪*x) with ↪*-≡-shape ≡↪*x +... | ⟨ a , ⟨ b , ⟨ refl , ⟨ u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape ≡'↪*x +... | ⟨ _ , ⟨ _ , ⟨ refl , ⟨ u₁'↪*a , u₂'↪*b ⟩ ⟩ ⟩ ⟩ + = ⟨ mk-≈ a u₁↪*a u₁'↪*a , mk-≈ b u₂↪*b u₂'↪*b ⟩ + +invert-⊢refl' : ∀ {n} {Γ : Context n} {t : Term n} + → Γ ⊢ `refl ⦂ t + → ∃[ u₁ ] ∃[ u₂ ] + t ≈ u₁ `≡ u₂ × + u₁ ≈ u₂ +invert-⊢refl' (⊢-≈ t₁≈t ⊢refl) with invert-⊢refl' ⊢refl +... | ⟨ u₁ , ⟨ u₂ , ⟨ t₁≈≡ , u₁≈u₂ ⟩ ⟩ ⟩ + = ⟨ _ , ⟨ _ , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈≡ , u₁≈u₂ ⟩ ⟩ ⟩ +invert-⊢refl' (⊢-refl ⊢refl) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ≈-refl ⟩ ⟩ ⟩ + +invert-⊢refl : ∀ {n} {Γ : Context n} {u₁ u₂ : Term n} + → Γ ⊢ `refl ⦂ u₁ `≡ u₂ + → u₁ ≈ u₂ +invert-⊢refl (⊢-refl ⊢refl) = ≈-refl +invert-⊢refl (⊢-≈ t≈≡ ⊢refl) with invert-⊢refl' ⊢refl +... | ⟨ u₁' , ⟨ u₂' , ⟨ t≈≡' , ≈' ⟩ ⟩ ⟩ with invert-≈-≡ (≈-trans (≈-sym t≈≡') t≈≡) +... | ⟨ ≈₁ , ≈₂ ⟩ + = ≈-trans (≈-trans (≈-sym ≈₁) ≈') ≈₂ diff --git a/SubjectReduction/Specification.agda b/SubjectReduction/Specification.agda new file mode 100644 index 0000000..a79a407 --- /dev/null +++ b/SubjectReduction/Specification.agda @@ -0,0 +1,469 @@ +module univTypes.SubjectReduction.Specification where + +open import Data.Nat using (ℕ; zero; suc) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import univTypes.Util.Fin using (Fin; zero; suc) + +-- Fixities -------------------------------------------------------------------- + +infix 4 _↪_ _↪*_ +infix 4 _⊢_⦂_ +infixl 5 _,_ +infix 5 `λ_ +infixl 7 _·_ +infix 9 `_ +infixl 9 _[_] + +-- Axioms ---------------------------------------------------------------------- + +-- Functional Extensionality +postulate + fun-ext : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : A → Set ℓ₂} {f g : (x : A) → B x} + → (∀ x → f x ≡ g x) + → f ≡ g + +-- No other postulates are allowed! + +-- Syntax ---------------------------------------------------------------------- + +data Term : ℕ → Set where + `_ : ∀ {n} → Fin n → Term n + `λ_ : ∀ {n} → Term (suc n) → Term n + _·_ : ∀ {n} → Term n → Term n → Term n + ∀[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n + + -- My Extension + `Setω_ : ∀ {n} (l : Term n) → Term n + `Setn_ : ∀ {n} (l : Term n) → Term n + `Level : ∀ {n} → Term n + `lzero : ∀ {n} → Term n + `lsuc : ∀ {n} → Term n → Term n + _`⊔_ : ∀ {n} → Term n → Term n → Term n + + -- Extension + ∃[x⦂_]_ : ∀ {n} → Term n → Term (suc n) → Term n + _`,_ : ∀ {n} → Term n → Term n → Term n + `proj₁ : ∀ {n} → Term n → Term n + `proj₂ : ∀ {n} → Term n → Term n + _`≡_ : ∀ {n} → Term n → Term n → Term n + `refl : ∀ {n} → Term n + `subst : ∀ {n} → Term (suc n) → Term n → Term n → Term n + +-- Substitution ---------------------------------------------------------------- + +`Set : ∀ {n} → Term n +`Set = `Setn (`lzero) + +-- Renamings + +Ren : ℕ → ℕ → Set +Ren m n = Fin m → Fin n + +extᵣ : ∀ {m n} → Ren m n → Ren (suc m) (suc n) +extᵣ ρ zero = zero +extᵣ ρ (suc x) = suc (ρ x) + +ren : ∀ {m n} + → Ren m n + → (Term m → Term n) +ren ρ (` x) = ` (ρ x) +ren ρ (`λ e) = `λ (ren (extᵣ ρ) e) +ren ρ (e₁ · e₂) = (ren ρ e₁) · (ren ρ e₂) +ren ρ (∀[x⦂ e₁ ] e₂) = ∀[x⦂ ren ρ e₁ ] ren (extᵣ ρ) e₂ +ren ρ (`Setω l) = `Setω (ren ρ l) +ren ρ (`Setn x) = `Setn ren ρ x +ren ρ `Level = `Level +ren ρ `lzero = `lzero +ren ρ (`lsuc l) = `lsuc (ren ρ l) +ren ρ (l `⊔ r) = (ren ρ l) `⊔ (ren ρ r) +ren ρ (∃[x⦂ t₁ ] t₂) = ∃[x⦂ ren ρ t₁ ] ren (extᵣ ρ) t₂ +ren ρ (e₁ `, e₂) = (ren ρ e₁) `, (ren ρ e₂) +ren ρ (`proj₁ e) = `proj₁ (ren ρ e) +ren ρ (`proj₂ e) = `proj₂ (ren ρ e) +ren ρ `refl = `refl +ren ρ (e₁ `≡ e₂) = ren ρ e₁ `≡ ren ρ e₂ +ren ρ (`subst t e₁ e₂) = `subst (ren (extᵣ ρ) t) (ren ρ e₁) (ren ρ e₂) + +wk : ∀ {n} → Ren n (suc n) +wk x = suc x + +-- Substitutions + +Sub : ℕ → ℕ → Set +Sub m n = Fin m → Term n + +extₛ : ∀ {m n} → Sub m n → Sub (suc m) (suc n) +extₛ σ zero = ` zero +extₛ σ (suc x) = ren wk (σ x) + +sub : ∀ {m n} + → Sub m n + → (Term m → Term n) +sub σ (` x) = σ x +sub σ (`λ e) = `λ (sub (extₛ σ) e) +sub σ (e₁ · e₂) = (sub σ e₁) · (sub σ e₂) +sub σ (∀[x⦂ e₁ ] e₂) = ∀[x⦂ sub σ e₁ ] sub (extₛ σ) e₂ +sub σ (`Setω l) = `Setω (sub σ l) +sub σ (`Setn l) = `Setn sub σ l +sub σ (`Level) = `Level +sub σ `lzero = `lzero +sub σ (`lsuc l) = `lsuc (sub σ l) +sub σ (l `⊔ r) = (sub σ l) `⊔ (sub σ r) +sub σ (∃[x⦂ t₁ ] t₂) = ∃[x⦂ sub σ t₁ ] sub (extₛ σ) t₂ +sub σ (e₁ `, e₂) = (sub σ e₁) `, (sub σ e₂) +sub σ (`proj₁ e) = `proj₁ (sub σ e) +sub σ (`proj₂ e) = `proj₂ (sub σ e) +sub σ `refl = `refl +sub σ (e₁ `≡ e₂) = sub σ e₁ `≡ sub σ e₂ +sub σ (`subst t e₁ e₂) = `subst (sub (extₛ σ) t) (sub σ e₁) (sub σ e₂) + +0↦ : ∀ {n} → Term n → Sub (suc n) n +(0↦ e) zero = e +(0↦ e) (suc x) = ` x + +_[_] : ∀ {n} → Term (suc n) → Term n → Term n +e₁ [ e₂ ] = sub (0↦ e₂) e₁ + +-- Semantics ------------------------------------------------------------------- + +-- Values + +mutual + data Value : ∀ {n} → Term n → Set where + val-λ : ∀ {n} {e : Term (suc n)} + → Value e + ------------ + → Value (`λ e) + val-∀ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)} + → Value e₁ + → Value e₂ + -------------------- + → Value (∀[x⦂ e₁ ] e₂) + val-Setω : ∀ {n l} + → Value {n = n} (`Setω l) + val-Setn : ∀ {n l} + → Value l + → Value {n = n} (`Setn l) + + val-Level : ∀ {n} + → Value {n = n} `Level + + val-l : ∀ {n v} + → Value {n = n} (`lzero) + + val-lsuc : ∀ {n v l} + → Value l + → Value {n = n} (`lsuc l) + + val-neu : ∀ {n} {e : Term n} + → Neutral e + --------- + → Value e + val-∃ : ∀ {n} {e₁ : Term n} {e₂ : Term (suc n)} + → Value e₁ + → Value e₂ + -------------------- + → Value (∃[x⦂ e₁ ] e₂) + val-, : ∀ {n} {e₁ e₂ : Term n} + → Value e₁ + → Value e₂ + --------- + → Value (e₁ `, e₂) + val-≡ : ∀ {n} {e₁ : Term n} {e₂ : Term n} + → Value e₁ + → Value e₂ + -------------------- + → Value (e₁ `≡ e₂) + val-refl : ∀ {n} + → Value {n = n} `refl + + data Neutral : ∀ {n} → Term n → Set where + neu-` : ∀ {n} {x : Fin n} + → Neutral (` x) + neu-· : ∀ {n} {e₁ e₂ : Term n} + → Neutral e₁ + → Value e₂ + ----------------- + → Neutral (e₁ · e₂) + neu-proj₁ : ∀ {n} {e : Term n} + → Neutral e + ----------------- + → Neutral (`proj₁ e) + neu-proj₂ : ∀ {n} {e : Term n} + → Neutral e + ----------------- + → Neutral (`proj₂ e) + neu-subst : ∀ {n} {t : Term (suc n)} {e₁ e₂ : Term n} + → Value t + → Neutral e₁ + → Value e₂ + ------------------------ + → Neutral (`subst t e₁ e₂) + +-- Reduction + +data _↪_ : ∀ {n} → Term n → Term n → Set where + β-λ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n} + → (`λ e₁) · e₂ ↪ e₁ [ e₂ ] + + ξ-λ : ∀ {n} {e e' : Term (suc n)} + → e ↪ e' + --------------- + → `λ e ↪ `λ e' + + ξ-·₁ : ∀ {n} {e₁ e₂ e₁' : Term n} + → e₁ ↪ e₁' + --------------------- + → e₁ · e₂ ↪ e₁' · e₂ + + ξ-·₂ : ∀ {n} {e₁ e₂ e₂' : Term n} + → e₂ ↪ e₂' + --------------------- + → e₁ · e₂ ↪ e₁ · e₂' + + ξ-∀₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)} + → t₁ ↪ t₁' + ------------------------------- + → ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁' ] t₂ + + ξ-∀₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)} + → t₂ ↪ t₂' + ------------------------------- + → ∀[x⦂ t₁ ] t₂ ↪ ∀[x⦂ t₁ ] t₂' + + β-proj₁ : ∀ {n} {e₁ e₂ : Term n} + → `proj₁ (e₁ `, e₂) ↪ e₁ + + β-proj₂ : ∀ {n} {e₁ e₂ : Term n} + → `proj₂ (e₁ `, e₂) ↪ e₂ + + β-subst : ∀ {n} {t : Term (suc n)} {e : Term n} + → `subst t `refl e ↪ e + + ξ-∃₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term (suc n)} + → t₁ ↪ t₁' + ------------------------------- + → ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁' ] t₂ + + ξ-∃₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term (suc n)} + → t₂ ↪ t₂' + ------------------------------- + → ∃[x⦂ t₁ ] t₂ ↪ ∃[x⦂ t₁ ] t₂' + + ξ-proj₁ : ∀ {n} {e e' : Term n} + → e ↪ e' + → `proj₁ e ↪ `proj₁ e' + + ξ-proj₂ : ∀ {n} {e e' : Term n} + → e ↪ e' + → `proj₂ e ↪ `proj₂ e' + + ξ-,₁ : ∀ {n} {e₁ e₁' e₂ : Term n} + → e₁ ↪ e₁' + → (e₁ `, e₂) ↪ (e₁' `, e₂) + + ξ-,₂ : ∀ {n} {e₁ e₂ e₂' : Term n} + → e₂ ↪ e₂' + → (e₁ `, e₂) ↪ (e₁ `, e₂') + + ξ-≡₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n} + → t₁ ↪ t₁' + ------------------------------- + → (t₁ `≡ t₂) ↪ (t₁' `≡ t₂) + + ξ-≡₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n} + → t₂ ↪ t₂' + ------------------------------- + → (t₁ `≡ t₂) ↪ (t₁ `≡ t₂') + + ξ-subst₁ : ∀ {n} {t t' : Term (suc n)} {e₁ e₂ : Term n} + → t ↪ t' + → `subst t e₁ e₂ ↪ `subst t' e₁ e₂ + + ξ-subst₂ : ∀ {n} {t : Term (suc n)} {e₁ e₁' e₂ : Term n} + → e₁ ↪ e₁' + → `subst t e₁ e₂ ↪ `subst t e₁' e₂ + + ξ-subst₃ : ∀ {n} {t : Term (suc n)} {e₁ e₂ e₂' : Term n} + → e₂ ↪ e₂' + → `subst t e₁ e₂ ↪ `subst t e₁ e₂' + +-- Extension: + ξ-⊔₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n} + → t₁ ↪ t₁' + ------------------------------- + → (t₁ `⊔ t₂) ↪ (t₁' `⊔ t₂) + + ξ-⊔₂ : ∀ {n} {t₁ : Term n} {t₂ t₂' : Term n} + → t₂ ↪ t₂' + ------------------------------- + → (t₁ `⊔ t₂) ↪ (t₁ `⊔ t₂') + + ξ-Setn : ∀ {n} {l l' : Term n} + → l ↪ l' + → `Setn l ↪ `Setn l' + + ξ-Setω : ∀ {n} {l l' : Term n} + → l ↪ l' + → `Setω l ↪ `Setω l' + +-- Reflexive, Transitive Closure of Reduction + +data _↪*_ : ∀ {n} → Term n → Term n → Set where + ↪*-refl : ∀ {n} {e : Term n} + → e ↪* e + ↪*-step : ∀ {n} {e₁ e₂ e₃ : Term n} + → e₁ ↪ e₂ + → e₂ ↪* e₃ + → e₁ ↪* e₃ + +↪*-trans : ∀ {n} {e₁ e₂ e₃ : Term n} + → e₁ ↪* e₂ + → e₂ ↪* e₃ + → e₁ ↪* e₃ +↪*-trans ↪*-refl q = q +↪*-trans (↪*-step x p) q = ↪*-step x (↪*-trans p q) + +module ↪*-Reasoning where + infix 1 begin_ + infixr 2 _↪⟨_⟩_ _↪*⟨_⟩_ _≡⟨_⟩_ _≡⟨⟩_ + infix 3 _∎ + + begin_ : ∀ {n} {e₁ e₂ : Term n} → e₁ ↪* e₂ → e₁ ↪* e₂ + begin p = p + + _↪⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃ + _ ↪⟨ p ⟩ q = ↪*-step p q + + _↪*⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₂ ↪* e₃ → e₁ ↪* e₃ + _ ↪*⟨ p ⟩ q = ↪*-trans p q + + _≡⟨_⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ≡ e₂ → e₂ ↪* e₃ → e₁ ↪* e₃ + _ ≡⟨ refl ⟩ q = q + + _≡⟨⟩_ : ∀ {n} (e₁ {e₂} {e₃} : Term n) → e₁ ↪* e₂ → e₁ ↪* e₂ + _ ≡⟨⟩ q = q + + _∎ : ∀ {n} (e : Term n) → e ↪* e + _ ∎ = ↪*-refl + +-- Conversion + +-- Two terms are convertible iff they reduce to a common term. + +infix 4 _≈_ +record _≈_ {n} (e₁ e₂ : Term n) : Set where + constructor mk-≈ + field + e-common : Term n + e₁↪*e-common : e₁ ↪* e-common + e₂↪*e-common : e₂ ↪* e-common + +open _≈_ public + +-- Typing ---------------------------------------------------------------------- + +data Context : ℕ → Set where + ∅ : Context zero + _,_ : ∀ {n} → Context n → Term n → Context (suc n) + +lookup : ∀ {n} → Context n → Fin n → Term n +lookup (Γ , e) zero = ren wk e +lookup (Γ , e) (suc x) = ren wk (lookup Γ x) + +data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where + + ⊢-` : ∀ {n t} {Γ : Context n} (x : Fin n) + → lookup Γ x ≡ t + -------------- + → Γ ⊢ ` x ⦂ t + + ⊢-λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ l : Term n} {t₂ : Term (suc n)} + → Γ ⊢ t₁ ⦂ `Setn l + → Γ , t₁ ⊢ e ⦂ t₂ + ----------------------- + → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂ + + ⊢-· : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ e₁ ⦂ ∀[x⦂ t₁ ] t₂ + → Γ ⊢ e₂ ⦂ t₁ + ----------------------- + → Γ ⊢ e₁ · e₂ ⦂ t₂ [ e₂ ] + + ⊢-∀ : ∀ {n} {Γ : Context n} {t₁ l₁ l₃ : Term n} {t₂ l₂ : Term (suc n)} + → Γ ⊢ t₁ ⦂ `Setn l₁ + → Γ , t₁ ⊢ t₂ ⦂ `Setn l₂ + ----------------------- + → Γ ⊢ ∀[x⦂ t₁ ] t₂ ⦂ `Setn l₃ + + ⊢-≈ : ∀ {n} {Γ : Context n} {e : Term n} {t t' : Term n} + → t ≈ t' + → Γ ⊢ e ⦂ t + ------------ + → Γ ⊢ e ⦂ t' + + ⊢-∃ : ∀ {n} {Γ : Context n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ t₁ ⦂ `Set + → Γ , t₁ ⊢ t₂ ⦂ `Set + ----------------------- + → Γ ⊢ ∃[x⦂ t₁ ] t₂ ⦂ `Set + + ⊢-, : ∀ {n} {Γ : Context n} {e₁ e₂ : Term n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ e₁ ⦂ t₁ + → Γ ⊢ e₂ ⦂ t₂ [ e₁ ] + ----------------------- + → Γ ⊢ (e₁ `, e₂) ⦂ ∃[x⦂ t₁ ] t₂ + + ⊢-proj₁ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂ + → Γ ⊢ `proj₁ e ⦂ t₁ + + ⊢-proj₂ : ∀ {n} {Γ : Context n} {e : Term n} {t₁ : Term n} {t₂ : Term (suc n)} + → Γ ⊢ e ⦂ ∃[x⦂ t₁ ] t₂ + → Γ ⊢ `proj₂ e ⦂ t₂ [ `proj₁ e ] + + ⊢-≡ : ∀ {n} {Γ : Context n} {e₁ e₂ t : Term n} + → Γ ⊢ e₁ ⦂ t + → Γ ⊢ e₂ ⦂ t + ----------------------- + → Γ ⊢ (e₁ `≡ e₂) ⦂ `Set + + ⊢-refl : ∀ {n} {Γ : Context n} {e t : Term n} + → Γ ⊢ e ⦂ t + ------------------ + → Γ ⊢ `refl ⦂ e `≡ e + + ⊢-subst : ∀ {n} {Γ : Context n} {e₁ e₂ u₁ u₂ : Term n} {t' : Term n} {t : Term (suc n)} + → Γ , t' ⊢ t ⦂ `Set + → Γ ⊢ u₁ ⦂ t' + → Γ ⊢ u₂ ⦂ t' + → Γ ⊢ e₁ ⦂ (u₁ `≡ u₂) + → Γ ⊢ e₂ ⦂ t [ u₁ ] + ------------------------------ + → Γ ⊢ `subst t e₁ e₂ ⦂ t [ u₂ ] + +-- Extension + ⊢-Setn : ∀ {n} {Γ : Context n} {l} + → Γ ⊢ `Setn l ⦂ (`Setn (`lsuc l)) + + ⊢-Setω : ∀ {n} {Γ : Context n} {l} + → Γ ⊢ `Setω l ⦂ (`Setω (`lsuc l)) + + ⊢-lzero : ∀ {n} {Γ : Context n} + → Γ ⊢ `lzero ⦂ `Level + + ⊢-lsuc : ∀ {n} {Γ : Context n} {l} + → Γ ⊢ l ⦂ `Level + → Γ ⊢ `lsuc l ⦂ `Level + + ⊢-⊔ : ∀ {n} {Γ : Context n} {l₁ l₂} + → Γ ⊢ l₁ ⦂ `Level + → Γ ⊢ l₂ ⦂ `Level + → Γ ⊢ (l₁ `⊔ l₂) ⦂ `Level + + ⊢-Level : ∀ {n} {Γ : Context n} + → Γ ⊢ `Level ⦂ `Set + +cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v a b} → x ≡ y → u ≡ v → a ≡ b → f x u a ≡ f y v b +cong₃ f refl refl refl = refl diff --git a/SubjectReduction/SubjectReduction.agda b/SubjectReduction/SubjectReduction.agda new file mode 100644 index 0000000..14c6a68 --- /dev/null +++ b/SubjectReduction/SubjectReduction.agda @@ -0,0 +1,90 @@ +module univTypes.SubjectReduction.SubjectReduction where + +open import Data.Product renaming (_,_ to ⟨_,_⟩) +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning) +open import Data.Fin using (zero; suc) renaming (Fin to 𝔽) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.Util.Fin using (zero; suc) +open import univTypes.SubjectReduction.Specification +open import univTypes.SubjectReduction.Inversion using (invert-⊢λ; invert-⊢,; invert-⊢refl) +open import univTypes.SubjectReduction.SubstitutionPreservesTyping using (⊢sub; ⊢sub₁) +open import univTypes.SubjectReduction.ConversionProperties using (≈-sym; ≈σ-sub; ≈σ-sub₁; ≈→≈σ; ↪→≈; ≈-Γ-⊢₁; ≈-trans; ≈-sub; ≈-ren; ≈-refl) + +-- Subject Reduction + +type-two : ∀ {n} {Γ : Context n} {e : Term n} {x t} + → Γ ⊢ e ⦂ ∀[x⦂ x ] t + → Term _ +type-two {t = t} _ = t + +subject-reduction : ∀ {n} {Γ : Context n} {e e' t : Term n} + → Γ ⊢ e ⦂ t + → e ↪ e' + ---------- + → Γ ⊢ e' ⦂ t +subject-reduction (⊢-≈ t≈t₁ ⊢e) β-λ = ⊢-≈ t≈t₁ (subject-reduction ⊢e β-λ) +subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-λ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-λ e↪e')) +subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₁ e↪e')) +subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₂ e↪e')) +subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₁ e↪e')) +subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₂ e↪e')) +subject-reduction (⊢-λ ⊢e₁ ⊢e₂) (ξ-λ e₁↪e₁') = ⊢-λ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁') +subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₁ e₁↪e₁') = ⊢-· (subject-reduction ⊢e₁ e₁↪e₁') ⊢e₂ +subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₂ e₂↪e₂') = + ⊢-≈ (≈-sym (≈σ-sub {e = type-two ⊢e₁} (≈→≈σ (↪→≈ e₂↪e₂')))) (⊢-· ⊢e₁ (subject-reduction ⊢e₂ e₂↪e₂')) +subject-reduction (⊢-∀ ⊢t ⊢e) (ξ-∀₁ t↪t') = + ⊢-∀ (subject-reduction ⊢t t↪t') (≈-Γ-⊢₁ (↪→≈ t↪t') ⊢e) +subject-reduction (⊢-∀ ⊢e₁ ⊢e₂) (ξ-∀₂ e₁↪e₁') = ⊢-∀ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁') +subject-reduction (⊢-· ⊢e₁ ⊢e₂) β-λ with invert-⊢λ ⊢e₁ +... | ⟨ t₁' , ⟨ t₂' , ⟨ t₁≈t₁' , ⟨ t₂≈t₂' , ⟨ ⊢t₁' , Γ,t₁'⊢e₁⦂t₂' ⟩ ⟩ ⟩ ⟩ ⟩ + = ⊢sub (⊢sub₁ (⊢-≈ t₁≈t₁' ⊢e₂)) ⊢e₁⦂t₂ + where + ⊢e₁⦂t₂ = ⊢-≈ (≈-sym t₂≈t₂') Γ,t₁'⊢e₁⦂t₂' +subject-reduction (⊢-` x x₁) () +subject-reduction ⊢-Set () +subject-reduction (⊢-≈ x ⊢e) β-proj₁ = ⊢-≈ x (subject-reduction ⊢e β-proj₁) +subject-reduction (⊢-≈ x ⊢e) β-proj₂ = ⊢-≈ x (subject-reduction ⊢e β-proj₂) +subject-reduction (⊢-≈ x ⊢e) β-subst = ⊢-≈ x (subject-reduction ⊢e β-subst) +subject-reduction (⊢-≈ x ⊢e) (ξ-∃₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₁ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-∃₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₂ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-proj₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₁ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-proj₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₂ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-,₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₁ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-,₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₂ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-≡₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₁ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-≡₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₂ e↪e')) +subject-reduction (⊢-≈ t₁≈t ⊢e) (ξ-subst₁ t₂↪t') = ⊢-≈ t₁≈t (subject-reduction ⊢e (ξ-subst₁ t₂↪t')) +subject-reduction (⊢-≈ x ⊢e) (ξ-subst₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₂ e↪e')) +subject-reduction (⊢-≈ x ⊢e) (ξ-subst₃ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₃ e↪e')) +subject-reduction (⊢-∃ ⊢t₁ t₁⊢t₂) (ξ-∃₁ t₁↪t₁') + = ⊢-∃ (subject-reduction ⊢t₁ t₁↪t₁') (≈-Γ-⊢₁ (↪→≈ t₁↪t₁') t₁⊢t₂) +subject-reduction (⊢-∃ ⊢e ⊢e₁) (ξ-∃₂ e↪e') = ⊢-∃ ⊢e (subject-reduction ⊢e₁ e↪e') +subject-reduction (⊢-, {t₂ = t₂} ⊢l ⊢r) (ξ-,₁ l↪l') + = ⊢-, (subject-reduction ⊢l l↪l') + (⊢-≈ (≈σ-sub₁ {e = t₂} (↪→≈ l↪l')) ⊢r) +-- t₂ [ e₁ ] ≈ t₂ [ e₁' ] +subject-reduction (⊢-, ⊢l ⊢r) (ξ-,₂ r↪r') = ⊢-, ⊢l (subject-reduction ⊢r r↪r') +subject-reduction (⊢-proj₁ ⊢e) β-proj₁ with invert-⊢, ⊢e +... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩ + = ⊢e' +subject-reduction (⊢-proj₁ ⊢e) (ξ-proj₁ e↪e') = ⊢-proj₁ (subject-reduction ⊢e e↪e') +subject-reduction (⊢-proj₂ {t₂ = t'} ⊢e) β-proj₂ with invert-⊢, ⊢e +... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩ + = ⊢-≈ (≈σ-sub₁ {e = t'} (mk-≈ _ ↪*-refl (↪*-step β-proj₁ ↪*-refl))) ⊢e₂ +subject-reduction (⊢-proj₂ {e = e} {t₂ = t₂} ⊢e) (ξ-proj₂ e↪e') + = ⊢-≈ (≈-sym (≈σ-sub {e = t₂} (≈→≈σ (↪→≈ (ξ-proj₁ e↪e'))))) (⊢-proj₂ (subject-reduction ⊢e e↪e')) +subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₁ e↪e') = ⊢-≡ (subject-reduction ⊢e e↪e') ⊢e₁ +subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₂ e↪e') = ⊢-≡ ⊢e (subject-reduction ⊢e₁ e↪e') +subject-reduction (⊢-refl ⊢e) () +subject-reduction (⊢-subst {t = t} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) β-subst with invert-⊢refl ⊢≈ +... | u₁≈u₂ + = ⊢-≈ (≈σ-sub₁ {e = t} u₁≈u₂) ⊢t[u₁] +subject-reduction (⊢-subst {u₁ = u₁} {u₂ = u₂} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) (ξ-subst₁ t↪t') + = ⊢-≈ (≈-sym (≈-sub (0↦ u₂) (↪→≈ t↪t'))) (⊢-subst (subject-reduction ⊢t t↪t') ⊢u₁ ⊢u₂ ⊢≈ (⊢-≈ (≈-sub (0↦ u₁) (↪→≈ t↪t')) ⊢t[u₁])) +subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₂ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ (subject-reduction ⊢e₃ e↪e') ⊢e₄ +subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₃ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ (subject-reduction ⊢e₄ e↪e') diff --git a/SubjectReduction/SubstitutionPreservesTyping.agda b/SubjectReduction/SubstitutionPreservesTyping.agda new file mode 100644 index 0000000..b088f49 --- /dev/null +++ b/SubjectReduction/SubstitutionPreservesTyping.agda @@ -0,0 +1,125 @@ +module univTypes.SubjectReduction.SubstitutionPreservesTyping where + +open import Data.Product renaming (_,_ to ⟨_,_⟩) +open import Data.Sum +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Function using (_∘_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning) +open import Data.Fin using (zero; suc) renaming (Fin to 𝔽) +open import Relation.Nullary using (¬_) +open import Data.Empty using (⊥; ⊥-elim) + +open import univTypes.SubjectReduction.Specification +open import univTypes.SubjectReduction.ConversionProperties using (≈-ren; ≈-sub) +open import univTypes.SubjectReduction.Composition using (wk-extᵣ-fusion; swap-0↦-extᵣ-fusion; wk-extₛ-fusion; swap-0↦-extₛ-fusion; wk-0↦-fusion) + +open import univTypes.Util.Fin + +-- Renaming Typings + +infix 4 _⦂_⇒ᵣ_ + +_⦂_⇒ᵣ_ : ∀ {m n} → Ren m n → Context m → Context n → Set +ρ ⦂ Γ₁ ⇒ᵣ Γ₂ = ∀ x → lookup Γ₂ (ρ x) ≡ ren ρ (lookup Γ₁ x) + +⊢extᵣ : ∀ {m n t ρ} {Γ₁ : Context m} {Γ₂ : Context n} + → ρ ⦂ Γ₁ ⇒ᵣ Γ₂ + → extᵣ ρ ⦂ Γ₁ , t ⇒ᵣ Γ₂ , (ren ρ t) +⊢extᵣ {ρ = ρ} ⊢ρ zero = wk-extᵣ-fusion _ _ +⊢extᵣ ⊢ρ (suc x) rewrite ⊢ρ x = wk-extᵣ-fusion _ _ +type : ∀ {n} {Γ : Context n} {e t : Term n} → Γ ⊢ e ⦂ t → Term n +type {t = t} _ = t + +term : ∀ {n} {Γ : Context n} {e t : Term n} → Γ ⊢ e ⦂ t → Term n +term {e = e} _ = e + +∀-type : ∀ {n} {Γ : Context n} {e : Term n} {x t} + → Γ ⊢ e ⦂ ∀[x⦂ x ] t + → Term _ +∀-type {t = t} _ = t + +∃-type : ∀ {n} {Γ : Context n} {e : Term n} {x t} + → Γ ⊢ e ⦂ ∃[x⦂ x ] t + → Term _ +∃-type {t = t} _ = t + +sub-type : ∀ {n} {Γ : Context n} {e : Term n} {a b} + → Γ ⊢ e ⦂ a [ b ] + → Term _ +sub-type {a = a} _ = a + +≡→≈ : ∀ {n} {a b : Term n} → a ≡ b → a ≈ b +≡→≈ refl = mk-≈ _ ↪*-refl ↪*-refl + + + +⊢ren : ∀ {m n} {Γ₁ : Context m} {Γ₂ : Context n} {e t ρ} + → ρ ⦂ Γ₁ ⇒ᵣ Γ₂ + → Γ₁ ⊢ e ⦂ t + ------------------------ + → Γ₂ ⊢ ren ρ e ⦂ ren ρ t +⊢ren ⊢ρ ⊢-Set = ⊢-Set +⊢ren ⊢ρ (⊢-refl ⊢-e) = ⊢-refl (⊢ren ⊢ρ ⊢-e) +⊢ren ⊢ρ (⊢-` x refl) = ⊢-` _ (⊢ρ x) +⊢ren ⊢ρ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (⊢ren ⊢ρ ⊢l) (⊢ren ⊢ρ ⊢r) +⊢ren {m} {n} {Γ₁} {Γ₂} {e} { ∃[x⦂ _ ] a } {ρ} ⊢ρ (⊢-, ⊢l ⊢r) + = ⊢-, (⊢ren ⊢ρ ⊢l) (⊢-≈ (≡→≈ (sym (swap-0↦-extᵣ-fusion ρ (term ⊢l) a) )) (⊢ren {Γ₂ = Γ₂} ⊢ρ ⊢r)) +⊢ren ⊢ρ (⊢-≈ t₁≈t ⊢e) = ⊢-≈ (≈-ren _ t₁≈t) (⊢ren ⊢ρ ⊢e) +⊢ren ⊢ρ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (⊢ren ⊢ρ ⊢e₁) (⊢ren (⊢extᵣ ⊢ρ) ⊢e₂) +⊢ren ⊢ρ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (⊢ren ⊢ρ ⊢e₁) (⊢ren (⊢extᵣ ⊢ρ) ⊢e₂) +⊢ren ⊢ρ (⊢-λ ⊢t t⊢e) = ⊢-λ (⊢ren ⊢ρ ⊢t) (⊢ren (⊢extᵣ ⊢ρ) t⊢e) +⊢ren {ρ = ρ} ⊢ρ (⊢-· ⊢l ⊢r) = ⊢-≈ (≡→≈ ((swap-0↦-extᵣ-fusion ρ (term ⊢r) (∀-type ⊢l)))) (⊢-· (⊢ren ⊢ρ ⊢l) (⊢ren ⊢ρ ⊢r)) +⊢ren ⊢ρ (⊢-proj₁ ⊢e) = ⊢-proj₁ (⊢ren ⊢ρ ⊢e) +⊢ren {m} {n} {Γ₁} {Γ₂} {e} {t} {ρ} ⊢ρ (⊢-proj₂ ⊢e) + = ⊢-≈ (≡→≈ (swap-0↦-extᵣ-fusion ρ (`proj₁ (term ⊢e)) (∃-type ⊢e))) (⊢-proj₂ (⊢ren ⊢ρ ⊢e)) +⊢ren {m} {n} {Γ₁} {Γ₂} {e} {t} {ρ} ⊢ρ x@(⊢-subst {t = t*} t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁]) + = ⊢-≈ (≡→≈ (swap-0↦-extᵣ-fusion ρ (term ⊢u₂) t* )) + (⊢-subst (⊢ren (⊢extᵣ ⊢ρ) t'⊢t) (⊢ren ⊢ρ ⊢u₁) (⊢ren ⊢ρ ⊢u₂) (⊢ren ⊢ρ ⊢≡) + (⊢-≈ (≡→≈ (sym (swap-0↦-extᵣ-fusion ρ (term ⊢u₁) (t*)))) (⊢ren ⊢ρ ⊢t[u₁]))) + +⊢wk : ∀ {n} {Γ : Context n} {t : Term n} + → wk ⦂ Γ ⇒ᵣ (Γ , t) +⊢wk x = refl + +-- Substitution Typings + +infix 4 _⦂_⇒ₛ_ + +_⦂_⇒ₛ_ : ∀ {m n} → Sub m n → Context m → Context n → Set +σ ⦂ Γ₁ ⇒ₛ Γ₂ = ∀ x → Γ₂ ⊢ σ x ⦂ sub σ (lookup Γ₁ x) + +⊢extₛ : ∀ {m n σ} {t : Term m} {Γ₁ : Context m} {Γ₂ : Context n} + → σ ⦂ Γ₁ ⇒ₛ Γ₂ + → extₛ σ ⦂ Γ₁ , t ⇒ₛ Γ₂ , (sub σ t) +⊢extₛ {σ = σ} {t = t} ⊢σ zero = ⊢-` zero (wk-extₛ-fusion σ t) +⊢extₛ {σ = σ} {Γ₁ = Γ₁} ⊢σ (suc x) = ⊢-≈ (≡→≈ (wk-extₛ-fusion σ (lookup Γ₁ x))) (⊢ren (λ _ → refl) (⊢σ x)) + +⊢sub : ∀ {m n} {Γ₁ : Context m} {Γ₂ : Context n} {e t σ} + → σ ⦂ Γ₁ ⇒ₛ Γ₂ + → Γ₁ ⊢ e ⦂ t + ------------------------ + → Γ₂ ⊢ sub σ e ⦂ sub σ t +⊢sub ⊢σ ⊢-Set = ⊢-Set +⊢sub ⊢σ (⊢-` x refl) = ⊢σ x +⊢sub ⊢σ (⊢-refl e) = ⊢-refl (⊢sub ⊢σ e) +⊢sub {σ = σ} ⊢σ (⊢-· ⊢l ⊢r) = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (term ⊢r) (∀-type ⊢l))) (⊢-· (⊢sub ⊢σ ⊢l) (⊢sub ⊢σ ⊢r)) +⊢sub ⊢σ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (⊢sub ⊢σ ⊢l) (⊢sub ⊢σ ⊢r) +⊢sub {σ = σ} ⊢σ (⊢-, {e₁ = e₁} {t₂ = t₂} ⊢l ⊢r) + = ⊢-, (⊢sub ⊢σ ⊢l) (⊢-≈ (≡→≈ (sym (swap-0↦-extₛ-fusion σ e₁ t₂))) (⊢sub ⊢σ ⊢r)) +⊢sub {σ = σ} ⊢σ (⊢-≈ t'≈t ⊢e) = ⊢-≈ (≈-sub σ t'≈t) (⊢sub ⊢σ ⊢e) +⊢sub ⊢σ (⊢-λ ⊢e₁ ⊢e₂) = ⊢-λ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂) +⊢sub ⊢σ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂) +⊢sub ⊢σ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂) +⊢sub ⊢σ (⊢-proj₁ e) = ⊢-proj₁ (⊢sub ⊢σ e) +⊢sub {m} {n} {Γ₁} {Γ₂} {e} {t} {σ} ⊢σ (⊢-proj₂ {e = a} {t₂ = t₂} ⊢e) + = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (`proj₁ a) t₂)) (⊢-proj₂ (⊢sub ⊢σ ⊢e)) +⊢sub {m} {n} {Γ₁} {Γ₂} {e} {t} {σ} ⊢σ (⊢-subst {t = t*} t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁]) + = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (term ⊢u₂) t* )) + (⊢-subst (⊢sub (⊢extₛ ⊢σ) t'⊢t) (⊢sub ⊢σ ⊢u₁) (⊢sub ⊢σ ⊢u₂) (⊢sub ⊢σ ⊢≡) + (⊢-≈ (≡→≈ (sym (swap-0↦-extₛ-fusion σ (term ⊢u₁) (t*)))) (⊢sub ⊢σ ⊢t[u₁]))) + +⊢sub₁ : ∀ {n} {Γ : Context n} {e : Term n} {t} + → Γ ⊢ e ⦂ t + → 0↦ e ⦂ Γ , t ⇒ₛ Γ +⊢sub₁ {n} {Γ} {e} {t} ⊢e zero = ⊢-≈ (≡→≈ (sym (wk-0↦-fusion e t))) ⊢e +⊢sub₁ {n} {Γ} {e} {t} ⊢e (suc x) = ⊢-` x (sym (wk-0↦-fusion e (lookup Γ x) )) diff --git a/Util/Fin.agda b/Util/Fin.agda new file mode 100644 index 0000000..fafe27e --- /dev/null +++ b/Util/Fin.agda @@ -0,0 +1,10 @@ +module univTypes.Util.Fin where + +open import Data.Nat using (ℕ; suc; zero) + +-- `Fin n` is a type with `n` elements. +-- You can think of `Fin n` as the type of all natural numbers less than `n`. + +data Fin : ℕ → Set where + zero : ∀ {n} → Fin (suc n) + suc : ∀ {n} → (i : Fin n) → Fin (suc n)