michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #568 from Altariarite/substitution

Browse source 
fixed indentation for proper code displays in Substitution.lagda.md
This commit is contained in:
Philip Wadler 2021-06-25 20:17:00 +01:00 committed by GitHub
commit e54f752b6f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/plfa/part2/Substitution.lagda.md
View file

@ -733,13 +733,13 @@ The proof is by induction on the term `M`.
* If `x = S y`, we obtain the goal by the following equational reasoning.
exts (exts σ) (ext ρ (S y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (rename S_ (σ (ρ y) (by the premise)
≡ rename (ext ρ) (exts σ (S y)) (by compose-rename)
≡ rename ((ext ρ) ∘ S_) (σ y)
≡ rename (ext ρ) (rename S_ (σ y)) (by compose-rename)
≡ rename (ext ρ) (exts σ (S y))
exts (exts σ) (ext ρ (S y))
≡ rename S_ (exts σ (ρ y))
≡ rename S_ (rename S_ (σ (ρ y) (by the premise)
≡ rename (ext ρ) (exts σ (S y)) (by compose-rename)
≡ rename ((ext ρ) ∘ S_) (σ y)
≡ rename (ext ρ) (rename S_ (σ y)) (by compose-rename)
≡ rename (ext ρ) (exts σ (S y))
* If `M` is an application, we obtain the goal using the induction
hypothesis for each subterm.
@ -807,11 +807,11 @@ We proceed by induction on the term `M`.
* If `M = ƛ N`, we first use the induction hypothesis to show that
ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N
ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N) ≡ ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N
and then use the lemma `exts-seq` to show
ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N
ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N ≡ ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N
* If `M` is an application, we use the induction hypothesis
for both subterms.