getting ready to move Substitution, LambdaReduction, and CallByName to plfa

extra/extra/CallByName.lagda

@@ -1,21 +1,25 @@
 \begin{code}
-module extra.CallByName where
+module plfa.CallByName where
 \end{code}
 
 ## Imports
 
 \begin{code}
-open import extra.LambdaReduction
-  using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[]; appL-cong)
 open import plfa.Untyped
   using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_; rename; subst;
          ext; exts; _[_]; subst-zero)
-open import plfa.Adequacy
-   using (Clos; ClosEnv; clos; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app)
+open import plfa.Substitution
+   using (rename-subst; sub-id; sub-sub; ids)
+open import plfa.LambdaReduction
+  using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[]; appL-cong)
+open import plfa.Denotational
+   using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
+open import plfa.Compositional   
+   using (Ctx; plug; compositionality)
 open import plfa.Soundness
-   using (Subst)
-open import extra.Substitution
-   using (rename-subst; sub-id; sub-sub)
+   using (Subst; soundness)
+open import plfa.Adequacy
+   using (Clos; ClosEnv; ∅'; clos; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app; adequacy)
 
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
@@ -101,3 +105,50 @@ cbn-soundness {Γ} {γ} {σ} {.(_ · _)} {c}
     let rs = (ƛ subst (exts σ₁) N) · subst σ M —→⟨ r ⟩ r' in
     ⟨ N' , ⟨ —↠-trans (appL-cong σL—↠L') rs , bl ⟩ ⟩
 \end{code}
