some progress on confluence
This commit is contained in:
Jeremy Siek
parent
2e999b167e
commit
b4c8986009
3 changed files with 451 additions and 202 deletions
|
|
@ -29,208 +29,6 @@ open import Function using (_∘_)
|
|||
\end{code}
|
||||
|
||||
|
||||
## Lemmas about Renaming and Substitution
|
||||
|
||||
\begin{code}
|
||||
same-rename : ∀{Γ Δ} → Rename Γ Δ → Rename Γ Δ → Set
|
||||
same-rename{Γ}{Δ} σ σ' = ∀{A}{x : Γ ∋ A} → σ x ≡ σ' x
|
||||
|
||||
same-rename-ext : ∀{Γ Δ}{σ σ' : Rename Γ Δ}
|
||||
→ same-rename σ σ'
|
||||
→ same-rename (ext σ {B = ★}) (ext σ' )
|
||||
same-rename-ext ss {x = Z} = refl
|
||||
same-rename-ext ss {x = S x} = cong S_ ss
|
||||
|
||||
rename-equal : ∀{Γ Δ}{ρ ρ' : Rename Γ Δ}{M : Γ ⊢ ★}
|
||||
→ same-rename ρ ρ'
|
||||
→ rename ρ M ≡ rename ρ' M
|
||||
rename-equal {M = ` x} s = cong `_ s
|
||||
rename-equal {ρ = ρ}{ρ' = ρ'}{M = ƛ N} s =
|
||||
cong ƛ_ (rename-equal {ρ = ext ρ}{ρ' = ext ρ'}{M = N} (same-rename-ext s))
|
||||
rename-equal {M = L · M} s = cong₂ _·_ (rename-equal s) (rename-equal s)
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
same-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
|
||||
same-subst{Γ}{Δ} σ σ' = ∀{A}{x : Γ ∋ A} → σ x ≡ σ' x
|
||||
|
||||
same-subst-ext : ∀{Γ Δ}{σ σ' : Subst Γ Δ}{B}
|
||||
→ same-subst σ σ'
|
||||
→ same-subst (exts σ {B = B}) (exts σ' )
|
||||
same-subst-ext ss {x = Z} = refl
|
||||
same-subst-ext ss {x = S x} = cong (rename (λ {A} → S_)) ss
|
||||
|
||||
subst-equal : ∀{Γ Δ}{σ σ' : Subst Γ Δ}{M : Γ ⊢ ★}
|
||||
→ same-subst σ σ'
|
||||
→ subst σ M ≡ subst σ' M
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {` x} ss = ss
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {ƛ M} ss =
|
||||
let ih = subst-equal {Γ = Γ , ★} {Δ = Δ , ★}
|
||||
{σ = exts σ}{σ' = exts σ'} {M = M}
|
||||
(λ {x}{A} → same-subst-ext {Γ}{Δ}{σ}{σ'} ss {x}{A}) in
|
||||
cong ƛ_ ih
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {L · M} ss =
|
||||
let ih1 = subst-equal {Γ} {Δ} {σ} {σ'} {L} ss in
|
||||
let ih2 = subst-equal {Γ} {Δ} {σ} {σ'} {M} ss in
|
||||
cong₂ _·_ ih1 ih2
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
compose-ext : ∀{Γ Δ Σ}{ρ : Rename Δ Σ} {ρ' : Rename Γ Δ} {A B} {x : Γ , B ∋ A}
|
||||
→ ((ext ρ) ∘ (ext ρ')) x ≡ ext (ρ ∘ ρ') x
|
||||
compose-ext {x = Z} = refl
|
||||
compose-ext {x = S x} = refl
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
compose-rename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ' : Rename Γ Δ}
|
||||
→ rename ρ (rename ρ' M) ≡ rename (ρ ∘ ρ') M
|
||||
compose-rename {M = ` x} = refl
|
||||
compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ'} = cong ƛ_ G
|
||||
where
|
||||
IH : rename ( ext ρ) (rename ( ext ρ') N) ≡ rename ((ext ρ) ∘ (ext ρ')) N
|
||||
IH = compose-rename{Γ , ★}{Δ , ★}{Σ , ★}{★}{N}{ext ρ}{ext ρ'}
|
||||
G : rename (ext ρ) (rename (ext ρ') N) ≡ rename (ext (ρ ∘ ρ')) N
|
||||
G =
|
||||
begin
|
||||
rename (ext ρ) (rename (ext ρ') N)
|
||||
≡⟨ IH ⟩
|
||||
rename ((ext ρ) ∘ (ext ρ')) N
|
||||
≡⟨ rename-equal compose-ext ⟩
|
||||
rename (ext (ρ ∘ ρ')) N
|
||||
∎
|
||||
compose-rename {M = L · M} =
|
||||
cong₂ _·_ compose-rename compose-rename
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ}
|
||||
{ρ : ∀{Γ} → Rename Γ (Γ , ★)}
|
||||
→ (∀{x : Γ ∋ ★} → exts σ {B = ★} (ρ x) ≡ rename ρ (σ x))
|
||||
→ subst (exts σ {B = ★}) (rename ρ M) ≡ rename ρ (subst σ M)
|
||||
commute-subst-rename {M = ` x} r = r
|
||||
commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r = cong ƛ_ IH
|
||||
where
|
||||
ρ' : ∀ {Γ} → Rename Γ (Γ , ★)
|
||||
ρ' {∅} = λ ()
|
||||
ρ' {Γ , ★} = ext ρ
|
||||
|
||||
H : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
|
||||
H {Z} = refl
|
||||
H {S x} =
|
||||
begin
|
||||
rename S_ (exts σ (ρ x))
|
||||
≡⟨ cong (rename S_) r ⟩
|
||||
rename S_ (rename ρ (σ x))
|
||||
≡⟨ compose-rename ⟩
|
||||
rename (S_ ∘ ρ) (σ x)
|
||||
≡⟨ rename-equal (λ {A} {x₁} → refl) ⟩
|
||||
rename ((ext ρ) ∘ S_) (σ x)
|
||||
≡⟨ sym compose-rename ⟩
|
||||
rename (ext ρ) (rename S_ (σ x))
|
||||
∎
|
||||
IH : subst (exts (exts σ)) (rename (ext ρ) N) ≡
|
||||
rename (ext ρ) (subst (exts σ) N)
|
||||
IH = commute-subst-rename{Γ , ★}{Δ , ★}{N}
|
||||
{exts σ}{ρ = ρ'} (λ {x} → H {x})
|
||||
|
||||
commute-subst-rename {M = L · M}{ρ = ρ} r =
|
||||
cong₂ _·_ (commute-subst-rename{M = L}{ρ = ρ} r)
|
||||
(commute-subst-rename{M = M}{ρ = ρ} r)
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
subst-exts : ∀{Γ Δ Δ'}{A}{x : Γ , ★ ∋ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Δ'}
|
||||
→ ((subst (exts σ₂)) ∘ (exts σ₁)) x ≡ exts ((subst σ₂) ∘ σ₁) x
|
||||
subst-exts {x = Z} = refl
|
||||
subst-exts {A = ★}{x = S x}{σ₁}{σ₂} = G
|
||||
where
|
||||
G : ((subst (exts σ₂)) ∘ exts σ₁) (S x) ≡ rename S_ (((subst σ₂) ∘ σ₁) x)
|
||||
G =
|
||||
begin
|
||||
((subst (exts σ₂)) ∘ exts σ₁) (S x)
|
||||
≡⟨⟩
|
||||
subst (exts σ₂) (rename S_ (σ₁ x))
|
||||
≡⟨ commute-subst-rename{M = σ₁ x}{σ = σ₂}{ρ = S_} (λ {x₁} → refl) ⟩
|
||||
rename S_ (subst σ₂ (σ₁ x))
|
||||
≡⟨⟩
|
||||
rename S_ (((subst σ₂) ∘ σ₁) x)
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
subst-subst : ∀{Γ Δ Σ}{M : Γ ⊢ ★} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
|
||||
→ ((subst σ₂) ∘ (subst σ₁)) M ≡ subst (subst σ₂ ∘ σ₁) M
|
||||
subst-subst {M = ` x} = refl
|
||||
subst-subst {Γ}{Δ}{Σ}{ƛ N}{σ₁}{σ₂} = G
|
||||
where
|
||||
G : ((subst σ₂) ∘ subst σ₁) (ƛ N) ≡ (ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
G =
|
||||
begin
|
||||
((subst σ₂) ∘ subst σ₁) (ƛ N)
|
||||
≡⟨⟩
|
||||
ƛ ((subst (exts σ₂)) ∘ (subst (exts σ₁))) N
|
||||
≡⟨ cong ƛ_ (subst-subst{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩
|
||||
ƛ subst ((subst (exts σ₂)) ∘ (exts σ₁)) N
|
||||
≡⟨ cong ƛ_ (subst-equal{M = N} (λ {A}{x} → subst-exts{x = x})) ⟩
|
||||
(ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
∎
|
||||
subst-subst {M = L · M} = cong₂ _·_ (subst-subst{M = L}) (subst-subst{M = M})
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
rename-subst : ∀{Γ Δ Δ'}{M : Γ ⊢ ★}{ρ : Rename Γ Δ}{σ : Subst Δ Δ'}
|
||||
→ ((subst σ) ∘ (rename ρ)) M ≡ subst (σ ∘ ρ) M
|
||||
rename-subst {M = ` x} = refl
|
||||
rename-subst {Γ}{Δ}{Δ'}{M = ƛ M}{ρ}{σ} =
|
||||
let ih : subst (exts σ) (rename (ext ρ) M)
|
||||
≡ subst ((exts σ) ∘ ext ρ) M
|
||||
ih = rename-subst {M = M}{ρ = ext ρ}{σ = exts σ} in
|
||||
cong ƛ_ g
|
||||
where
|
||||
ss : same-subst ((exts σ) ∘ (ext ρ)) (exts (σ ∘ ρ))
|
||||
ss {A} {Z} = refl
|
||||
ss {A} {S x} = refl
|
||||
h : subst ((exts σ) ∘ (ext ρ)) M ≡ subst (exts (σ ∘ ρ)) M
|
||||
h = subst-equal{Γ , ★}{Δ = Δ' , ★}{σ = ((exts σ) ∘ (ext ρ))}
|
||||
{σ' = (exts (σ ∘ ρ))}{M = M} (λ {A} {x} → ss{A}{x})
|
||||
g : subst (exts σ) (rename (ext ρ) M)
|
||||
≡ subst (exts (σ ∘ ρ)) M
|
||||
g =
|
||||
begin
|
||||
subst (exts σ) (rename (ext ρ) M)
|
||||
≡⟨ rename-subst {M = M}{ρ = ext ρ}{σ = exts σ} ⟩
|
||||
subst ((exts σ) ∘ ext ρ) M
|
||||
≡⟨ h ⟩
|
||||
subst (exts (σ ∘ ρ)) M
|
||||
∎
|
||||
rename-subst {M = L · M} =
|
||||
cong₂ _·_ (rename-subst{M = L}) (rename-subst{M = M})
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
is-id-subst : ∀{Γ} → Subst Γ Γ → Set
|
||||
is-id-subst {Γ} σ = ∀{x : Γ ∋ ★} → σ x ≡ ` x
|
||||
|
||||
is-id-exts : ∀{Γ} {σ : Subst Γ Γ}
|
||||
→ is-id-subst σ
|
||||
→ is-id-subst (exts σ {B = ★})
|
||||
is-id-exts id {Z} = refl
|
||||
is-id-exts{Γ}{σ} id {S x} rewrite id {x} = refl
|
||||
|
||||
subst-id : ∀{Γ} {M : Γ ⊢ ★} {σ : Subst Γ Γ}
|
||||
→ is-id-subst σ
|
||||
→ subst σ M ≡ M
|
||||
subst-id {M = ` x} {σ} id = id
|
||||
subst-id {M = ƛ M} {σ} id = cong ƛ_ (subst-id (is-id-exts id))
|
||||
subst-id {M = L · M} {σ} id = cong₂ _·_ (subst-id id) (subst-id id)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Logical Relation between CBN Closures and Terms
|
||||
|
||||
|
|
|
|||
228
extra/extra/Confluence.lagda
Normal file
228
extra/extra/Confluence.lagda
Normal file
|
|
@ -0,0 +1,228 @@
|
|||
\begin{code}
|
||||
module extra.Confluence where
|
||||
\end{code}
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
open import extra.Substitution
|
||||
open import plfa.Untyped
|
||||
renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to start_; _∎ to _[])
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
|
||||
{- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) -}
|
||||
\end{code}
|
||||
|
||||
## Reduction without the restrictions
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ₁ : ∀ {Γ} {L L′ M : Γ ⊢ ★}
|
||||
→ L —→ L′
|
||||
----------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ₂ : ∀ {Γ} {L M M′ : Γ ⊢ ★}
|
||||
→ M —→ M′
|
||||
----------------
|
||||
→ L · M —→ L · M′
|
||||
|
||||
β : ∀ {Γ} {N : Γ , ★ ⊢ ★} {M : Γ ⊢ ★}
|
||||
---------------------------------
|
||||
→ (ƛ N) · M —→ N [ M ]
|
||||
|
||||
ζ : ∀ {Γ} {N N′ : Γ , ★ ⊢ ★}
|
||||
→ N —→ N′
|
||||
-----------
|
||||
→ ƛ N —→ ƛ N′
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_∎ : ∀ {Γ A} (M : Γ ⊢ A)
|
||||
--------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
→ M —↠ N
|
||||
---------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
—↠-trans : ∀{Γ}{L M N : Γ ⊢ ★}
|
||||
→ L —↠ M
|
||||
→ M —↠ N
|
||||
→ L —↠ N
|
||||
—↠-trans (M ∎) mn = mn
|
||||
—↠-trans (L —→⟨ r ⟩ lm) mn = L —→⟨ r ⟩ (—↠-trans lm mn)
|
||||
\end{code}
|
||||
|
||||
## Congruences
|
||||
|
||||
\begin{code}
|
||||
abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★}
|
||||
→ N —↠ N'
|
||||
----------
|
||||
→ ƛ N —↠ ƛ N'
|
||||
abs-cong (M ∎) = ƛ M ∎
|
||||
abs-cong (L —→⟨ r ⟩ rs) = ƛ L —→⟨ ζ r ⟩ abs-cong rs
|
||||
|
||||
appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★}
|
||||
→ L —↠ L'
|
||||
---------------
|
||||
→ L · M —↠ L' · M
|
||||
appL-cong {Γ}{L}{L'}{M} (L ∎) = L · M ∎
|
||||
appL-cong {Γ}{L}{L'}{M} (L —→⟨ r ⟩ rs) = L · M —→⟨ ξ₁ r ⟩ appL-cong rs
|
||||
|
||||
appR-cong : ∀ {Γ} {L M M' : Γ ⊢ ★}
|
||||
→ M —↠ M'
|
||||
---------------
|
||||
→ L · M —↠ L · M'
|
||||
appR-cong {Γ}{L}{M}{M'} (M ∎) = L · M ∎
|
||||
appR-cong {Γ}{L}{M}{M'} (M —→⟨ r ⟩ rs) = L · M —→⟨ ξ₂ r ⟩ appR-cong rs
|
||||
\end{code}
|
||||
|
||||
## Parallel Reduction
|
||||
|
||||
\begin{code}
|
||||
infix 2 _⇒_
|
||||
|
||||
data _⇒_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
pvar : ∀{Γ A}{x : Γ ∋ A}
|
||||
---------
|
||||
→ (` x) ⇒ (` x)
|
||||
|
||||
pabs : ∀{Γ}{N N' : Γ , ★ ⊢ ★}
|
||||
→ N ⇒ N'
|
||||
----------
|
||||
→ ƛ N ⇒ ƛ N'
|
||||
|
||||
papp : ∀{Γ}{L L' M M' : Γ ⊢ ★}
|
||||
→ L ⇒ L' → M ⇒ M'
|
||||
-----------------
|
||||
→ L · M ⇒ L' · M'
|
||||
|
||||
pbeta : ∀{Γ}{N N' : Γ , ★ ⊢ ★}{M M' : Γ ⊢ ★}
|
||||
→ N ⇒ N' → M ⇒ M'
|
||||
-----------------------
|
||||
→ (ƛ N) · M ⇒ N' [ M' ]
|
||||
\end{code}
|
||||
|
||||
## Proof of Confluence
|
||||
|
||||
\begin{code}
|
||||
par-refl : ∀{Γ A}{M : Γ ⊢ A} → M ⇒ M
|
||||
par-refl {Γ} {A} {` x} = pvar
|
||||
par-refl {Γ} {★} {ƛ N} = pabs par-refl
|
||||
par-refl {Γ} {★} {L · M} = papp par-refl par-refl
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
beta-par : ∀{Γ A}{M N : Γ ⊢ A}
|
||||
→ M —→ N
|
||||
------
|
||||
→ M ⇒ N
|
||||
beta-par {Γ} {★} {L · M} (ξ₁ r) =
|
||||
papp (beta-par {M = L} r) par-refl
|
||||
beta-par {Γ} {★} {L · M} (ξ₂ r) =
|
||||
papp par-refl (beta-par {M = M} r)
|
||||
beta-par {Γ} {★} {(ƛ N) · M} β =
|
||||
pbeta par-refl par-refl
|
||||
beta-par {Γ} {★} {ƛ N} (ζ r) =
|
||||
pabs (beta-par r)
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
par-beta : ∀{Γ A}{M N : Γ ⊢ A}
|
||||
→ M ⇒ N
|
||||
------
|
||||
→ M —↠ N
|
||||
par-beta {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) ∎
|
||||
par-beta {Γ} {★} {ƛ N} (pabs p) =
|
||||
abs-cong (par-beta p)
|
||||
par-beta {Γ} {★} {L · M} (papp p₁ p₂) =
|
||||
—↠-trans (appL-cong{M = M} (par-beta p₁)) (appR-cong (par-beta p₂))
|
||||
par-beta {Γ} {★} {(ƛ N) · M} (pbeta{N' = N'}{M' = M'} p₁ p₂) =
|
||||
let ih₁ = par-beta p₁ in
|
||||
let ih₂ = par-beta p₂ in
|
||||
let a : (ƛ N) · M —↠ (ƛ N') · M
|
||||
a = appL-cong{M = M} (abs-cong ih₁) in
|
||||
let b : (ƛ N') · M —↠ (ƛ N') · M'
|
||||
b = appR-cong{L = ƛ N'} ih₂ in
|
||||
let c = (ƛ N') · M' —→⟨ β ⟩ N' [ M' ] ∎ in
|
||||
—↠-trans (—↠-trans a b) c
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
Rename : Context → Context → Set
|
||||
Rename Γ Δ = ∀{A} → Γ ∋ A → Δ ∋ A
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
Subst : Context → Context → Set
|
||||
Subst Γ Δ = ∀{A} → Γ ∋ A → Δ ⊢ A
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
par-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
|
||||
par-subst {Γ}{Δ} σ₁ σ₂ = ∀{A}{x : Γ ∋ A} → σ₁ x ⇒ σ₂ x
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
rename-subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{ρ : Rename Γ Δ }
|
||||
→ (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ])
|
||||
rename-subst-commute {Γ}{Δ}{N}{M}{ρ} =
|
||||
{-
|
||||
let x = commute-subst-rename{σ = subst-zero M}{ρ = ρ} ? in
|
||||
-}
|
||||
{!!}
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
par-rename : ∀{Γ Δ A} {ρ : Rename Γ Δ} {M M' : Γ ⊢ A}
|
||||
→ M ⇒ M'
|
||||
------------------------
|
||||
→ rename ρ M ⇒ rename ρ M'
|
||||
par-rename pvar = pvar
|
||||
par-rename (pabs p) = pabs (par-rename p)
|
||||
par-rename (papp p₁ p₂) = papp (par-rename p₁) (par-rename p₂)
|
||||
par-rename {Γ}{Δ}{A}{ρ} (pbeta{Γ}{N}{N'}{M}{M'} p₁ p₂)
|
||||
with pbeta (par-rename{ρ = ext ρ} p₁) (par-rename{ρ = ρ} p₂)
|
||||
... | G rewrite rename-subst-commute{Γ}{Δ}{N'}{M'}{ρ} = G
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
subst-par : ∀{Γ Δ A} {σ₁ σ₂ : Subst Γ Δ} {M M' : Γ ⊢ A}
|
||||
→ par-subst σ₁ σ₂ → M ⇒ M'
|
||||
--------------------------
|
||||
→ subst σ₁ M ⇒ subst σ₂ M'
|
||||
subst-par {Γ} {Δ} {A} {σ₁} {σ₂} {` x} s pvar = s
|
||||
subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {ƛ N} s (pabs p) =
|
||||
let ih = subst-par {σ₁ = exts σ₁}{σ₂ = exts σ₂} {!!} p in
|
||||
pabs {!!}
|
||||
where
|
||||
H : par-subst (exts σ₁ {B = ★}) (exts σ₂)
|
||||
H {★} {Z} = pvar
|
||||
H {A} {S x} = {!!}
|
||||
|
||||
subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {L · M} s (papp p p₁) = {!!}
|
||||
subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {(ƛ N) · M} s (pbeta p p₁) = {!!}
|
||||
\end{code}
|
||||
223
extra/extra/Substitution.lagda
Normal file
223
extra/extra/Substitution.lagda
Normal file
|
|
@ -0,0 +1,223 @@
|
|||
\begin{code}
|
||||
module extra.Substitution where
|
||||
\end{code}
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
open import plfa.Untyped
|
||||
using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst;
|
||||
ext; exts; _[_]; subst-zero)
|
||||
renaming (_∎ to _[])
|
||||
open import plfa.Denotational using (Rename)
|
||||
open import plfa.Soundness using (Subst)
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Function using (_∘_)
|
||||
\end{code}
|
||||
|
||||
## Properties of renaming and substitution
|
||||
|
||||
|
||||
\begin{code}
|
||||
same-rename : ∀{Γ Δ} → Rename Γ Δ → Rename Γ Δ → Set
|
||||
same-rename{Γ}{Δ} σ σ' = ∀{A}{x : Γ ∋ A} → σ x ≡ σ' x
|
||||
|
||||
same-rename-ext : ∀{Γ Δ}{σ σ' : Rename Γ Δ}
|
||||
→ same-rename σ σ'
|
||||
→ same-rename (ext σ {B = ★}) (ext σ' )
|
||||
same-rename-ext ss {x = Z} = refl
|
||||
same-rename-ext ss {x = S x} = cong S_ ss
|
||||
|
||||
rename-equal : ∀{Γ Δ}{ρ ρ' : Rename Γ Δ}{M : Γ ⊢ ★}
|
||||
→ same-rename ρ ρ'
|
||||
→ rename ρ M ≡ rename ρ' M
|
||||
rename-equal {M = ` x} s = cong `_ s
|
||||
rename-equal {ρ = ρ}{ρ' = ρ'}{M = ƛ N} s =
|
||||
cong ƛ_ (rename-equal {ρ = ext ρ}{ρ' = ext ρ'}{M = N} (same-rename-ext s))
|
||||
rename-equal {M = L · M} s = cong₂ _·_ (rename-equal s) (rename-equal s)
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
same-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
|
||||
same-subst{Γ}{Δ} σ σ' = ∀{A}{x : Γ ∋ A} → σ x ≡ σ' x
|
||||
|
||||
same-subst-ext : ∀{Γ Δ}{σ σ' : Subst Γ Δ}{B}
|
||||
→ same-subst σ σ'
|
||||
→ same-subst (exts σ {B = B}) (exts σ' )
|
||||
same-subst-ext ss {x = Z} = refl
|
||||
same-subst-ext ss {x = S x} = cong (rename (λ {A} → S_)) ss
|
||||
|
||||
subst-equal : ∀{Γ Δ}{σ σ' : Subst Γ Δ}{M : Γ ⊢ ★}
|
||||
→ same-subst σ σ'
|
||||
→ subst σ M ≡ subst σ' M
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {` x} ss = ss
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {ƛ M} ss =
|
||||
let ih = subst-equal {Γ = Γ , ★} {Δ = Δ , ★}
|
||||
{σ = exts σ}{σ' = exts σ'} {M = M}
|
||||
(λ {x}{A} → same-subst-ext {Γ}{Δ}{σ}{σ'} ss {x}{A}) in
|
||||
cong ƛ_ ih
|
||||
subst-equal {Γ} {Δ} {σ} {σ'} {L · M} ss =
|
||||
let ih1 = subst-equal {Γ} {Δ} {σ} {σ'} {L} ss in
|
||||
let ih2 = subst-equal {Γ} {Δ} {σ} {σ'} {M} ss in
|
||||
cong₂ _·_ ih1 ih2
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
compose-ext : ∀{Γ Δ Σ}{ρ : Rename Δ Σ} {ρ' : Rename Γ Δ} {A B} {x : Γ , B ∋ A}
|
||||
→ ((ext ρ) ∘ (ext ρ')) x ≡ ext (ρ ∘ ρ') x
|
||||
compose-ext {x = Z} = refl
|
||||
compose-ext {x = S x} = refl
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
compose-rename : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A}{ρ : Rename Δ Σ}{ρ' : Rename Γ Δ}
|
||||
→ rename ρ (rename ρ' M) ≡ rename (ρ ∘ ρ') M
|
||||
compose-rename {M = ` x} = refl
|
||||
compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ'} = cong ƛ_ G
|
||||
where
|
||||
IH : rename ( ext ρ) (rename ( ext ρ') N) ≡ rename ((ext ρ) ∘ (ext ρ')) N
|
||||
IH = compose-rename{Γ , ★}{Δ , ★}{Σ , ★}{★}{N}{ext ρ}{ext ρ'}
|
||||
G : rename (ext ρ) (rename (ext ρ') N) ≡ rename (ext (ρ ∘ ρ')) N
|
||||
G =
|
||||
begin
|
||||
rename (ext ρ) (rename (ext ρ') N)
|
||||
≡⟨ IH ⟩
|
||||
rename ((ext ρ) ∘ (ext ρ')) N
|
||||
≡⟨ rename-equal compose-ext ⟩
|
||||
rename (ext (ρ ∘ ρ')) N
|
||||
∎
|
||||
compose-rename {M = L · M} =
|
||||
cong₂ _·_ compose-rename compose-rename
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
commute-subst-rename : ∀{Γ Δ}{M : Γ ⊢ ★}{σ : Subst Γ Δ}
|
||||
{ρ : ∀{Γ} → Rename Γ (Γ , ★)}
|
||||
→ (∀{x : Γ ∋ ★} → exts σ {B = ★} (ρ x) ≡ rename ρ (σ x))
|
||||
→ subst (exts σ {B = ★}) (rename ρ M) ≡ rename ρ (subst σ M)
|
||||
commute-subst-rename {M = ` x} r = r
|
||||
commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r = cong ƛ_ IH
|
||||
where
|
||||
ρ' : ∀ {Γ} → Rename Γ (Γ , ★)
|
||||
ρ' {∅} = λ ()
|
||||
ρ' {Γ , ★} = ext ρ
|
||||
|
||||
H : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
|
||||
H {Z} = refl
|
||||
H {S x} =
|
||||
begin
|
||||
rename S_ (exts σ (ρ x))
|
||||
≡⟨ cong (rename S_) r ⟩
|
||||
rename S_ (rename ρ (σ x))
|
||||
≡⟨ compose-rename ⟩
|
||||
rename (S_ ∘ ρ) (σ x)
|
||||
≡⟨ rename-equal (λ {A} {x₁} → refl) ⟩
|
||||
rename ((ext ρ) ∘ S_) (σ x)
|
||||
≡⟨ sym compose-rename ⟩
|
||||
rename (ext ρ) (rename S_ (σ x))
|
||||
∎
|
||||
IH : subst (exts (exts σ)) (rename (ext ρ) N) ≡
|
||||
rename (ext ρ) (subst (exts σ) N)
|
||||
IH = commute-subst-rename{Γ , ★}{Δ , ★}{N}
|
||||
{exts σ}{ρ = ρ'} (λ {x} → H {x})
|
||||
|
||||
commute-subst-rename {M = L · M}{ρ = ρ} r =
|
||||
cong₂ _·_ (commute-subst-rename{M = L}{ρ = ρ} r)
|
||||
(commute-subst-rename{M = M}{ρ = ρ} r)
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
subst-exts : ∀{Γ Δ Δ'}{A}{x : Γ , ★ ∋ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Δ'}
|
||||
→ ((subst (exts σ₂)) ∘ (exts σ₁)) x ≡ exts ((subst σ₂) ∘ σ₁) x
|
||||
subst-exts {x = Z} = refl
|
||||
subst-exts {A = ★}{x = S x}{σ₁}{σ₂} = G
|
||||
where
|
||||
G : ((subst (exts σ₂)) ∘ exts σ₁) (S x) ≡ rename S_ (((subst σ₂) ∘ σ₁) x)
|
||||
G =
|
||||
begin
|
||||
((subst (exts σ₂)) ∘ exts σ₁) (S x)
|
||||
≡⟨⟩
|
||||
subst (exts σ₂) (rename S_ (σ₁ x))
|
||||
≡⟨ commute-subst-rename{M = σ₁ x}{σ = σ₂}{ρ = S_} (λ {x₁} → refl) ⟩
|
||||
rename S_ (subst σ₂ (σ₁ x))
|
||||
≡⟨⟩
|
||||
rename S_ (((subst σ₂) ∘ σ₁) x)
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
subst-subst : ∀{Γ Δ Σ}{M : Γ ⊢ ★} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
|
||||
→ ((subst σ₂) ∘ (subst σ₁)) M ≡ subst (subst σ₂ ∘ σ₁) M
|
||||
subst-subst {M = ` x} = refl
|
||||
subst-subst {Γ}{Δ}{Σ}{ƛ N}{σ₁}{σ₂} = G
|
||||
where
|
||||
G : ((subst σ₂) ∘ subst σ₁) (ƛ N) ≡ (ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
G =
|
||||
begin
|
||||
((subst σ₂) ∘ subst σ₁) (ƛ N)
|
||||
≡⟨⟩
|
||||
ƛ ((subst (exts σ₂)) ∘ (subst (exts σ₁))) N
|
||||
≡⟨ cong ƛ_ (subst-subst{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩
|
||||
ƛ subst ((subst (exts σ₂)) ∘ (exts σ₁)) N
|
||||
≡⟨ cong ƛ_ (subst-equal{M = N} (λ {A}{x} → subst-exts{x = x})) ⟩
|
||||
(ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
∎
|
||||
subst-subst {M = L · M} = cong₂ _·_ (subst-subst{M = L}) (subst-subst{M = M})
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
rename-subst : ∀{Γ Δ Δ'}{M : Γ ⊢ ★}{ρ : Rename Γ Δ}{σ : Subst Δ Δ'}
|
||||
→ ((subst σ) ∘ (rename ρ)) M ≡ subst (σ ∘ ρ) M
|
||||
rename-subst {M = ` x} = refl
|
||||
rename-subst {Γ}{Δ}{Δ'}{M = ƛ M}{ρ}{σ} =
|
||||
let ih : subst (exts σ) (rename (ext ρ) M)
|
||||
≡ subst ((exts σ) ∘ ext ρ) M
|
||||
ih = rename-subst {M = M}{ρ = ext ρ}{σ = exts σ} in
|
||||
cong ƛ_ g
|
||||
where
|
||||
ss : same-subst ((exts σ) ∘ (ext ρ)) (exts (σ ∘ ρ))
|
||||
ss {A} {Z} = refl
|
||||
ss {A} {S x} = refl
|
||||
h : subst ((exts σ) ∘ (ext ρ)) M ≡ subst (exts (σ ∘ ρ)) M
|
||||
h = subst-equal{Γ , ★}{Δ = Δ' , ★}{σ = ((exts σ) ∘ (ext ρ))}
|
||||
{σ' = (exts (σ ∘ ρ))}{M = M} (λ {A} {x} → ss{A}{x})
|
||||
g : subst (exts σ) (rename (ext ρ) M)
|
||||
≡ subst (exts (σ ∘ ρ)) M
|
||||
g =
|
||||
begin
|
||||
subst (exts σ) (rename (ext ρ) M)
|
||||
≡⟨ rename-subst {M = M}{ρ = ext ρ}{σ = exts σ} ⟩
|
||||
subst ((exts σ) ∘ ext ρ) M
|
||||
≡⟨ h ⟩
|
||||
subst (exts (σ ∘ ρ)) M
|
||||
∎
|
||||
rename-subst {M = L · M} =
|
||||
cong₂ _·_ (rename-subst{M = L}) (rename-subst{M = M})
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
is-id-subst : ∀{Γ} → Subst Γ Γ → Set
|
||||
is-id-subst {Γ} σ = ∀{x : Γ ∋ ★} → σ x ≡ ` x
|
||||
|
||||
is-id-exts : ∀{Γ} {σ : Subst Γ Γ}
|
||||
→ is-id-subst σ
|
||||
→ is-id-subst (exts σ {B = ★})
|
||||
is-id-exts id {Z} = refl
|
||||
is-id-exts{Γ}{σ} id {S x} rewrite id {x} = refl
|
||||
|
||||
subst-id : ∀{Γ} {M : Γ ⊢ ★} {σ : Subst Γ Γ}
|
||||
→ is-id-subst σ
|
||||
→ subst σ M ≡ M
|
||||
subst-id {M = ` x} {σ} id = id
|
||||
subst-id {M = ƛ M} {σ} id = cong ƛ_ (subst-id (is-id-exts id))
|
||||
subst-id {M = L · M} {σ} id = cong₂ _·_ (subst-id id) (subst-id id)
|
||||
\end{code}
|
||||
|
||||
Loading…
Reference in a new issue