ouais

src/LambdaPi.agda

@@ -0,0 +1,81 @@
+module LambdaPi where
+
+open import Data.Nat using (ℕ; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (yes; no; ¬_)
+
+infix  4 _—→_
+infix  5  ƛ_
+infixl 7  _·_
+infix  9  `_
+infix  9 _[_:=_]
+
+data Term : Set where
+  -- var
+  `_ : ℕ → Term
+
+  -- lam
+  ƛ_ : Term → Term
+
+  -- app
+  _·_ : Term → Term → Term
+
+data Value : Term → Set where
+  -- lam is a value
+  V-ƛ : ∀ {N} → Value (ƛ N)
+
+----------------------------------------------------
+-- substitution
+----------------------------------------------------
+_[_:=_] : Term → ℕ → Term → Term
+
+-- var
+(` n₁) [ n₂ := V ] with n₁ ≟ n₂
+... | yes _ = V
+... | no _ = ` n₁
+
+-- lam 
+(ƛ N) [ n := V ] = ƛ (N [ suc n := V ])
+
+-- app
+(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
+
+----------------------------------------------------
+-- reduction
+----------------------------------------------------
+data _—→_ : Term → Term → Set where
+  -- beta reduction for lambda applications
+  β-ƛ : ∀ {x N V} → Value V → (ƛ N) · V —→ N [ x := V ]
+
+----------------------------------------------------
+-- typing
+----------------------------------------------------
+data Type : Set where
+  _⇒_ : Type → Type → Type
+  `ℕ : Type
+
+----------------------------------------------------
+-- typing context
+----------------------------------------------------
+data Context : Set where
+  ∅ : Context
+  _::_ : Type → Context
+
+----------------------------------------------------
+-- typing judgment
+----------------------------------------------------
+data _⊢_⦂_ : Context → Term → Type → Set where
+
+----------------------------------------------------
+-- progress
+----------------------------------------------------
+data Progress (M : Term) : Set where
+  step : ∀ {N} → M —→ N → Progress M
+  done : Value M → Progress M
+
+progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
+
+----------------------------------------------------
+-- preservation
+----------------------------------------------------
+preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A