removed remaining references to nth
This commit is contained in:
Jeremy Siek
parent
489daa4519
commit
40f287e050
2 changed files with 36 additions and 45 deletions
|
|
@ -240,8 +240,8 @@ _`,_ : ∀ {Γ} → Env Γ → Value → Env (Γ , ★)
|
|||
(γ `, v) (S x) = γ x
|
||||
```
|
||||
|
||||
We can recover the initial environment from an extended environment,
|
||||
and the last value. Putting them back together again takes us where we started.
|
||||
We can recover the previous environment from an extended environment,
|
||||
and the last value. Putting them together again takes us back to where we started.
|
||||
```
|
||||
init : ∀ {Γ} → Env (Γ , ★) → Env Γ
|
||||
init γ x = γ (S x)
|
||||
|
|
@ -256,14 +256,6 @@ init-last {Γ} γ = extensionality lemma
|
|||
lemma (S x) = refl
|
||||
```
|
||||
|
||||
The nth function takes a de Bruijn index and finds the corresponding
|
||||
value in the environment.
|
||||
|
||||
```
|
||||
nth : ∀{Γ} → (Γ ∋ ★) → Env Γ → Value
|
||||
nth x ρ = ρ x
|
||||
```
|
||||
|
||||
We extend the `⊑` relation point-wise to environments with the
|
||||
following definition.
|
||||
|
||||
|
|
@ -716,27 +708,26 @@ same or larger than the original values. This generalization is useful
|
|||
in proving that reduction implies denotational equality.
|
||||
|
||||
As before, we need an extension lemma to handle the case where we
|
||||
proceed underneath a lambda abstraction. Here, the nth function
|
||||
performs lookup in the environment, analogous to `Γ ∋ A`. Now suppose
|
||||
that `ρ` is a renaming that maps variables in `γ` into variables with
|
||||
equal or larger values in `δ`. This lemmas says that extending the
|
||||
renaming producing a renaming `ext r` that maps `γ , v` to `δ , v`.
|
||||
proceed underneath a lambda abstraction. Suppose that `ρ` is a
|
||||
renaming that maps variables in `γ` into variables with equal or
|
||||
larger values in `δ`. This lemmas says that extending the renaming
|
||||
producing a renaming `ext r` that maps `γ , v` to `δ , v`.
|
||||
|
||||
```
|
||||
ext-nth : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
|
||||
ext-⊑ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
|
||||
→ (ρ : Rename Γ Δ)
|
||||
→ γ `⊑ (δ ∘ ρ)
|
||||
------------------------------
|
||||
→ (γ `, v) `⊑ ((δ `, v) ∘ ext ρ)
|
||||
ext-nth ρ lt Z = ⊑-refl
|
||||
ext-nth ρ lt (S n′) = lt n′
|
||||
ext-⊑ ρ lt Z = ⊑-refl
|
||||
ext-⊑ ρ lt (S n′) = lt n′
|
||||
```
|
||||
|
||||
We proceed by cases on the de Bruijn index `n`.
|
||||
|
||||
* If it is `Z`, then we just need to show that `v ≡ v`, which we have by `refl`.
|
||||
|
||||
* If it is `S n′`, then the goal simplifies to `nth n′ γ ≡ nth (ρ n′) δ`,
|
||||
* If it is `S n′`, then the goal simplifies to `γ n′ ≡ δ (ρ n′)`,
|
||||
which is an instance of the premise.
|
||||
|
||||
Now for the renaming lemma. Suppose we have a renaming that maps
|
||||
|
|
@ -756,7 +747,7 @@ rename-pres ρ lt (var {x = x}) = sub var (lt x)
|
|||
rename-pres ρ lt (↦-elim d d₁) =
|
||||
↦-elim (rename-pres ρ lt d) (rename-pres ρ lt d₁)
|
||||
rename-pres ρ lt (↦-intro d) =
|
||||
↦-intro (rename-pres (ext ρ) (ext-nth ρ lt) d)
|
||||
↦-intro (rename-pres (ext ρ) (ext-⊑ ρ lt) d)
|
||||
rename-pres ρ lt ⊥-intro = ⊥-intro
|
||||
rename-pres ρ lt (⊔-intro d d₁) =
|
||||
⊔-intro (rename-pres ρ lt d) (rename-pres ρ lt d₁)
|
||||
|
|
@ -767,11 +758,11 @@ rename-pres ρ lt (sub d lt′) =
|
|||
The proof is by induction on the semantics of `M`. As you can see, all
|
||||
of the cases are trivial except the cases for variables and lambda.
|
||||
|
||||
* For a variable `x`, we make use of the premise to
|
||||
show that `nth x γ ≡ nth (ρ x) δ`.
|
||||
* For a variable `x`, we make use of the premise to show that
|
||||
`γ x ≡ δ (ρ x)`.
|
||||
|
||||
* For a lambda abstraction, the induction hypothesis requires us to
|
||||
extend the renaming. We do so, and use the `ext-nth` lemma to show
|
||||
extend the renaming. We do so, and use the `ext-⊑` lemma to show
|
||||
that the extended renaming maps variables to ones with equivalent
|
||||
values.
|
||||
|
||||
|
|
@ -809,11 +800,11 @@ up-env : ∀ {Γ} {γ : Env Γ} {M v u₁ u₂}
|
|||
→ u₁ ⊑ u₂
|
||||
-----------------
|
||||
→ (γ `, u₂) ⊢ M ↓ v
|
||||
up-env d lt = ⊑-env d (nth-le lt)
|
||||
up-env d lt = ⊑-env d (ext-le lt)
|
||||
where
|
||||
nth-le : ∀ {γ u₁ u₂} → u₁ ⊑ u₂ → (γ `, u₁) `⊑ (γ `, u₂)
|
||||
nth-le lt Z = lt
|
||||
nth-le lt (S n) = ⊑-refl
|
||||
ext-le : ∀ {γ u₁ u₂} → u₁ ⊑ u₂ → (γ `, u₁) `⊑ (γ `, u₂)
|
||||
ext-le lt Z = lt
|
||||
ext-le lt (S n) = ⊑-refl
|
||||
```
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -105,7 +105,7 @@ The proof is by cases on the de Bruijn index `x`.
|
|||
which we have by rule `var`.
|
||||
|
||||
* If it is `S x′`,then we need to show that
|
||||
`δ , v ⊢ rename S_ (σ x′) ↓ nth x′ γ`,
|
||||
`δ , v ⊢ rename S_ (σ x′) ↓ γ x′`,
|
||||
which we obtain by the `rename-pres` lemma.
|
||||
|
||||
With the extension lemma in hand, the proof that simultaneous
|
||||
|
|
@ -132,9 +132,9 @@ subst-pres σ s (sub d lt) = sub (subst-pres σ s d) lt
|
|||
The proof is by induction on the semantics of `M`. The two interesting
|
||||
cases are for variables and lambda abstractions.
|
||||
|
||||
* For a variable `x`, we have that `v ⊑ nth x γ` and we need to show that
|
||||
* For a variable `x`, we have that `v ⊑ γ x` and we need to show that
|
||||
`δ ⊢ σ x ↓ v`. From the premise applied to `x`, we have that
|
||||
`δ ⊢ σ x ↓ nth x γ`, so we conclude by the `sub` rule.
|
||||
`δ ⊢ σ x ↓ γ x`, so we conclude by the `sub` rule.
|
||||
|
||||
* For a lambda abstraction, we must extend the substitution
|
||||
for the induction hypothesis. We apply the `subst-ext` lemma
|
||||
|
|
@ -170,12 +170,12 @@ To use the lemma, we just need to show that `subst-zero M` maps
|
|||
variables to terms that produces the same values as those in `γ , v`.
|
||||
Let `y` be an arbitrary variable (de Bruijn index).
|
||||
|
||||
* If it is `Z`, then `(subst-zero M) y = M` and `nth y (γ , v) = v`.
|
||||
* If it is `Z`, then `(subst-zero M) y = M` and `(γ , v) y = v`.
|
||||
By the premise we conclude that `γ ⊢ M ↓ v`.
|
||||
|
||||
* If it is `S x`, then `(subst-zero M) (S x) = x` and
|
||||
`nth (S x) (γ , v) = nth x γ`. So we conclude that
|
||||
`γ ⊢ x ↓ nth x γ` by rule `var`.
|
||||
`(γ , v) (S x) = γ x`. So we conclude that
|
||||
`γ ⊢ x ↓ γ x` by rule `var`.
|
||||
|
||||
|
||||
### Reduction preserves denotations
|
||||
|
|
@ -241,13 +241,13 @@ if `δ ⊢ rename ρ M ↓ v`, then `γ ⊢ M ↓ v`, where `(δ ∘ ρ) `⊑ γ
|
|||
|
||||
First, we need a variant of a lemma given earlier.
|
||||
```
|
||||
nth-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
|
||||
ext-⊑′ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ}
|
||||
→ (ρ : Rename Γ Δ)
|
||||
→ (δ ∘ ρ) `⊑ γ
|
||||
------------------------------
|
||||
→ ((δ `, v) ∘ ext ρ) `⊑ (γ `, v)
|
||||
nth-ext ρ lt Z = ⊑-refl
|
||||
nth-ext ρ lt (S x) = lt x
|
||||
ext-⊑′ ρ lt Z = ⊑-refl
|
||||
ext-⊑′ ρ lt (S x) = lt x
|
||||
```
|
||||
|
||||
The proof is then as follows.
|
||||
|
|
@ -261,7 +261,7 @@ rename-reflect : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} { M : Γ ⊢ ★}
|
|||
rename-reflect {M = ` x} all-n d with var-inv d
|
||||
... | lt = sub var (⊑-trans lt (all-n x))
|
||||
rename-reflect {M = ƛ N}{ρ = ρ} all-n (↦-intro d) =
|
||||
↦-intro (rename-reflect (nth-ext ρ all-n) d)
|
||||
↦-intro (rename-reflect (ext-⊑′ ρ all-n) d)
|
||||
rename-reflect {M = ƛ N} all-n ⊥-intro = ⊥-intro
|
||||
rename-reflect {M = ƛ N} all-n (⊔-intro d₁ d₂) =
|
||||
⊔-intro (rename-reflect all-n d₁) (rename-reflect all-n d₂)
|
||||
|
|
@ -280,8 +280,8 @@ We cannot prove this lemma by induction on the derivation of
|
|||
`δ ⊢ rename ρ M ↓ v`, so instead we proceed by induction on `M`.
|
||||
|
||||
* If it is a variable, we apply the inversion lemma to obtain
|
||||
that `v ⊑ nth (ρ x) δ`. Instantiating the premise to `x` we have
|
||||
`nth (ρ x) δ = nth x γ`, so we conclude by the `var` rule.
|
||||
that `v ⊑ δ (ρ x)`. Instantiating the premise to `x` we have
|
||||
`δ (ρ x) = γ x`, so we conclude by the `var` rule.
|
||||
|
||||
* If it is a lambda abstraction `ƛ N`, we have
|
||||
rename `ρ (ƛ N) = ƛ (rename (ext ρ) N)`.
|
||||
|
|
@ -318,7 +318,7 @@ rename-inc-reflect d = rename-reflect `⊑-refl d
|
|||
|
||||
We are almost ready to begin proving that simultaneous substitution
|
||||
reflects denotations. That is, if `γ ⊢ (subst σ M) ↓ v`, then
|
||||
`γ ⊢ σ k ↓ nth k δ` and `δ ⊢ M ↓ v` for any `k` and some `δ`.
|
||||
`γ ⊢ σ k ↓ δ k` and `δ ⊢ M ↓ v` for any `k` and some `δ`.
|
||||
We shall start with the case in which `M` is a variable `x`.
|
||||
So instead the premise is `γ ⊢ σ x ↓ v` and we need to show that
|
||||
`δ ⊢ x ↓ v` for some `δ`. The `δ` that we choose shall be the
|
||||
|
|
@ -361,11 +361,11 @@ same-const-env {x = x} rewrite var≟-refl x = refl
|
|||
and `const-env x v` maps `y` to `⊥, so long as `x ≢ y`.
|
||||
|
||||
```
|
||||
diff-nth-const-env : ∀{Γ} {x y : Γ ∋ ★} {v}
|
||||
diff-const-env : ∀{Γ} {x y : Γ ∋ ★} {v}
|
||||
→ x ≢ y
|
||||
-------------------
|
||||
→ const-env x v y ≡ ⊥
|
||||
diff-nth-const-env {Γ} {x} {y} neq with x var≟ y
|
||||
diff-const-env {Γ} {x} {y} neq with x var≟ y
|
||||
... | yes eq = ⊥-elim (neq eq)
|
||||
... | no _ = refl
|
||||
```
|
||||
|
|
@ -400,7 +400,7 @@ subst-reflect-var {Γ}{Δ}{γ}{x}{v}{σ} xv
|
|||
const-env-ok : γ `⊢ σ ↓ const-env x v
|
||||
const-env-ok y with x var≟ y
|
||||
... | yes x≡y rewrite sym x≡y | same-const-env {Γ}{x}{v} = xv
|
||||
... | no x≢y rewrite diff-nth-const-env {Γ}{x}{y}{v} x≢y = ⊥-intro
|
||||
... | no x≢y rewrite diff-const-env {Γ}{x}{y}{v} x≢y = ⊥-intro
|
||||
```
|
||||
|
||||
|
||||
|
|
@ -527,8 +527,8 @@ subst-reflect (sub d lt) eq
|
|||
By the lemma `var-inv` we have `v′ ⊑ v₁`, so by the `up-env` lemma we
|
||||
have `(δ′ , v₁) ⊢ M′ ↓ v₂` and therefore `δ′ ⊢ ƛ M′ ↓ v₁ → v₂`. We
|
||||
also need to show that `δ `⊢ σ ↓ δ′`. Fix `k`. We have
|
||||
`(δ , v₁) ⊢ rename S_ σ k ↓ nth k δ′`. We then apply the lemma
|
||||
`rename-inc-reflect` to obtain `δ ⊢ σ k ↓ nth k δ′`, so this case is
|
||||
`(δ , v₁) ⊢ rename S_ σ k ↓ δ k′`. We then apply the lemma
|
||||
`rename-inc-reflect` to obtain `δ ⊢ σ k ↓ δ k′`, so this case is
|
||||
complete.
|
||||
|
||||
* Case `⊥-intro`: We choose `⊥` for `δ`.
|
||||
|
|
|
|||
Loading…
Reference in a new issue