+
+
+## Denotational Equivalence Implies Contextual Equivalence
+
+\begin{code}
+terminates : ∀{Γ} → (M : Γ ⊢ ★) → Set
+terminates {Γ} M = Σ[ N ∈ (Γ , ★ ⊢ ★) ] (M —↠ ƛ N)
+\end{code}
+
+\begin{code}
+_≅_ : ∀{Γ} → (M N : Γ ⊢ ★) → Set
+(_≅_ {Γ} M N) = ∀ {C : Ctx Γ ∅}
+                → (terminates (plug C M)) iff (terminates (plug C N))
+\end{code}
+
+\begin{code}
+denot-equal-terminates : ∀{Γ} {M N : Γ ⊢ ★} {C : Ctx Γ ∅}
+  → ℰ M ≃ ℰ N
+  → terminates (plug C M)
+  → terminates (plug C N)
+denot-equal-terminates {Γ}{M}{N}{C} eq ⟨ N' , CM—↠CƛN' ⟩ =
+  let ℰCM≃ℰCƛN' = soundness CM—↠CƛN' in
+  let ℰCM≃ℰCN = compositionality{Γ = Γ}{Δ = ∅}{C = C} eq in
+  let ℰCN≃ℰCƛN' = ≃-trans (≃-sym ℰCM≃ℰCN) ℰCM≃ℰCƛN' in
+    G (adequacy ℰCN≃ℰCƛN')
+  where
+  H-id : ℍ ∅' ids
+  H-id {()}
+
+  G : (Σ[ Δ ∈ Context ] Σ[ M' ∈ (Δ , ★ ⊢ ★) ] Σ[ γ ∈ ClosEnv Δ ]
+         ∅' ⊢ (plug C N) ⇓ clos (ƛ M') γ)
+    → terminates (plug C N)
+  G ⟨ Δ , ⟨ M' , ⟨ γ , CN⇓ƛM'γ ⟩ ⟩ ⟩
+      with cbn-soundness{σ = ids} CN⇓ƛM'γ H-id
+  ... | ⟨ N'' , ⟨ rs , ⟨ σ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩
+      rewrite sub-id{M = plug C N} | eq2 =
+      ⟨ subst (λ {A} → exts σ) M' , rs ⟩
+\end{code}
+
+\begin{code}
+denot-equal-contex-equal : ∀{Γ} {M N : Γ ⊢ ★}
+  → ℰ M ≃ ℰ N
+  → M ≅ N
+denot-equal-contex-equal{Γ}{M}{N} eq {C} =
+   ⟨ (λ tm → denot-equal-terminates eq tm) ,
+     (λ tn → denot-equal-terminates (≃-sym eq) tn) ⟩
+\end{code}

extra/extra/LambdaReduction.lagda

@@ -1,5 +1,5 @@
 \begin{code}
-module extra.LambdaReduction where
+module plfa.LambdaReduction where
 \end{code}
 
 ## Imports

extra/extra/Substitution.lagda

@@ -1,5 +1,5 @@
 \begin{code}
-module extra.Substitution where
+module plfa.Substitution where
 \end{code}
 
 ## Imports

src/plfa/Adequacy.lagda

@@ -659,9 +659,13 @@ gives us `∅ ⊢ M ↓ ⊥ ↦ ⊥`. Then the main lemma gives us
 
 \begin{code}
 adequacy : ∀{M : ∅ ⊢ ★}{N : ∅ , ★ ⊢ ★}  →  ℰ M ≃ ℰ (ƛ N)
-         →  Σ[ c ∈ Clos ] ∅' ⊢ M ⇓ c
+         →  Σ[ Γ ∈ Context ] Σ[ N ∈ (Γ , ★ ⊢ ★) ] Σ[ γ ∈ ClosEnv Γ ]
+            ∅' ⊢ M ⇓ clos (ƛ N) γ
 adequacy{M}{N} eq
     with ↓→𝔼 𝔾-∅ ((proj₂ (eq `∅ (⊥ ↦ ⊥))) (↦-intro ⊥-intro))
                  ⟨ ⊥ , ⟨ ⊥ , Refl⊑ ⟩ ⟩
-... | ⟨ c , ⟨ M⇓c , Vc ⟩ ⟩ = ⟨ c , M⇓c ⟩
+... | ⟨ clos {Γ} M' γ , ⟨ M⇓c , Vc ⟩ ⟩
+    with 𝕍→WHNF Vc
+... | ƛ_ {N = N'} = 
+    ⟨ Γ , ⟨ N' , ⟨ γ , M⇓c ⟩  ⟩ ⟩
 \end{code}

src/plfa/Soundness.lagda

@@ -14,6 +14,10 @@ module plfa.Soundness where
 
 \begin{code}
 open import plfa.Untyped
+  using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
+         subst; _[_]; subst-zero; ext; rename; exts)
+open import extra.LambdaReduction
+  using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[])
 open import plfa.Denotational
 open import plfa.Compositional
 
@@ -192,8 +196,8 @@ preserve : ∀ {Γ} {γ : Env Γ} {M N v}
     ----------
   → γ ⊢ N ↓ v
 preserve (var) ()
-preserve (↦-elim d₁ d₂) (ξ₁ x r) = ↦-elim (preserve d₁ r) d₂ 
-preserve (↦-elim d₁ d₂) (ξ₂ x r) = ↦-elim d₁ (preserve d₂ r) 
+preserve (↦-elim d₁ d₂) (ξ₁ r) = ↦-elim (preserve d₁ r) d₂ 
+preserve (↦-elim d₁ d₂) (ξ₂ r) = ↦-elim d₁ (preserve d₂ r) 
 preserve (↦-elim d₁ d₂) β = substitution (lambda-inversion d₁) d₂
 preserve (↦-intro d) (ζ r) = ↦-intro (preserve d r)
 preserve ⊥-intro r = ⊥-intro
@@ -650,20 +654,20 @@ reflect : ∀ {Γ} {γ : Env Γ} {M M' N v}
   → γ ⊢ N ↓ v  →  M —→ M'  →   M' ≡ N
     ---------------------------------
   → γ ⊢ M ↓ v
-reflect var (ξ₁ x₁ r) ()
-reflect var (ξ₂ x₁ r) ()
+reflect var (ξ₁ r) ()
+reflect var (ξ₂ r) ()
 reflect{γ = γ} (var{x = x}) β mn
     with var{γ = γ}{x = x}
 ... | d' rewrite sym mn = reflect-beta d' 
 reflect var (ζ r) ()
-reflect (↦-elim d₁ d₂) (ξ₁ x r) refl = ↦-elim (reflect d₁ r refl) d₂ 
-reflect (↦-elim d₁ d₂) (ξ₂ x r) refl = ↦-elim d₁ (reflect d₂ r refl) 
+reflect (↦-elim d₁ d₂) (ξ₁ r) refl = ↦-elim (reflect d₁ r refl) d₂ 
+reflect (↦-elim d₁ d₂) (ξ₂ r) refl = ↦-elim d₁ (reflect d₂ r refl) 
 reflect (↦-elim d₁ d₂) β mn
     with ↦-elim d₁ d₂
 ... | d' rewrite sym mn = reflect-beta d'
 reflect (↦-elim d₁ d₂) (ζ r) ()
-reflect (↦-intro d) (ξ₁ x r) ()
-reflect (↦-intro d) (ξ₂ x r) ()
+reflect (↦-intro d) (ξ₁ r) ()
+reflect (↦-intro d) (ξ₂ r) ()
 reflect (↦-intro d) β mn
     with ↦-intro d
 ... | d' rewrite sym mn = reflect-beta d'
@@ -697,7 +701,7 @@ soundness : ∀{Γ} {M : Γ ⊢ ★} {N : Γ , ★ ⊢ ★}
   → M —↠ ƛ N
     -----------------
   → ℰ M ≃ ℰ (ƛ N)
-soundness (.(ƛ _) ∎) γ v = ⟨ (λ x → x) , (λ x → x) ⟩
+soundness (.(ƛ _) []) γ v = ⟨ (λ x → x) , (λ x → x) ⟩
 soundness {Γ} (L —→⟨ r ⟩ M—↠N) γ v =
    let ih = soundness M—↠N in
    let e = reduce-equal r in