From 5bfc503eec0780c115f7d18521e03cde815661f3 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Wed, 20 May 2020 09:05:06 -0400 Subject: [PATCH] remove second premise from cong-rename --- src/plfa/part2/Substitution.lagda.md | 22 +++++++++++----------- src/plfa/part3/Compositional.lagda.md | 3 +-- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/plfa/part2/Substitution.lagda.md b/src/plfa/part2/Substitution.lagda.md index 536adb4a..887c0c92 100644 --- a/src/plfa/part2/Substitution.lagda.md +++ b/src/plfa/part2/Substitution.lagda.md @@ -346,15 +346,15 @@ cong-ext{Γ}{Δ}{ρ}{ρ′}{B} rr {A} = extensionality λ x → lemma {x} ``` ``` -cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M M′ : Γ ⊢ B} - → (∀{A} → ρ ≡ ρ′ {A}) → M ≡ M′ - ------------------------------ - → rename ρ M ≡ rename ρ′ M′ -cong-rename {M = ` x} rr refl = cong `_ (cong-app rr x) -cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr refl = - cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr) refl) -cong-rename {M = L · M} rr refl = - cong₂ _·_ (cong-rename rr refl) (cong-rename rr refl) +cong-rename : ∀{Γ Δ}{ρ ρ′ : Rename Γ Δ}{B}{M : Γ ⊢ B} + → (∀{A} → ρ ≡ ρ′ {A}) + ------------------------ + → rename ρ M ≡ rename ρ′ M +cong-rename {M = ` x} rr = cong `_ (cong-app rr x) +cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr = + cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr)) +cong-rename {M = L · M} rr = + cong₂ _·_ (cong-rename rr) (cong-rename rr) ``` ``` @@ -670,7 +670,7 @@ compose-rename {Γ}{Δ}{Σ}{A}{ƛ N}{ρ}{ρ′} = cong ƛ_ G rename (ext ρ) (rename (ext ρ′) N) ≡⟨ compose-rename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩ rename ((ext ρ) ∘ (ext ρ′)) N - ≡⟨ cong-rename compose-ext refl ⟩ + ≡⟨ cong-rename compose-ext ⟩ rename (ext (ρ ∘ ρ′)) N ∎ compose-rename {M = L · M} = cong₂ _·_ compose-rename compose-rename @@ -705,7 +705,7 @@ commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r = rename S_ (rename ρ (σ y)) ≡⟨ compose-rename ⟩ rename (S_ ∘ ρ) (σ y) - ≡⟨ cong-rename refl refl ⟩ + ≡⟨ cong-rename refl ⟩ rename ((ext ρ) ∘ S_) (σ y) ≡⟨ sym compose-rename ⟩ rename (ext ρ) (rename S_ (σ y)) diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index 6bf420c9..a22245a5 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -213,8 +213,7 @@ describe the proof below. ... | inj₂ ⟨ v₁′ , ⟨ L↓v12 , M↓v3 ⟩ ⟩ | inj₂ ⟨ v₁′′ , ⟨ L↓v12′ , M↓v3′ ⟩ ⟩ = let L↓⊔ = ⊔-intro L↓v12 L↓v12′ in let M↓⊔ = ⊔-intro M↓v3 M↓v3′ in - let x = inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩ in - x + inj₂ ⟨ v₁′ ⊔ v₁′′ , ⟨ sub L↓⊔ ⊔↦⊔-dist , M↓⊔ ⟩ ⟩ ℰ·→●ℰ {Γ}{γ}{L}{M}{v} (sub d lt) with ℰ·→●ℰ d ... | inj₁ lt2 = inj₁ (⊑-trans lt lt2)