From 433587bc6125a7af6518b562ea0e2331c30b29fa Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Thu, 9 Apr 2020 09:18:30 -0400 Subject: [PATCH] more edits --- src/plfa/part3/ContextualEquivalence.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/part3/ContextualEquivalence.lagda.md b/src/plfa/part3/ContextualEquivalence.lagda.md index 748c2b98..c1b0d9f7 100644 --- a/src/plfa/part3/ContextualEquivalence.lagda.md +++ b/src/plfa/part3/ContextualEquivalence.lagda.md @@ -20,7 +20,7 @@ open import plfa.part2.BigStep using (_⊢_⇓_; cbn→reduce) open import plfa.part3.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_) open import plfa.part3.Compositional using (Ctx; plug; compositionality) open import plfa.part3.Soundness using (soundness) -open import plfa.part3.Adequacy using (adequacy) +open import plfa.part3.Adequacy using (↓→⇓) ``` ## Contextual Equivalence @@ -78,7 +78,7 @@ denot-equal-terminates {Γ}{M}{N}{C} ℰM≃ℰN ⟨ N′ , CM—↠ƛN′ ⟩ = let ℰCM≃ℰƛN′ = soundness CM—↠ƛN′ in let ℰCM≃ℰCN = compositionality{Γ = Γ}{Δ = ∅}{C = C} ℰM≃ℰN in let ℰCN≃ℰƛN′ = ≃-trans (≃-sym ℰCM≃ℰCN) ℰCM≃ℰƛN′ in - cbn→reduce (proj₂ (proj₂ (proj₂ (adequacy ℰCN≃ℰƛN′)))) + cbn→reduce (proj₂ (proj₂ (proj₂ (↓→⇓ ℰCN≃ℰƛN′)))) ``` The proof is direct. Because `plug C —↠ plug C (ƛN′)`, @@ -94,7 +94,7 @@ Putting these two facts together gives us ℰ (plug C N) ≃ ℰ (ƛN′). -We then apply adequacy to deduce +We then apply `↓→⇓` from Chapter [Adequacy](../Adequacy.lagda.md) to deduce ∅' ⊢ plug C N ⇓ clos (ƛ N′′) δ).