finished call-by-name soundness
This commit is contained in:
Jeremy Siek
parent
569e1718b2
commit
7b088da512
2 changed files with 372 additions and 164 deletions
|
|
@ -9,9 +9,9 @@ open import plfa.Untyped
|
|||
using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst;
|
||||
_—↠_; _—→⟨_⟩_; _—→_; ξ₁; ξ₂; β; ζ; ap; ext; exts; _[_]; subst-zero)
|
||||
renaming (_∎ to _[])
|
||||
open import plfa.Adequacy
|
||||
open import plfa.Denotational
|
||||
open import plfa.Soundness
|
||||
open import plfa.Adequacy
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
|
||||
|
|
@ -19,6 +19,7 @@ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
|||
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum
|
||||
open import Data.Nat
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Negation using (contradiction)
|
||||
open import Data.Empty using (⊥-elim) renaming (⊥ to Bot)
|
||||
|
|
@ -27,10 +28,57 @@ open import Relation.Nullary using (Dec; yes; no)
|
|||
open import Function using (_∘_)
|
||||
\end{code}
|
||||
|
||||
## Soundness of call-by-name evaluation with respect to reduction
|
||||
|
||||
## 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)
|
||||
|
||||
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
|
||||
|
||||
compose-exts : ∀{Γ Δ Δ'}{ρ : Rename Γ Δ}{σ : Subst Δ Δ'}
|
||||
→ (exts σ) ∘ (ext ρ) ≡ exts (σ ∘ ρ)
|
||||
compose-exts{Γ}{Δ}{Δ'}{ρ}{σ} = extensionality lemma
|
||||
|
|
@ -38,31 +86,110 @@ compose-exts{Γ}{Δ}{Δ'}{ρ}{σ} = extensionality lemma
|
|||
→ ((exts σ) ∘ (ext ρ)) x ≡ exts (σ ∘ ρ) x
|
||||
lemma Z = refl
|
||||
lemma (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}
|
||||
|
||||
|
||||
same-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
|
||||
same-subst{Γ}{Δ} σ σ' = ∀{x : Γ ∋ ★} → σ x ≡ σ' x
|
||||
\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 ρ
|
||||
|
||||
same-subst-ext : ∀{Γ Δ}{σ σ' : Subst Γ Δ}
|
||||
→ same-subst σ σ'
|
||||
→ same-subst (exts σ {B = ★}) (exts σ' )
|
||||
same-subst-ext ss {x = Z} = refl
|
||||
same-subst-ext ss {x = S x} = cong (rename (λ {A} → S_)) ss
|
||||
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})
|
||||
|
||||
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} → same-subst-ext {Γ}{Δ}{σ}{σ'} ss {x}) 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
|
||||
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{Γ}{Δ}{Σ}{A}{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
|
||||
|
|
@ -72,32 +199,30 @@ rename-subst {Γ}{Δ}{Δ'}{M = ƛ M}{ρ}{σ} =
|
|||
ih = rename-subst {M = M}{ρ = ext ρ}{σ = exts σ} in
|
||||
cong ƛ_ g
|
||||
where
|
||||
e : (exts σ) ∘ (ext ρ) ≡ exts (σ ∘ ρ) {★}{★}
|
||||
e : (exts σ) ∘ (ext ρ) ≡ exts (σ ∘ ρ)
|
||||
e = compose-exts{Γ}{Δ}{Δ'}{ρ}{σ}
|
||||
ss : same-subst ((exts σ) ∘ (ext ρ)) (exts (σ ∘ ρ))
|
||||
ss {Z} = refl
|
||||
ss {S x} = refl
|
||||
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} (λ {x} → ss {x})
|
||||
{σ' = (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
|
||||
subst ((exts σ) ∘ ext ρ) M
|
||||
≡⟨ h ⟩
|
||||
subst (exts (σ ∘ ρ)) {★} M
|
||||
subst (exts (σ ∘ ρ)) M
|
||||
∎
|
||||
rename-subst {M = L · M} =
|
||||
cong₂ _·_ (rename-subst{M = L}) (rename-subst{M = M})
|
||||
\end{code}
|
||||
|
||||
|
||||
inc-subst-zero-id : ∀{Γ}{M : Γ ⊢ ★}{x : Γ ∋ ★} → ((subst-zero M) ∘ S_) x ≡ ` x
|
||||
inc-subst-zero-id {.(_ , ★)} {M} {Z} = refl
|
||||
inc-subst-zero-id {.(_ , _)} {M} {S x} = refl
|
||||
|
||||
\begin{code}
|
||||
is-id-subst : ∀{Γ} → Subst Γ Γ → Set
|
||||
is-id-subst {Γ} σ = ∀{x : Γ ∋ ★} → σ x ≡ ` x
|
||||
|
||||
|
|
@ -116,6 +241,8 @@ subst-id {M = L · M} {σ} id = cong₂ _·_ (subst-id id) (subst-id id)
|
|||
\end{code}
|
||||
|
||||
|
||||
## Logical Relation between CBN Closures and Terms
|
||||
|
||||
\begin{code}
|
||||
𝔹 : Clos → (∅ ⊢ ★) → Set
|
||||
ℍ : ∀{Γ} → ClosEnv Γ → Subst Γ ∅ → Set
|
||||
|
|
@ -125,16 +252,12 @@ subst-id {M = L · M} {σ} id = cong₂ _·_ (subst-id id) (subst-id id)
|
|||
ℍ γ σ = ∀{x} → 𝔹 (γ x) (σ x)
|
||||
|
||||
ext-subst : ∀{Γ Δ} → Subst Γ Δ → Δ ⊢ ★ → Subst (Γ , ★) Δ
|
||||
{-
|
||||
ext-subst σ N Z = N
|
||||
ext-subst σ N (S n) = σ n
|
||||
-}
|
||||
ext-subst{Γ}{Δ} σ N {A} = (subst (subst-zero N)) ∘ (exts σ)
|
||||
|
||||
ℍ-ext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {c} {N : ∅ ⊢ ★}
|
||||
→ ℍ γ σ → 𝔹 c N
|
||||
--------------------------------
|
||||
→ ℍ (γ ,' c) (ext-subst{Γ}{∅} σ N)
|
||||
→ ℍ (γ ,' c) ((subst (subst-zero N)) ∘ (exts σ))
|
||||
ℍ-ext {Γ} {γ} {σ} g e {Z} = e
|
||||
ℍ-ext {Γ} {γ} {σ}{c}{N} g e {S x} = G g
|
||||
where
|
||||
|
|
@ -153,18 +276,6 @@ ext-subst{Γ}{Δ} σ N {A} = (subst (subst-zero N)) ∘ (exts σ)
|
|||
G b rewrite eq = b
|
||||
\end{code}
|
||||
|
||||
|
||||
|
||||
\begin{code}
|
||||
cbn-result-clos : ∀{Γ}{γ : ClosEnv Γ}{M : Γ ⊢ ★}{c : Clos}
|
||||
→ γ ⊢ M ⇓ c
|
||||
→ Σ[ Δ ∈ Context ] Σ[ δ ∈ ClosEnv Δ ] Σ[ N ∈ Δ , ★ ⊢ ★ ]
|
||||
c ≡ clos (ƛ N) δ
|
||||
cbn-result-clos (⇓-var x₁ d) = cbn-result-clos d
|
||||
cbn-result-clos {Γ}{γ}{ƛ N} ⇓-lam = ⟨ Γ , ⟨ γ , ⟨ N , refl ⟩ ⟩ ⟩
|
||||
cbn-result-clos (⇓-app d₁ d₂) = cbn-result-clos d₂
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
—↠-trans : ∀{Γ}{L M N : Γ ⊢ ★}
|
||||
→ L —↠ M
|
||||
|
|
@ -179,7 +290,7 @@ cbn-result-clos (⇓-app d₁ d₂) = cbn-result-clos d₂
|
|||
→ L —→ L'
|
||||
→ L · M —→ L' · M
|
||||
—→-app-cong (ξ₁ ap ll') = ξ₁ ap (—→-app-cong ll')
|
||||
—→-app-cong (ξ₂ neu ll') = ξ₁ ap (ξ₂ neu ll')
|
||||
—→-app-cong (ξ₂ ne ll') = ξ₁ ap (ξ₂ ne ll')
|
||||
—→-app-cong β = ξ₁ ap β
|
||||
—→-app-cong (ζ ll') = {!!} {- JGS: problem with ξ₁! -}
|
||||
|
||||
|
|
@ -191,117 +302,6 @@ cbn-result-clos (⇓-app d₁ d₂) = cbn-result-clos d₂
|
|||
L · M —→⟨ —→-app-cong r ⟩ (—↠-app-cong ll')
|
||||
\end{code}
|
||||
|
||||
|
||||
\begin{code}
|
||||
rename-inc-subst : ∀{Γ}{M : Γ ⊢ ★}{N : Γ ⊢ ★}
|
||||
→ (subst (subst-zero M) (rename S_ N)) ≡ N
|
||||
rename-inc-subst {Γ} {M} {N} rewrite
|
||||
rename-subst{M = N}{ρ = S_}{σ = subst-zero M} = subst-id refl
|
||||
|
||||
|
||||
subst-empty : ∀{σ : Subst ∅ ∅}{M : ∅ ⊢ ★}
|
||||
→ subst σ M ≡ M
|
||||
subst-empty {σ} {` ()}
|
||||
subst-empty {σ} {ƛ M} = cong ƛ_ (subst-id G)
|
||||
where G : is-id-subst (exts σ {B = ★})
|
||||
G {Z} = refl
|
||||
G {S ()}
|
||||
subst-empty {σ} {L · M} = cong₂ _·_ subst-empty subst-empty
|
||||
|
||||
commute-exts-subst : ∀{Γ Δ Δ'} {σ : Subst Γ Δ} {σ' : Subst Δ Δ'}
|
||||
{A}{B} {x : Γ , B ∋ A}
|
||||
→ ((subst (exts σ')) ∘ exts σ) x ≡ (exts ((subst σ') ∘ σ)) x
|
||||
commute-exts-subst {Γ} {Δ} {Δ'} {σ} {σ'} {x = Z} = refl
|
||||
commute-exts-subst {∅} {Δ} {Δ'} {σ} {σ'} {x = S ()}
|
||||
commute-exts-subst {Γ , A} {Δ} {Δ'} {σ} {σ'} {x = S x} =
|
||||
let ih = commute-exts-subst {Γ}{{!!}}{{!!}}{λ y → {!!}}{{!!}}{x = x} in
|
||||
{!!}
|
||||
{-
|
||||
((subst (exts σ')) ∘ exts σ) (S x)
|
||||
≡
|
||||
(subst (exts σ')) ((exts σ) (S x) )
|
||||
≡
|
||||
(subst (exts σ')) (rename S_ (σ x))
|
||||
≡
|
||||
subst ((exts σ') ∘ S_) (σ x)
|
||||
≡
|
||||
subst (S_ ∘ σ') (σ x)
|
||||
|
||||
|
||||
Goal: ((subst (exts σ')) ∘ exts σ) (S x) ≡
|
||||
rename S_ (((subst σ') ∘ σ) x)
|
||||
|
||||
-}
|
||||
|
||||
|
||||
{-
|
||||
|
||||
((subst (exts σ')) ∘ subst (exts σ)) N
|
||||
≡
|
||||
subst ((subst (exts σ')) ∘ exts σ) N
|
||||
≡?
|
||||
subst (exts ((subst σ') ∘ σ)) N
|
||||
|
||||
|
||||
goal:
|
||||
((subst (exts σ')) ∘ (subst (exts σ))) N
|
||||
≡
|
||||
subst (exts ((subst σ') ∘ σ)) N
|
||||
|
||||
-}
|
||||
|
||||
subst-subst : ∀{Γ Δ Δ'} {σ : Subst Γ Δ} {σ' : Subst Δ Δ'} {M : Γ ⊢ ★}
|
||||
→ ((subst σ') ∘ (subst σ)) M ≡ subst (subst σ' ∘ σ) M
|
||||
subst-subst {Γ} {Δ} {Δ'} {σ} {σ'} {` x} = refl
|
||||
subst-subst {Γ} {Δ} {Δ'} {σ} {σ'} {ƛ N} =
|
||||
let ih = subst-subst{Γ , ★}{Δ , ★}{Δ' , ★}{exts σ}{exts σ'}{M = N} in
|
||||
cong ƛ_ {!!}
|
||||
subst-subst {Γ} {Δ} {Δ'} {σ} {σ'} {L · M} =
|
||||
cong₂ _·_ (subst-subst{M = L}) (subst-subst{M = M})
|
||||
|
||||
{-
|
||||
|
||||
subst (subst-zero (subst σ M)) (subst (exts σ₁) N)
|
||||
=
|
||||
((subst (subst-zero (subst σ M))) ∘ (subst (exts σ))) N
|
||||
|
||||
(subst σ) ∘ (subst σ')
|
||||
=
|
||||
subst (subst σ ∘ σ')
|
||||
|
||||
|
||||
|
||||
subst ( (subst (subst-zero (subst σ M)) ∘ (exts σ₁)) N
|
||||
=
|
||||
subst (ext-subst σ₁ (subst σ M)) N
|
||||
|
||||
-}
|
||||
|
||||
subst-exts-ext-subst : ∀{Γ Δ Δ'}{σ : Subst Γ Δ'}{σ₁ : Subst Δ Δ'}
|
||||
{M : Γ ⊢ ★}{N : Δ , ★ ⊢ ★}
|
||||
→ subst (subst-zero (subst σ M)) (subst (exts σ₁) N)
|
||||
≡ subst (ext-subst σ₁ (subst σ M)) N
|
||||
subst-exts-ext-subst {Γ} {Δ} {Δ'} {σ} {σ₁} {M} {` Z} = refl
|
||||
subst-exts-ext-subst {Γ} {Δ} {Δ'} {σ} {σ₁} {M} {` (S x)} = {!!}
|
||||
subst-exts-ext-subst {Γ} {Δ} {Δ'} {σ} {σ₁} {M} {ƛ N} =
|
||||
let ih : subst(subst-zero(subst (λ x → rename S_ (σ x)) M))(subst(exts σ') N)
|
||||
≡ subst (ext-subst σ' (subst (λ x → rename S_ (σ x)) M)) N
|
||||
ih = (subst-exts-ext-subst{Γ}{Δ , ★}{Δ' , ★}
|
||||
{λ x → rename S_ (σ x)}{σ'}{M}{N}) in
|
||||
let x : subst (exts (subst-zero (subst σ M)))
|
||||
(subst (exts (exts σ₁)) N)
|
||||
≡ subst (exts (ext-subst σ₁ (subst σ M))) N
|
||||
x = {!!} in
|
||||
cong ƛ_ x
|
||||
where σ' : Subst (Δ , ★) (Δ' , ★)
|
||||
σ' Z = ` Z
|
||||
σ' (S x) = rename S_ (σ₁ x)
|
||||
|
||||
subst-exts-ext-subst {Γ} {Δ} {Δ'} {σ} {σ₁} {M} {N · N'} =
|
||||
cong₂ _·_ (subst-exts-ext-subst{Γ}{Δ}{Δ'}{σ}{σ₁}{M}{N})
|
||||
(subst-exts-ext-subst{Γ}{Δ}{Δ'}{σ}{σ₁}{M}{N'})
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
cbn-soundness : ∀{Γ}{γ : ClosEnv Γ}{σ : Subst Γ ∅}{M : Γ ⊢ ★}{c : Clos}
|
||||
→ γ ⊢ M ⇓ c → ℍ γ σ
|
||||
|
|
@ -321,8 +321,8 @@ cbn-soundness {Γ} {γ} {σ} {.(_ · _)} {c}
|
|||
with cbn-soundness{σ = ext-subst σ₁ (subst σ M)} d₂
|
||||
(λ {x} → ℍ-ext{Δ}{σ = σ₁} Hδσ₁ (⟨ σ , ⟨ h , refl ⟩ ⟩){x})
|
||||
| β{∅}{subst (exts σ₁) N}{subst σ M}
|
||||
... | ⟨ N' , ⟨ r' , bl ⟩ ⟩ | r
|
||||
rewrite subst-exts-ext-subst {Γ}{Δ}{∅}{σ}{σ₁}{M}{N} =
|
||||
... | ⟨ N' , ⟨ r' , bl ⟩ ⟩ | r
|
||||
rewrite subst-subst{M = N}{σ₁ = exts σ₁}{σ₂ = subst-zero (subst σ M)} =
|
||||
let rs = (ƛ subst (exts σ₁) N) · subst σ M —→⟨ r ⟩ r' in
|
||||
⟨ N' , ⟨ —↠-trans (—↠-app-cong σL—↠L') rs , bl ⟩ ⟩
|
||||
⟨ N' , ⟨ —↠-trans (—↠-app-cong σL—↠L') rs , bl ⟩ ⟩
|
||||
\end{code}
|
||||
|
|
|
|||
208
extra/extra/ComposeSubst.lagda
Normal file
208
extra/extra/ComposeSubst.lagda
Normal file
|
|
@ -0,0 +1,208 @@
|
|||
\begin{code}
|
||||
module extra.ComposeSubst where
|
||||
\end{code}
|
||||
|
||||
I was having trouble proving a lemma about composition of subsitution.
|
||||
To find the proof, I had to strip away the well-scoping requirements
|
||||
for terms. Next I'm going to see if I can do the proof with
|
||||
well-scoped terms. -Jeremy
|
||||
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat
|
||||
open import Function using (_∘_)
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
postulate
|
||||
extensionality : ∀ {A B : Set} {f g : A → B}
|
||||
→ (∀ (x : A) → f x ≡ g x)
|
||||
-----------------------
|
||||
→ f ≡ g
|
||||
\end{code}
|
||||
|
||||
## Untyped Lambda Calculus
|
||||
|
||||
\begin{code}
|
||||
Var : Set
|
||||
Var = ℕ
|
||||
|
||||
data Term : Set where
|
||||
|
||||
`_ :
|
||||
Var
|
||||
----
|
||||
→ Term
|
||||
|
||||
ƛ_ :
|
||||
Term
|
||||
----
|
||||
→ Term
|
||||
|
||||
_·_ :
|
||||
Term
|
||||
→ Term
|
||||
----
|
||||
→ Term
|
||||
|
||||
ext : (Var → Var)
|
||||
-----------
|
||||
→ (Var → Var)
|
||||
ext ρ zero = zero
|
||||
ext ρ (suc x) = suc (ρ x)
|
||||
|
||||
rename :
|
||||
(Var → Var)
|
||||
-------------
|
||||
→ (Term → Term)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
|
||||
exts : (Var → Term)
|
||||
------------
|
||||
→ (Var → Term)
|
||||
exts σ zero = ` zero
|
||||
exts σ (suc x) = rename suc (σ x)
|
||||
|
||||
subst :
|
||||
(Var → Term)
|
||||
-------------
|
||||
→ (Term → Term)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
|
||||
|
||||
same-subst : (Var → Term) → (Var → Term) → Set
|
||||
same-subst σ σ' = ∀{x : Var} → σ x ≡ σ' x
|
||||
|
||||
|
||||
same-subst-ext : {σ σ' : Var → Term}
|
||||
→ same-subst σ σ'
|
||||
→ same-subst (exts σ) (exts σ' )
|
||||
same-subst-ext ss {x = zero} = refl
|
||||
same-subst-ext ss {x = suc x} = cong (rename suc) ss
|
||||
|
||||
|
||||
subst-equal : {σ σ' : Var → Term}{M : Term}
|
||||
→ same-subst σ σ'
|
||||
→ subst σ M ≡ subst σ' M
|
||||
subst-equal {σ} {σ'} {` x} ss = ss
|
||||
subst-equal {σ} {σ'} {ƛ M} ss =
|
||||
let ih = subst-equal {σ = exts σ}{σ' = exts σ'} {M = M}
|
||||
(λ {x} → same-subst-ext{σ}{σ'} ss {x}) 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
|
||||
|
||||
|
||||
compose-ext : ∀{ρ ρ' : Var → Var}
|
||||
→ (ext ρ) ∘ (ext ρ') ≡ ext (ρ ∘ ρ')
|
||||
compose-ext{ρ}{ρ'} = extensionality lemma
|
||||
where
|
||||
lemma : (x : Var) → ext ρ (ext ρ' x) ≡ ext (ρ ∘ ρ') x
|
||||
lemma zero = refl
|
||||
lemma (suc x) = refl
|
||||
|
||||
|
||||
compose-rename : ∀{M : Term}{ρ ρ' : Var → Var}
|
||||
→ rename ρ (rename ρ' M) ≡ rename (ρ ∘ ρ') M
|
||||
compose-rename {` x} {ρ} {ρ'} = refl
|
||||
compose-rename {ƛ N} {ρ} {ρ'} = cong ƛ_ G
|
||||
where IH : {ρ : Var → Var} {ρ' : Var → Var} →
|
||||
rename ρ (rename ρ' N) ≡ rename (ρ ∘ ρ') N
|
||||
IH = compose-rename {N}
|
||||
G : rename (ext ρ) (rename (ext ρ') N)
|
||||
≡ rename (ext (ρ ∘ ρ')) N
|
||||
G =
|
||||
begin
|
||||
rename (ext ρ) (rename (ext ρ') N)
|
||||
≡⟨ IH ⟩
|
||||
rename ((ext ρ) ∘ (ext ρ')) N
|
||||
≡⟨ cong₂ rename compose-ext refl ⟩
|
||||
rename (ext (ρ ∘ ρ')) N
|
||||
∎
|
||||
compose-rename {L · M} {ρ} {ρ'} = cong₂ _·_ compose-rename compose-rename
|
||||
|
||||
|
||||
commute-subst-rename : ∀{M : Term}{σ : Var → Term}{ρ : Var → Var}
|
||||
→ (∀{x : Var} → exts σ (ρ x) ≡ rename ρ (σ x))
|
||||
→ subst (exts σ) (rename ρ M) ≡ rename ρ (subst σ M)
|
||||
commute-subst-rename {` x} {σ}{ρ} r = r
|
||||
commute-subst-rename {ƛ N} {σ}{ρ} r = cong ƛ_ G
|
||||
where
|
||||
IH : ∀ {σ : Var → Term}{ρ : Var → Var}
|
||||
→ (∀{x : Var} → exts σ (ρ x) ≡ rename ρ (σ x))
|
||||
→ subst (exts σ) (rename ρ N) ≡ rename ρ (subst σ N)
|
||||
IH = commute-subst-rename {N}
|
||||
|
||||
H : ∀{x : Var} →
|
||||
exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
|
||||
H {zero} = refl
|
||||
H {suc x} =
|
||||
begin
|
||||
rename suc (exts σ (ρ x))
|
||||
≡⟨ cong₂ rename (extensionality (λ x₁ → refl)) r ⟩
|
||||
rename suc (rename ρ (σ x))
|
||||
≡⟨ compose-rename ⟩
|
||||
rename (suc ∘ ρ) (σ x)
|
||||
≡⟨ cong₂ rename (extensionality λ x₁ → refl) refl ⟩
|
||||
rename ((ext ρ) ∘ suc) (σ x)
|
||||
≡⟨ sym compose-rename ⟩
|
||||
rename (ext ρ) (rename suc (σ x))
|
||||
∎
|
||||
G : subst (exts (exts σ)) (rename (ext ρ) N) ≡
|
||||
rename (ext ρ) (subst (exts σ) N)
|
||||
G = IH{σ = exts σ}{ρ = ext ρ} (λ {x} → H{x})
|
||||
commute-subst-rename {L · M} {σ} r =
|
||||
cong₂ _·_ (commute-subst-rename{L} r) (commute-subst-rename{M} r)
|
||||
|
||||
|
||||
subst-exts : ∀{x : Var} {σ₁ σ₂ : Var → Term}
|
||||
→ ((subst (exts σ₂)) ∘ (exts σ₁)) x ≡ exts ((subst σ₂) ∘ σ₁) x
|
||||
subst-exts {zero} = refl
|
||||
subst-exts {suc x}{σ₁}{σ₂} = G
|
||||
where
|
||||
G : ((subst (exts σ₂)) ∘ exts σ₁) (suc x) ≡ rename suc (((subst σ₂) ∘ σ₁) x)
|
||||
G =
|
||||
begin
|
||||
((subst (exts σ₂)) ∘ exts σ₁) (suc x)
|
||||
≡⟨⟩
|
||||
subst (exts σ₂) (rename suc (σ₁ x))
|
||||
≡⟨ commute-subst-rename{σ₁ x}{σ₂}{suc} (λ {x₁} → refl) ⟩
|
||||
rename suc (subst σ₂ (σ₁ x))
|
||||
≡⟨⟩
|
||||
rename suc (((subst σ₂) ∘ σ₁) x)
|
||||
∎
|
||||
|
||||
|
||||
subst-subst : ∀{M : Term} {σ₁ σ₂ : Var → Term}
|
||||
→ ((subst σ₂) ∘ (subst σ₁)) M ≡ subst (subst σ₂ ∘ σ₁) M
|
||||
subst-subst {` x} {σ₁} {σ₂} = refl
|
||||
subst-subst {ƛ N} {σ₁} {σ₂} = G
|
||||
where
|
||||
IH : ∀ {σ₁ σ₂ : ℕ → Term} →
|
||||
((subst σ₂) ∘ (subst σ₁)) N ≡ subst ((subst σ₂) ∘ σ₁) N
|
||||
IH = subst-subst {N}
|
||||
|
||||
G : ((subst σ₂) ∘ subst σ₁) (ƛ N) ≡ (ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
G =
|
||||
begin
|
||||
((subst σ₂) ∘ subst σ₁) (ƛ N)
|
||||
≡⟨⟩
|
||||
ƛ ((subst (exts σ₂)) ∘ (subst (exts σ₁))) N
|
||||
≡⟨ cong ƛ_ (IH{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩
|
||||
ƛ subst ((subst (exts σ₂)) ∘ (exts σ₁)) N
|
||||
≡⟨ cong ƛ_ (subst-equal{M = N} λ {x} → subst-exts{x}) ⟩
|
||||
(ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
|
||||
∎
|
||||
subst-subst {L · M} {σ₁} {σ₂} = cong₂ _·_ (subst-subst{L}) (subst-subst{M})
|
||||
\end{code}
|
||||
Loading…
Reference in a new issue