agda style in BigStep
This commit is contained in:
Jeremy Siek
parent
d9e07b0549
commit
0e27b583c2
1 changed files with 38 additions and 40 deletions
|
|
@ -34,15 +34,15 @@ single sub-computation has been completed.
|
|||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; trans; sym; cong-app)
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
using (_≡_; refl; trans; sym; cong-app)
|
||||
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Function using (_∘_)
|
||||
open import plfa.part2.Untyped
|
||||
using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_;
|
||||
subst; subst-zero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;
|
||||
—↠-trans; appL-cong)
|
||||
using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_;
|
||||
subst; subst-zero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;
|
||||
—↠-trans; appL-cong)
|
||||
open import plfa.part2.Substitution using (Subst; ids)
|
||||
```
|
||||
|
||||
|
|
@ -92,18 +92,18 @@ is a lambda abstraction.
|
|||
data _⊢_⇓_ : ∀{Γ} → ClosEnv Γ → (Γ ⊢ ★) → Clos → Set where
|
||||
|
||||
⇓-var : ∀{Γ}{γ : ClosEnv Γ}{x : Γ ∋ ★}{Δ}{δ : ClosEnv Δ}{M : Δ ⊢ ★}{V}
|
||||
→ γ x ≡ clos M δ
|
||||
→ δ ⊢ M ⇓ V
|
||||
-----------
|
||||
→ γ ⊢ ` x ⇓ V
|
||||
→ γ x ≡ clos M δ
|
||||
→ δ ⊢ M ⇓ V
|
||||
-----------
|
||||
→ γ ⊢ ` x ⇓ V
|
||||
|
||||
⇓-lam : ∀{Γ}{γ : ClosEnv Γ}{M : Γ , ★ ⊢ ★}
|
||||
→ γ ⊢ ƛ M ⇓ clos (ƛ M) γ
|
||||
→ γ ⊢ ƛ M ⇓ clos (ƛ M) γ
|
||||
|
||||
⇓-app : ∀{Γ}{γ : ClosEnv Γ}{L M : Γ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N : Δ , ★ ⊢ ★}{V}
|
||||
→ γ ⊢ L ⇓ clos (ƛ N) δ → (δ ,' clos M γ) ⊢ N ⇓ V
|
||||
---------------------------------------------------
|
||||
→ γ ⊢ L · M ⇓ V
|
||||
→ γ ⊢ L ⇓ clos (ƛ N) δ → (δ ,' clos M γ) ⊢ N ⇓ V
|
||||
---------------------------------------------------
|
||||
→ γ ⊢ L · M ⇓ V
|
||||
```
|
||||
|
||||
* The `⇓-var` rule evaluates a variable by finding the associated
|
||||
|
|
@ -139,10 +139,10 @@ straightforward induction on the two big-step derivations.
|
|||
|
||||
```
|
||||
⇓-determ : ∀{Γ}{γ : ClosEnv Γ}{M : Γ ⊢ ★}{V V' : Clos}
|
||||
→ γ ⊢ M ⇓ V → γ ⊢ M ⇓ V'
|
||||
→ V ≡ V'
|
||||
→ γ ⊢ M ⇓ V → γ ⊢ M ⇓ V'
|
||||
→ V ≡ V'
|
||||
⇓-determ (⇓-var eq1 mc) (⇓-var eq2 mc')
|
||||
with trans (sym eq1) eq2
|
||||
with trans (sym eq1) eq2
|
||||
... | refl = ⇓-determ mc mc'
|
||||
⇓-determ ⇓-lam ⇓-lam = refl
|
||||
⇓-determ (⇓-app mc mc₁) (⇓-app mc' mc'')
|
||||
|
|
@ -210,8 +210,7 @@ Of course, applying the identity substitution to a term returns
|
|||
the same term.
|
||||
|
||||
```
|
||||
sub-id : ∀{Γ} {A} {M : Γ ⊢ A}
|
||||
→ subst ids M ≡ M
|
||||
sub-id : ∀{Γ} {A} {M : Γ ⊢ A} → subst ids M ≡ M
|
||||
sub-id = plfa.part2.Substitution.sub-id
|
||||
```
|
||||
|
||||
|
|
@ -237,7 +236,7 @@ Chapter [Substitution]({{ site.baseurl }}/Substitution/).
|
|||
|
||||
```
|
||||
subst-zero-exts : ∀{Γ Δ}{σ : Subst Γ Δ}{B}{M : Δ ⊢ B}{x : Γ ∋ ★}
|
||||
→ (subst (subst-zero M) ∘ exts σ) (S x) ≡ σ x
|
||||
→ (subst (subst-zero M) ∘ exts σ) (S x) ≡ σ x
|
||||
subst-zero-exts {Γ}{Δ}{σ}{B}{M}{x} =
|
||||
cong-app (plfa.part2.Substitution.subst-zero-exts-cons{σ = σ}) (S x)
|
||||
```
|
||||
|
|
@ -246,9 +245,9 @@ So the proof of `≈ₑ-ext` is as follows.
|
|||
|
||||
```
|
||||
≈ₑ-ext : ∀ {Γ} {γ : ClosEnv Γ} {σ : Subst Γ ∅} {V} {N : ∅ ⊢ ★}
|
||||
→ γ ≈ₑ σ → V ≈ N
|
||||
--------------------------
|
||||
→ (γ ,' V) ≈ₑ (ext-subst σ N)
|
||||
→ γ ≈ₑ σ → V ≈ N
|
||||
--------------------------
|
||||
→ (γ ,' V) ≈ₑ (ext-subst σ N)
|
||||
≈ₑ-ext {Γ} {γ} {σ} {V} {N} γ≈ₑσ V≈N {Z} = V≈N
|
||||
≈ₑ-ext {Γ} {γ} {σ} {V} {N} γ≈ₑσ V≈N {S x}
|
||||
rewrite subst-zero-exts {σ = σ}{M = N}{x} = γ≈ₑσ
|
||||
|
|
@ -270,7 +269,7 @@ composing the two substitutions and then applying them.
|
|||
|
||||
```
|
||||
sub-sub : ∀{Γ Δ Σ}{A}{M : Γ ⊢ A} {σ₁ : Subst Γ Δ}{σ₂ : Subst Δ Σ}
|
||||
→ subst σ₂ (subst σ₁ M) ≡ subst (subst σ₂ ∘ σ₁) M
|
||||
→ subst σ₂ (subst σ₁ M) ≡ subst (subst σ₂ ∘ σ₁) M
|
||||
sub-sub {M = M} = plfa.part2.Substitution.sub-sub {M = M}
|
||||
```
|
||||
|
||||
|
|
@ -287,22 +286,22 @@ below.
|
|||
⇓→—↠×𝔹 {γ = γ} (⇓-var{x = x} γx≡Lδ δ⊢L⇓V) γ≈ₑσ
|
||||
with γ x | γ≈ₑσ {x} | γx≡Lδ
|
||||
... | clos L δ | ⟨ τ , ⟨ δ≈ₑτ , σx≡τL ⟩ ⟩ | refl
|
||||
with ⇓→—↠×𝔹{σ = τ} δ⊢L⇓V δ≈ₑτ
|
||||
... | ⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩ rewrite σx≡τL =
|
||||
⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩
|
||||
with ⇓→—↠×𝔹{σ = τ} δ⊢L⇓V δ≈ₑτ
|
||||
... | ⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩ rewrite σx≡τL =
|
||||
⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩
|
||||
⇓→—↠×𝔹 {σ = σ} {V = clos (ƛ N) γ} ⇓-lam γ≈ₑσ =
|
||||
⟨ subst σ (ƛ N) , ⟨ subst σ (ƛ N) ∎ , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩
|
||||
⇓→—↠×𝔹{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ
|
||||
with ⇓→—↠×𝔹{σ = σ} L⇓ƛNδ γ≈ₑσ
|
||||
... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN
|
||||
with ⇓→—↠×𝔹 {σ = ext-subst τ (subst σ M)} N⇓V
|
||||
(λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x})
|
||||
| β{∅}{subst (exts τ) N}{subst σ M}
|
||||
... | ⟨ N' , ⟨ —↠N' , V≈N' ⟩ ⟩ | ƛτN·σM—→
|
||||
rewrite sub-sub{M = N}{σ₁ = exts τ}{σ₂ = subst-zero (subst σ M)} =
|
||||
let rs = (ƛ subst (exts τ) N) · subst σ M —→⟨ ƛτN·σM—→ ⟩ —↠N' in
|
||||
let g = —↠-trans (appL-cong σL—↠ƛτN) rs in
|
||||
⟨ N' , ⟨ g , V≈N' ⟩ ⟩
|
||||
with ⇓→—↠×𝔹 {σ = ext-subst τ (subst σ M)} N⇓V
|
||||
(λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x})
|
||||
| β{∅}{subst (exts τ) N}{subst σ M}
|
||||
... | ⟨ N' , ⟨ —↠N' , V≈N' ⟩ ⟩ | ƛτN·σM—→
|
||||
rewrite sub-sub{M = N}{σ₁ = exts τ}{σ₂ = subst-zero (subst σ M)} =
|
||||
let rs = (ƛ subst (exts τ) N) · subst σ M —→⟨ ƛτN·σM—→ ⟩ —↠N' in
|
||||
let g = —↠-trans (appL-cong σL—↠ƛτN) rs in
|
||||
⟨ N' , ⟨ g , V≈N' ⟩ ⟩
|
||||
```
|
||||
|
||||
The proof is by induction on `γ ⊢ M ⇓ V`. We have three cases
|
||||
|
|
@ -364,14 +363,13 @@ of the equivalence between the big-step semantics and beta reduction.
|
|||
|
||||
```
|
||||
cbn→reduce : ∀{M : ∅ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N′ : Δ , ★ ⊢ ★}
|
||||
→ ∅' ⊢ M ⇓ clos (ƛ N′) δ
|
||||
-----------------------------
|
||||
→ Σ[ N ∈ ∅ , ★ ⊢ ★ ] (M —↠ ƛ N)
|
||||
→ ∅' ⊢ M ⇓ clos (ƛ N′) δ
|
||||
-----------------------------
|
||||
→ Σ[ N ∈ ∅ , ★ ⊢ ★ ] (M —↠ ƛ N)
|
||||
cbn→reduce {M}{Δ}{δ}{N′} M⇓c
|
||||
with ⇓→—↠×𝔹{σ = ids} M⇓c ≈ₑ-id
|
||||
... | ⟨ N , ⟨ rs , ⟨ σ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩
|
||||
rewrite sub-id{M = M} | eq2 =
|
||||
⟨ subst (exts σ) N′ , rs ⟩
|
||||
... | ⟨ N , ⟨ rs , ⟨ σ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩ rewrite sub-id{M = M} | eq2 =
|
||||
⟨ subst (exts σ) N′ , rs ⟩
|
||||
```
|
||||
|
||||
#### Exercise `big-alt-implies-multi` (practice)
|
||||
|
|
|
|||
Loading…
Reference in a new issue