homework 3 start
This commit is contained in:
parent
8c4fe03730
commit
fbc44a0f78
GPG key ID:
BDA47A31A3C8EE6B
5 changed files with 318 additions and 3 deletions
4
.vscode/settings.json
vendored
4
.vscode/settings.json
vendored
|
|
@ -1,7 +1,7 @@
|
|||
{
|
||||
"editor.fontFamily": "'Roboto Mono', 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'",
|
||||
"editor.fontSize": 15,
|
||||
"vim.insertModeKeyBindings": [
|
||||
{ "before": ["k", "j"], "after": ["<Esc>"] }
|
||||
]
|
||||
],
|
||||
"editor.fontFamily": "\"PragmataPro Mono Liga\", \"Roboto Mono\", 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'"
|
||||
}
|
||||
48
src/Homework3.agda
Normal file
48
src/Homework3.agda
Normal file
|
|
@ -0,0 +1,48 @@
|
|||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
open import Homework3Prelude
|
||||
|
||||
module Homework3 where
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 1
|
||||
---------------------------------------------------------
|
||||
|
||||
V¬—→ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ ⊢ A}
|
||||
→ Value M
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 2
|
||||
---------------------------------------------------------
|
||||
|
||||
mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
mul = μ -- *
|
||||
ƛ -- m
|
||||
ƛ -- n
|
||||
(case (# 1)
|
||||
-- case `zero
|
||||
(# 0)
|
||||
|
||||
-- case `suc
|
||||
(plus · # 0 · (# 3 · # 1 · # 0))
|
||||
)
|
||||
|
||||
task2 : mul {∅} · one · one —↠ one
|
||||
task2 =
|
||||
begin
|
||||
mul {∅} · (`suc `zero) · (`suc `zero)
|
||||
—→⟨ {! !} ⟩
|
||||
mul [ μ mul ] · (`suc `zero) · (`suc `zero)
|
||||
—→⟨ {! !} ⟩
|
||||
mul [ μ mul ] [ `suc `zero ] · (`suc `zero)
|
||||
—→⟨ {! !} ⟩
|
||||
one
|
||||
∎
|
||||
240
src/Homework3Prelude.agda
Normal file
240
src/Homework3Prelude.agda
Normal file
|
|
@ -0,0 +1,240 @@
|
|||
-- This file contains the code extracted from the DeBruijn chapter in PLFA
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
|
||||
module Homework3Prelude where
|
||||
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_ : Context → Type → Context
|
||||
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A}
|
||||
---------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ A
|
||||
---------
|
||||
→ Γ , B ∋ A
|
||||
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
`_ : ∀ {Γ A}
|
||||
→ Γ ∋ A
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
ƛ_ : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A ⇒ B
|
||||
→ Γ ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
---------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc_ : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
----------
|
||||
→ Γ ⊢ A
|
||||
|
||||
μ_ : ∀ {Γ A}
|
||||
→ Γ , A ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
|
||||
length : Context → ℕ
|
||||
length ∅ = zero
|
||||
length (Γ , _) = suc (length Γ)
|
||||
|
||||
lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
|
||||
lookup {(_ , A)} {zero} (s≤s z≤n) = A
|
||||
lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p
|
||||
|
||||
count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
|
||||
count {_ , _} {zero} (s≤s z≤n) = Z
|
||||
count {Γ , _} {(suc n)} (s≤s p) = S (count p)
|
||||
|
||||
#_ : ∀ {Γ}
|
||||
→ (n : ℕ)
|
||||
→ {n∈Γ : True (suc n ≤? length Γ)}
|
||||
--------------------------------
|
||||
→ Γ ⊢ lookup (toWitness n∈Γ)
|
||||
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
|
||||
|
||||
one : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
one = `suc `zero
|
||||
|
||||
two : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
two = `suc `suc `zero
|
||||
|
||||
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
|
||||
|
||||
ext : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
|
||||
ext ρ Z = Z
|
||||
ext ρ (S x) = S (ρ x)
|
||||
|
||||
rename : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
|
||||
exts : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
|
||||
exts σ Z = ` Z
|
||||
exts σ (S x) = rename S_ (σ x)
|
||||
|
||||
subst : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , B ⊢ A
|
||||
→ Γ ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
|
||||
where
|
||||
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
|
||||
σ Z = M
|
||||
σ (S x) = ` x
|
||||
|
||||
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||
|
||||
V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
|
||||
---------------------------
|
||||
→ Value (ƛ N)
|
||||
|
||||
V-zero : ∀ {Γ}
|
||||
-----------------
|
||||
→ Value (`zero {Γ})
|
||||
|
||||
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
|
||||
→ L —→ L′
|
||||
---------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
|
||||
→ Value V
|
||||
→ M —→ M′
|
||||
---------------
|
||||
→ V · M —→ V · M′
|
||||
|
||||
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
|
||||
→ Value W
|
||||
--------------------
|
||||
→ (ƛ N) · W —→ N [ W ]
|
||||
|
||||
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
|
||||
→ M —→ M′
|
||||
-----------------
|
||||
→ `suc M —→ `suc M′
|
||||
|
||||
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ L —→ L′
|
||||
-------------------------
|
||||
→ case L M N —→ case L′ M N
|
||||
|
||||
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
-------------------
|
||||
→ case `zero M N —→ M
|
||||
|
||||
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ Value V
|
||||
----------------------------
|
||||
→ case (`suc V) M N —→ N [ V ]
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
----------------
|
||||
→ μ N —→ N [ μ N ]
|
||||
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_∎ : (M : Γ ⊢ A)
|
||||
------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
→ M —↠ N
|
||||
------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
||||
27
src/LambdaTest.agda
Normal file
27
src/LambdaTest.agda
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
module LambdaTest where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
using (_≡_; _≢_; refl; sym; cong; cong₂)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Nat using (ℕ; zero; suc)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Product
|
||||
using (_×_; proj₁; proj₂; ∃; ∃-syntax)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Function using (_∘_)
|
||||
V¬—→ V-ƛ = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) (ξ-suc m) = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) = ?
|
||||
open import plfa.part2.Lambda
|
||||
|
||||
V¬—→ : ∀ {M N}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
||||
|
|
@ -1082,7 +1082,7 @@ Context≃List = record
|
|||
{ from = contextOfList
|
||||
; to = listOfContext
|
||||
; from∘to = contextListIso
|
||||
; to∘from = ?
|
||||
; to∘from = listContextIso
|
||||
}
|
||||
```
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue