progress

extra/extra/CallByName.lagda

@@ -12,6 +12,7 @@ open import plfa.Untyped
 open import plfa.Adequacy
 open import plfa.Denotational
 open import plfa.Soundness
+open import extra.Substitution
 
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
@@ -28,8 +29,6 @@ open import Relation.Nullary using (Dec; yes; no)
 open import Function using (_∘_)
 \end{code}
 
-
-
 ## Logical Relation between CBN Closures and Terms
 
 \begin{code}

extra/extra/Confluence.lagda

@@ -7,10 +7,11 @@ module extra.Confluence where
 \begin{code}
 open import extra.Substitution
 open import plfa.Untyped
-   renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to start_; _∎ to _[])
+   renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to commence_; _∎ to _fini)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
-{- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎) -}
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open import Function using (_∘_)
 \end{code}
 
 ## Reduction without the restrictions
@@ -42,13 +43,13 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
 \begin{code}
 infix  2 _—↠_
-infix  1 begin_
+infix  1 start_
 infixr 2 _—→⟨_⟩_
-infix  3 _∎
+infix  3 _[]
 
 data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
-  _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+  _[] : ∀ {Γ A} (M : Γ ⊢ A)
       --------
     → M —↠ M
 
@@ -58,11 +59,11 @@ data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
       ---------
     → L —↠ N
 
-begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
+start_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
   → M —↠ N
     ------
   → M —↠ N
-begin M—↠N = M—↠N
+start M—↠N = M—↠N
 \end{code}
 
 \begin{code}
@@ -70,7 +71,7 @@ begin M—↠N = M—↠N
          → L —↠ M
          → M —↠ N
          → L —↠ N
-—↠-trans (M ∎) mn = mn
+—↠-trans (M []) mn = mn
 —↠-trans (L —→⟨ r ⟩ lm) mn = L —→⟨ r ⟩ (—↠-trans lm mn)
 \end{code}
 
@@ -81,21 +82,21 @@ abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★}
          → N —↠ N'
            ----------
          → ƛ N —↠ ƛ N'
-abs-cong (M ∎) = ƛ M ∎
+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 []) = 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 []) = L · M []
 appR-cong {Γ}{L}{M}{M'} (M —→⟨ r ⟩ rs) = L · M —→⟨ ξ₂ r ⟩ appR-cong rs
 \end{code}
 
@@ -155,7 +156,7 @@ par-beta : ∀{Γ A}{M N : Γ ⊢ A}
          → M ⇒ N
            ------
          → M —↠ N
-par-beta {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) ∎
+par-beta {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) []
 par-beta {Γ} {★} {ƛ N} (pabs p) =
    abs-cong (par-beta p)
 par-beta {Γ} {★} {L · M} (papp p₁ p₂) =
@@ -167,7 +168,7 @@ par-beta {Γ} {★} {(ƛ N) · M} (pbeta{N' = N'}{M' = M'} p₁ p₂) =
       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
+  let c = (ƛ N') · M' —→⟨ β ⟩ N' [ M' ] [] in
   —↠-trans (—↠-trans a b) c
 \end{code}
 
@@ -190,9 +191,6 @@ par-subst {Γ}{Δ} σ₁ σ₂ = ∀{A}{x : Γ ∋ A} → σ₁ x ⇒ σ₂ x
 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}
 
@@ -210,19 +208,178 @@ par-rename {Γ}{Δ}{A}{ρ} (pbeta{Γ}{N}{N'}{M}{M'} p₁ p₂)
 \end{code}
 
 \begin{code}
-subst-par : ∀{Γ Δ A} {σ₁ σ₂ : Subst Γ Δ} {M M' : Γ ⊢ A}
+par-subst-ext : ∀{Γ Δ} {σ τ : Subst Γ Δ}
-   → par-subst σ₁ σ₂  →  M ⇒ M'
+   → par-subst σ τ
-     --------------------------
+   → par-subst (exts σ {B = ★}) (exts τ)
-   → subst σ₁ M ⇒ subst σ₂ M'
+par-subst-ext s {x = Z} = pvar
-subst-par {Γ} {Δ} {A} {σ₁} {σ₂} {` x} s pvar = s
+par-subst-ext s {x = S x} = par-rename s
-subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {ƛ N} s (pabs p) =
+\end{code}
-  let ih = subst-par {σ₁ = exts σ₁}{σ₂ = exts σ₂} {!!} p in
+
-  pabs {!!}
+
-  where
+\begin{code}
-    H : par-subst (exts σ₁ {B = ★}) (exts σ₂)
+ids : ∀{Γ} → Subst Γ Γ
-    H {★} {Z} = pvar
+ids {A} x = ` x
-    H {A} {S x} = {!!}
+
-
+cons : ∀{Γ Δ A} → (Δ ⊢ A) → Subst Γ Δ → Subst (Γ , A) Δ
-subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {L · M} s (papp p p₁) = {!!}
+cons {Γ} {Δ} {A} M σ {B} Z = M
-subst-par {Γ} {Δ} {★} {σ₁} {σ₂} {(ƛ N) · M} s (pbeta p p₁) = {!!}
+cons {Γ} {Δ} {A} M σ {B} (S x) = σ x
+
+seq : ∀{Γ Δ Σ} → Subst Γ Δ → Subst Δ Σ → Subst Γ Σ
+seq σ τ = (subst τ) ∘ σ
+
+ren : ∀{Γ Δ} → Rename Γ Δ → Subst Γ Δ
+ren ρ = ids ∘ ρ
+
+ren-ext : ∀ {Γ Δ}{B C : Type} {ρ : Rename Γ Δ} {x : Γ , B ∋ C}
+        → (ren (ext ρ)) x ≡ exts (ren ρ) x
+ren-ext {x = Z} = refl
+ren-ext {x = S x} = refl
+
+rename-seq-ren : ∀ {Γ Δ}{A} {ρ : Rename Γ Δ}{M : Γ ⊢ A}
+               → rename ρ M ≡ subst (ren ρ) M
+rename-seq-ren {M = ` x} = refl
+rename-seq-ren {ρ = ρ}{M = ƛ N} =
+  cong ƛ_ G
+  where IH : rename (ext ρ) N ≡ subst (ren (ext ρ)) N
+        IH = rename-seq-ren {ρ = ext ρ}{M = N} 
+
+        G : rename (ext ρ) N ≡ subst (exts (ren ρ)) N
+        G =
+          begin
+            rename (ext ρ) N
+          ≡⟨ IH ⟩
+            subst (ren (ext ρ)) N
+          ≡⟨ subst-equal {M = N} ren-ext ⟩
+            subst (exts (ren ρ)) N
+          ∎
+rename-seq-ren {M = L · M} = cong₂ _·_ rename-seq-ren rename-seq-ren
+
+
+exts-cons-shift : ∀{Γ Δ : Context} {A : Type}{B : Type} {σ : Subst Γ Δ}{x}
+    → exts σ {A}{B} x ≡ cons (` Z) (seq σ (ren S_)) x
+exts-cons-shift {x = Z} = refl
+exts-cons-shift {x = S x} = rename-seq-ren
+
+subst-cons-Z : ∀{Γ Δ : Context}{A : Type}{M : Δ ⊢ A}{σ : Subst Γ Δ}
+             → subst (cons M σ) (` Z) ≡ M
+subst-cons-Z = refl
+
+seq-inc-cons : ∀{Γ Δ : Context} {A B : Type} {M : Δ ⊢ A} {σ : Subst Γ Δ}
+                {x : Γ ∋ B}
+         → seq (ren S_) (cons M σ) x ≡ σ x
+seq-inc-cons = refl
+
+ids-id : ∀{Γ : Context}{A : Type} {M : Γ ⊢ A}
+         → subst ids M ≡ M
+ids-id = subst-id λ {A} {x} → refl
+
+cons-ext : ∀{Γ Δ : Context} {A B : Type} {σ : Subst (Γ , A) Δ} {x : Γ , A ∋ B}
+         → cons (subst σ (` Z)) (seq (ren S_) σ) x ≡ σ x
+cons-ext {x = Z} = refl
+cons-ext {x = S x} = refl
+
+id-seq : ∀{Γ Δ : Context} {B : Type} {σ : Subst Γ Δ} {x : Γ ∋ B}
+       → (seq ids σ) x ≡ σ x
+id-seq = refl
+
+seq-id : ∀{Γ Δ : Context} {B : Type} {σ : Subst Γ Δ} {x : Γ ∋ B}
+       → (seq σ ids) x ≡ σ x
+seq-id {Γ}{σ = σ}{x = x} =
+          begin
+            (seq σ ids) x
+          ≡⟨⟩
+            subst ids (σ x)
+          ≡⟨ ids-id ⟩
+            σ x
+          ∎
+
+seq-assoc : ∀{Γ Δ Σ Ψ : Context}{B} {σ : Subst Γ Δ} {τ : Subst Δ Σ}
+             {θ : Subst Σ Ψ} {x : Γ ∋ B}
+          → seq (seq σ τ) θ x ≡ seq σ (seq τ θ) x
+seq-assoc{Γ}{Δ}{Σ}{Ψ}{B}{σ}{τ}{θ}{x} =
+          begin
+            seq (seq σ τ) θ x
+          ≡⟨⟩
+            subst θ (subst τ (σ x))
+          ≡⟨ subst-subst{M = σ x} ⟩
+            (subst ((subst θ) ∘ τ)) (σ x)
+          ≡⟨⟩
+            seq σ (seq τ θ) x
+          ∎
+
+seq-cons :  ∀{Γ Δ Σ : Context} {A B} {σ : Subst Γ Δ} {τ : Subst Δ Σ}
+              {M : Δ ⊢ A} {x : Γ , A ∋ B}
+         → seq (cons M σ) τ x ≡ cons (subst τ M) (seq σ τ) x
+seq-cons {x = Z} = refl
+seq-cons {x = S x} = refl
+
+cons-zero-S : ∀{Γ}{A B}{x : Γ , A ∋ B} → cons (` Z) (ren S_) x ≡ ids x
+cons-zero-S {x = Z} = refl
+cons-zero-S {x = S x} = refl
+\end{code}
+
+\begin{code}
+subst-zero-cons-ids : ∀{Γ}{A B : Type}{M : Γ ⊢ B}{x : Γ , B ∋ A}
+                    → subst-zero M x ≡ cons M ids x
+subst-zero-cons-ids {x = Z} = refl
+subst-zero-cons-ids {x = S x} = refl
+\end{code}
+
+
+\begin{code}
+subst-commute : ∀{Γ Δ}{N : Γ , ★ ⊢ ★}{M : Γ ⊢ ★}{σ : Subst Γ Δ }
+    → (subst (exts σ) N) [ subst σ M ] ≡ subst σ (N [ M ])
+subst-commute {Γ}{Δ}{N}{M}{σ} =
+     begin
+       (subst (exts σ) N) [ subst σ M ]
+     ≡⟨⟩
+       subst (subst-zero (subst σ M)) (subst (exts σ) N)
+     ≡⟨ subst-equal{M = subst (exts σ) N}
+            (λ {A}{x} → subst-zero-cons-ids{A = A}{x = x}) ⟩
+       subst (cons (subst σ M) ids) (subst (exts σ) N)
+     ≡⟨ subst-subst{M = N} ⟩
+       subst (seq (exts σ) (cons (subst σ M) ids)) N
+     ≡⟨ {!!} ⟩
+       subst (seq (cons (` Z) (seq σ (ren S_))) (cons (subst σ M) ids)) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst (cons (subst σ M) ids) (` Z))
+                   (seq (seq σ (ren S_)) (cons (subst σ M) ids))) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst σ M)
+                   (seq (seq σ (ren S_)) (cons (subst σ M) ids))) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst σ M)
+                   (seq σ (seq (ren S_) (cons (subst σ M) ids)))) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst σ M) (seq σ ids)) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst σ M) σ) N
+     ≡⟨ {!!} ⟩
+       subst (cons (subst σ M) (seq ids σ)) N
+     ≡⟨ {!!} ⟩
+       subst (seq (cons M ids) σ) N
+     ≡⟨ sym (subst-subst{M = N}) ⟩
+       subst σ (subst (cons M ids) N)
+     ≡⟨ {!!} ⟩
+       subst σ (N [ M ])
+     ∎
+\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) =
+   pabs (subst-par {σ = exts σ} {τ = exts τ}
+            (λ {A}{x} → par-subst-ext s {A}{x}) p)
+subst-par {Γ} {Δ} {★} {σ} {τ} {L · M} s (papp p₁ p₂) =
+   papp (subst-par s p₁) (subst-par s p₂)
+subst-par {Γ} {Δ} {★} {σ} {τ} {(ƛ N) · M} s (pbeta{N' = N'}{M' = M'} p₁ p₂)
+    with pbeta (subst-par{σ = exts σ}{τ = exts τ}{M = N}
+                        (λ {A}{x} → par-subst-ext s {A}{x}) p₁)
+               (subst-par (λ {A}{x} → s{A}{x}) p₂)
+... | G rewrite subst-commute{N = N'}{M = M'}{σ = τ} =
+    G
 \end{code}

extra/extra/Substitution.lagda

@@ -6,7 +6,7 @@ module extra.Substitution where
 
 \begin{code}
 open import plfa.Untyped
-  using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst;
+  using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst;
          ext; exts; _[_]; subst-zero)
   renaming (_∎ to _[])
 open import plfa.Denotational using (Rename)
@@ -152,10 +152,10 @@ subst-exts {A = ★}{x = S x}{σ₁}{σ₂} = G
 
 
 \begin{code}
-subst-subst : ∀{Γ Δ Σ}{M : Γ ⊢ ★} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} 
+subst-subst : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ} 
             → ((subst σ₂) ∘ (subst σ₁)) M ≡ subst (subst σ₂ ∘ σ₁) M
 subst-subst {M = ` x} = refl
