Last active
April 16, 2026 09:26
-
-
Save jake-87/203b609433f6c0760d5fafafa4faa038 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| open import Relation.Binary.PropositionalEquality | |
| open import Data.Nat renaming (ℕ to Nat) | |
| open import Data.Fin | |
| open import Data.Empty | |
| open import Data.Unit | |
| open import Data.Sum | |
| open import Data.Vec | |
| open import Data.Product | |
| open import Relation.Nullary.Negation | |
| open import Data.Bool | |
| data Ty : Set where | |
| top : Ty | |
| bot : Ty | |
| bool : Ty | |
| _⇒_ : Ty → Ty → Ty | |
| Con : Nat → Set | |
| Con n = Vec Ty n | |
| data Tm : Nat → Set where | |
| Unit : ∀ {n} → Tm n | |
| Var : ∀ {n} → Fin n → Tm n | |
| App : ∀ {n} → Tm n → Tm n → Tm n | |
| Lam : ∀ {n} → Tm (suc n) → Tm n | |
| True : ∀ {n} → Tm n | |
| False : ∀ {n} → Tm n | |
| ITE : ∀ {n} → Tm n → Tm n → Tm n → Tm n | |
| data _⊢_⦂_ : ∀ {n} → Con n → Tm n → Ty → Set where | |
| U : ∀ {n} (Γ : Con n) → Γ ⊢ Unit ⦂ top | |
| V : ∀ {n} (Γ : Con n) (v : Fin n) ty | |
| → lookup Γ v ≡ ty | |
| → Γ ⊢ Var v ⦂ ty | |
| A : ∀ {n} (Γ : Con n) (t₁ t₂ : Ty) (f x : Tm n) | |
| → Γ ⊢ f ⦂ (t₁ ⇒ t₂) | |
| → Γ ⊢ x ⦂ t₁ | |
| → Γ ⊢ App f x ⦂ t₂ | |
| L : ∀ {n} (Γ : Con n) (t₁ t₂ : Ty) (b : Tm (suc n)) | |
| → (t₁ ∷ Γ) ⊢ b ⦂ t₂ | |
| → Γ ⊢ Lam b ⦂ (t₁ ⇒ t₂) | |
| Tb : ∀ {n} {Γ : Con n} → Γ ⊢ True ⦂ bool | |
| Fb : ∀ {n} {Γ : Con n} → Γ ⊢ False ⦂ bool | |
| ITE : ∀ {n} (Γ : Con n) (c g h : Tm n) t₁ | |
| → Γ ⊢ c ⦂ bool | |
| → Γ ⊢ g ⦂ t₁ | |
| → Γ ⊢ h ⦂ t₁ | |
| → Γ ⊢ ITE c g h ⦂ t₁ | |
| ⟦_⟧t : Ty → Set | |
| ⟦ top ⟧t = ⊤ | |
| ⟦ bot ⟧t = ⊥ | |
| ⟦ a ⇒ b ⟧t = ⟦ a ⟧t → ⟦ b ⟧t | |
| ⟦ bool ⟧t = Bool | |
| ⟦_⟧c : ∀ {n} → Con n → Set | |
| ⟦ [] ⟧c = ⊤ | |
| ⟦ x ∷ Γ ⟧c = ⟦ x ⟧t × ⟦ Γ ⟧c | |
| ⟦_,_⟧ : ∀ {n} {Γ : Con n} {e : Tm n} {t} → Γ ⊢ e ⦂ t → ⟦ Γ ⟧c → ⟦ t ⟧t | |
| ⟦ U _ , p ⟧ = tt | |
| ⟦ V (x ∷ Γ) (suc v) _ k , (fst , snd) ⟧ = ⟦ V Γ v _ k , snd ⟧ | |
| ⟦ V (x ∷ Γ) zero _ refl , (fst , snd) ⟧ = fst | |
| ⟦ A _ t₁ _ f a b c , p ⟧ with ⟦ b , p ⟧ | |
| ... | b' = b' ⟦ c , p ⟧ | |
| ⟦ L _ t₁ t₂ b x , p ⟧ = λ v → ⟦ x , (v , p) ⟧ | |
| ⟦ Tb , p ⟧ = true | |
| ⟦ Fb , p ⟧ = false | |
| ⟦ ITE _ c g h _ a₁ a₂ a₃ , p ⟧ with ⟦ a₁ , p ⟧ | |
| ... | true = ⟦ a₂ , p ⟧ | |
| ... | false = ⟦ a₃ , p ⟧ | |
| ¬bot : ∀ {n} (Γ : Con n) (e : Tm n) → ⟦ Γ ⟧c → ¬ (Γ ⊢ e ⦂ bot) | |
| ¬bot [] e Γc (A .[] t₁ .bot f x v v₁) = ⟦ v , tt ⟧ ⟦ v₁ , tt ⟧ | |
| ¬bot [] e Γc (ITE .[] c g h .bot v v₁ v₂) = ¬bot [] g tt v₁ | |
| ¬bot (x ∷ Γ) e Γc (V .(bot ∷ Γ) zero .bot refl) = Γc .proj₁ | |
| ¬bot (x ∷ Γ) e Γc (V .(x ∷ Γ) (suc v) .bot x₁) = ¬bot Γ (Var v) (Γc .proj₂) (V Γ v bot x₁) | |
| ¬bot (x ∷ Γ) e Γc (A .(x ∷ Γ) t₁ .bot f x₁ v v₁) = ⟦ v , Γc ⟧ ⟦ v₁ , Γc ⟧ | |
| ¬bot (x ∷ Γ) e Γc (ITE .(x ∷ Γ) c g h .bot v v₁ v₂) = ¬bot (x ∷ Γ) g Γc v₁ | |
| -- Bottom is not inhabited. | |
| ¬bot-zero : ∀ (e : Tm 0) → ¬ ([] ⊢ e ⦂ bot) | |
| ¬bot-zero e x = ¬bot [] e tt x | |
| f-extend : ∀ {n k} → (Fin n → Fin k) → Fin (suc n) → Fin (suc k) | |
| f-extend f zero = zero | |
| f-extend f (suc x) = suc (f x) | |
| rename : ∀ {n k} → (Fin n → Fin k) → Tm n → Tm k | |
| rename f Unit = Unit | |
| rename f (Var x) = Var (f x) | |
| rename f (App g x) = App (rename f g) (rename f x) | |
| rename f (Lam x) = Lam (rename (f-extend f) x) | |
| rename f True = True | |
| rename f False = False | |
| rename f (ITE c t x) = ITE (rename f c) (rename f t) (rename f x) | |
| incr : ∀ {n} → Tm n → Tm (suc n) | |
| incr x = rename suc x | |
| extend : ∀ {n k} → (Fin n → Tm k) → Fin (suc n) → Tm (suc k) | |
| extend f zero = Var zero | |
| extend f (suc x) = incr (f x) | |
| [σ_]_ : ∀ {n k} → (Fin n → Tm k) → Tm n → Tm k | |
| [σ f ] Unit = Unit | |
| [σ f ] Var x = f x | |
| [σ f ] App a b = App ([σ f ] a) ([σ f ] b) | |
| [σ f ] Lam x = Lam ([σ extend f ] x) | |
| [σ f ] True = True | |
| [σ f ] False = False | |
| [σ g ] ITE c t f = ITE ([σ g ] c) ([σ g ] t) ([σ g ] f) | |
| sub-down : ∀ {n} → Tm n → Fin (suc n) → Tm n | |
| sub-down x zero = x | |
| sub-down x (suc f) = Var f | |
| _[:=_] : ∀ {n} → Tm (suc n) → Tm n → Tm n | |
| x [:= y ] = [σ sub-down y ] x | |
| data _~>_ : ∀ {n} → Tm n → Tm n → Set where | |
| ~ITE : ∀ {n} {c c' t f : Tm n} | |
| → c ~> c' | |
| → ITE c t f ~> ITE c' t f | |
| ~ITEβ₁ : ∀ {n} {t f : Tm n} | |
| → ITE True t f ~> t | |
| ~ITEβ₂ : ∀ {n} {t f : Tm n} | |
| → ITE False t f ~> f | |
| ~APPᵣ : ∀ {n} {f f' x : Tm n} | |
| → f ~> f' | |
| → App f x ~> App f' x | |
| ~APPβ : ∀ {n} {f : Tm (suc n)} {x : Tm n} {k : Tm n} | |
| → k ≡ f [:= x ] | |
| → App (Lam f) x ~> k | |
| data _~>*_ : ∀ {n} → Tm n → Tm n → Set where | |
| *refl : ∀ {n} (x : Tm n) → x ~>* x | |
| *tran : ∀ {n} {x z : Tm n} {y : Tm n} | |
| → x ~> y | |
| → y ~>* z | |
| → x ~>* z | |
| is-renaming-wrt : ∀ {n k} (Γ : Con n) (Δ : Con k) | |
| → (f : Fin n → Fin k) | |
| → Set | |
| is-renaming-wrt Γ Δ f = ∀ i → lookup Δ (f i) ≡ lookup Γ i | |
| is-renaming-ext : ∀ {n k} (Γ : Con n) (Δ : Con k) | |
| → (f : Fin n → Fin k) | |
| → is-renaming-wrt Γ Δ f | |
| → ∀ {t} | |
| → is-renaming-wrt (t ∷ Γ) (t ∷ Δ) (f-extend f) | |
| is-renaming-ext Γ Δ f x zero = refl | |
| is-renaming-ext Γ Δ f x (suc i) = x i | |
| rename! : ∀ {n k} (Γ : Con n) (Δ : Con k) (f : Fin n → Fin k) | |
| → is-renaming-wrt Γ Δ f | |
| → ∀ x {t} | |
| → Γ ⊢ x ⦂ t | |
| → Δ ⊢ rename f x ⦂ t | |
| rename! Γ Δ f ren Unit (U .Γ) = U Δ | |
| rename! Γ Δ f ren (Var x) (V .Γ .x _ refl) = | |
| V Δ (f x) _ (ren x) | |
| rename! Γ Δ f ren (App x x₁) (A .Γ t₁ _ .x .x₁ j j₁) = | |
| A Δ t₁ _ (rename f x) (rename f x₁) (rename! Γ Δ f ren x j) | |
| (rename! Γ Δ f ren x₁ j₁) | |
| rename! Γ Δ f ren (Lam x) (L .Γ t₁ t₂ .x j) = | |
| L Δ t₁ t₂ (rename (f-extend f) x) | |
| (rename! _ _ (f-extend f) (is-renaming-ext Γ Δ f ren) x j) | |
| rename! Γ Δ f ren True Tb = Tb | |
| rename! Γ Δ f ren False Fb = Fb | |
| rename! Γ Δ f ren (ITE x x₁ x₂) (ITE .Γ .x .x₁ .x₂ _ j j₁ j₂) = | |
| ITE Δ (rename f x) (rename f x₁) (rename f x₂) _ | |
| (rename! Γ Δ f ren x j) | |
| (rename! Γ Δ f ren x₁ j₁) | |
| (rename! Γ Δ f ren x₂ j₂) | |
| incr! : ∀ {n} (Γ : Con n) (e : Tm n) t | |
| → Γ ⊢ e ⦂ t | |
| → (t ∷ Γ) ⊢ incr e ⦂ t | |
| incr! Γ e t x = rename! Γ (t ∷ Γ) suc (λ i → refl) e x | |
| is-subst-wrt : ∀ {n k} (Γ : Con n) (Δ : Con k) | |
| → (f : Fin n → Tm k) | |
| → Set | |
| is-subst-wrt Γ Δ f = ∀ i {t} → lookup Γ i ≡ t → Δ ⊢ f i ⦂ t | |
| extend! : ∀ {n k} (Γ : Con n) (Δ : Con k) | |
| → (f : Fin n → Tm k) | |
| → ∀ t | |
| → is-subst-wrt Γ Δ f | |
| → is-subst-wrt (t ∷ Γ) (t ∷ Δ) (extend f) | |
| extend! Γ Δ f t x zero s = V (t ∷ Δ) zero _ s | |
| extend! Γ Δ f t x (suc i) s = | |
| rename! Δ (t ∷ Δ) suc (λ i₁ → refl) (f i) (x i s) | |
| [σ]! : ∀ {n k} (Γ : Con n) (Δ : Con k) | |
| → (f : Fin n → Tm k) | |
| → is-subst-wrt Γ Δ f | |
| → ∀ e {t} | |
| → Γ ⊢ e ⦂ t | |
| → Δ ⊢ [σ f ] e ⦂ t | |
| [σ]! Γ Δ f σ Unit (U .Γ) = U Δ | |
| [σ]! Γ Δ f σ (Var x) (V .Γ .x _ j) = σ x j | |
| [σ]! Γ Δ f σ (App a b) (A .Γ t₁ _ .a .b j j₁) = | |
| A Δ _ _ ([σ f ] a) ([σ f ] b) | |
| ([σ]! Γ Δ f σ a j) ([σ]! Γ Δ f σ b j₁) | |
| [σ]! Γ Δ f σ (Lam e) (L .Γ t₁ t₂ .e j) = | |
| L Δ t₁ t₂ ([σ extend f ] e) | |
| ([σ]! (t₁ ∷ Γ) (t₁ ∷ Δ) (extend f) (extend! Γ Δ f t₁ σ) e j) | |
| [σ]! Γ Δ f σ True Tb = Tb | |
| [σ]! Γ Δ f σ False Fb = Fb | |
| [σ]! Γ Δ f σ (ITE c y n) (ITE .Γ .c .y .n _ j y' n') = | |
| ITE Δ ([σ f ] c) ([σ f ] y) ([σ f ] n) _ | |
| ([σ]! Γ Δ f σ c j) | |
| ([σ]! Γ Δ f σ y y') | |
| ([σ]! Γ Δ f σ n n') | |
| sub-down! : ∀ {n} (Γ : Con n) t x | |
| → Γ ⊢ x ⦂ t | |
| → is-subst-wrt (t ∷ Γ) Γ (sub-down x) | |
| sub-down! Γ t x p zero refl = p | |
| sub-down! Γ t x p (suc i) j = V Γ i _ j | |
| [:=]! : ∀ {n} (Γ : Con n) (f : Tm (suc n)) x t₁ t₂ | |
| → (t₁ ∷ Γ) ⊢ f ⦂ t₂ | |
| → Γ ⊢ x ⦂ t₁ | |
| → Γ ⊢ f [:= x ] ⦂ t₂ | |
| [:=]! Γ Unit x t₁ t₂ (U .(t₁ ∷ Γ)) j₂ = U Γ | |
| [:=]! Γ (Var zero) x t₁ t₂ (V .(t₁ ∷ Γ) .zero .(lookup (t₁ ∷ Γ) zero) refl) j₂ = j₂ | |
| [:=]! Γ (Var (suc x₁)) x t₁ t₂ (V .(t₁ ∷ Γ) .(suc x₁) .t₂ x₂) j₂ = V Γ x₁ t₂ x₂ | |
| [:=]! Γ (App f f₁) x t₁ t₂ (A .(t₁ ∷ Γ) t₃ .t₂ .f .f₁ j₁ j₃) j₂ = | |
| A Γ t₃ t₂ ([σ sub-down x ] f) ([σ sub-down x ] f₁) | |
| ([:=]! Γ f x t₁ (t₃ ⇒ t₂) j₁ j₂) ([:=]! Γ f₁ x t₁ t₃ j₃ j₂) | |
| [:=]! Γ (Lam f) x t₁ t₂ (L .(t₁ ∷ Γ) t₃ t₄ .f j₁) j₂ = | |
| L Γ t₃ t₄ ([σ extend (sub-down x) ] f) | |
| ([σ]! _ _ (extend (sub-down x)) | |
| (extend! (t₁ ∷ Γ) Γ (sub-down x) t₃ (sub-down! Γ t₁ x j₂)) f j₁) | |
| [:=]! Γ True x t₁ t₂ Tb j₂ = Tb | |
| [:=]! Γ False x t₁ t₂ Fb j₂ = Fb | |
| [:=]! Γ (ITE f f₁ f₂) x t₁ t₂ (ITE .(t₁ ∷ Γ) .f .f₁ .f₂ .t₂ j₁ j₃ j₄) j₂ = | |
| ITE Γ | |
| ([σ sub-down x ] f) | |
| ([σ sub-down x ] f₁) | |
| ([σ sub-down x ] f₂) t₂ | |
| ([:=]! Γ f x t₁ bool j₁ j₂) | |
| ([:=]! Γ f₁ x t₁ t₂ j₃ j₂) | |
| ([:=]! Γ f₂ x t₁ t₂ j₄ j₂) | |
| -- Reduction is type safe. | |
| ~>! : ∀ {n} (Γ : Con n) (e e' : Tm n) t | |
| → Γ ⊢ e ⦂ t | |
| → e ~> e' | |
| → Γ ⊢ e' ⦂ t | |
| ~>! Γ (App e e₁) e' t (A .Γ t₁ .t .e .e₁ j j₁) (~APPᵣ r) = | |
| A Γ t₁ t _ e₁ (~>! Γ e _ (t₁ ⇒ t) j r) j₁ | |
| ~>! Γ (App e e₁) e' t (A .Γ t₁ .t .(Lam _) .e₁ (L .Γ .t₁ .t _ j) j₁) (~APPβ refl) = | |
| [:=]! Γ _ e₁ _ _ j j₁ | |
| ~>! Γ (ITE e e₁ e₂) e' t (ITE .Γ .e .e₁ .e₂ .t j j₁ j₂) (~ITE r) = | |
| ITE Γ _ e₁ e₂ t (~>! Γ e _ bool j r) j₁ j₂ | |
| ~>! Γ (ITE e e₁ e₂) e' t (ITE .Γ .True .e₁ .e₂ .t j j₁ j₂) ~ITEβ₁ = j₁ | |
| ~>! Γ (ITE e e₁ e₂) e' t (ITE .Γ .False .e₁ .e₂ .t j j₁ j₂) ~ITEβ₂ = j₂ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment