570 lines
27 KiB
Agda
570 lines
27 KiB
Agda
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') ⟩ ⟩
|