-subst-subst {Γ}{Δ}{Σ}{ƛ N}{σ₁}{σ₂} = G
+subst-subst {Γ}{Δ}{Σ}{A}{ƛ N}{σ₁}{σ₂} = G
   where
   G : ((subst σ₂) ∘ subst σ₁) (ƛ N) ≡ (ƛ subst (exts ((subst σ₂) ∘ σ₁)) N)
   G =
@@ -205,15 +205,15 @@ rename-subst {M = L · M} =
 
 \begin{code}
 is-id-subst : ∀{Γ} → Subst Γ Γ → Set
-is-id-subst {Γ} σ = ∀{x : Γ ∋ ★} → σ x ≡ ` x
+is-id-subst {Γ} σ = ∀{A}{x : Γ ∋ A} → σ x ≡ ` x
 
 is-id-exts : ∀{Γ} {σ : Subst Γ Γ}
            → is-id-subst σ
            → is-id-subst (exts σ {B = ★})
-is-id-exts id {Z} = refl
+is-id-exts id {x = Z} = refl
-is-id-exts{Γ}{σ} id {S x} rewrite id {x} = refl
+is-id-exts{Γ}{σ} id {x = S x} rewrite id {x = x} = refl
 
-subst-id : ∀{Γ} {M : Γ ⊢ ★} {σ : Subst Γ Γ}
+subst-id : ∀{Γ : Context}{A : Type} {M : Γ ⊢ A} {σ : Subst Γ Γ}
          → is-id-subst σ
          → subst σ M ≡ M
 subst-id {M = ` x} {σ} id = id