Last active
April 20, 2026 15:20
-
-
Save jake-87/327d3812dcd0454afd33c5dc5bbc2f3b 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 hiding (_≤_; _≟_) | |
| open import Data.Empty | |
| open import Data.Unit hiding (_≟_) | |
| open import Data.Sum | |
| open import Data.Vec | |
| open import Data.Product renaming (proj₁ to fst; proj₂ to snd) | |
| open import Relation.Nullary.Negation | |
| open import Data.Bool hiding (_≤_; _≟_) | |
| open import Function.Base | |
| 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 .fst | |
| ¬bot (x ∷ Γ) e Γc (V .(x ∷ Γ) (suc v) .bot x₁) = ¬bot Γ (Var v) (Γc .snd) (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₁ | |
| ¬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 | |
| chain-length : ∀ {n} {e v : Tm n} → e ~>* v → Set | |
| chain-length (*refl _) = ⊤ | |
| chain-length (*tran x xs) = ⊤ × chain-length xs | |
| compose~> : ∀ {n} {a b c : Tm n} → a ~>* b → b ~>* c → a ~>* c | |
| compose~> (*refl ._) y = y | |
| compose~> (*tran x x₁) y = *tran x (compose~> x₁ y) | |
| 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₂ | |
| ~>*! : ∀ {n} (Γ : Con n) (e e' : Tm n) t | |
| → Γ ⊢ e ⦂ t | |
| → e ~>* e' | |
| → Γ ⊢ e' ⦂ t | |
| ~>*! Γ e e' t j (*refl .e) = j | |
| ~>*! Γ e e' t j (*tran x r) with ~>! Γ e _ t j x | |
| ... | p = ~>*! Γ _ e' t p r | |
| -- Reduction is determininstic. | |
| ITE-inj : ∀ {n} {a b c d e f : Tm n} → a ≡ d → b ≡ e → c ≡ f → ITE a b c ≡ ITE d e f | |
| ITE-inj refl refl refl = refl | |
| ~>-det : ∀ {n} (e : Tm n) v₁ v₂ → e ~> v₁ → e ~> v₂ → v₁ ≡ v₂ | |
| ~>-det (App e e₁) v₁ v₂ (~APPᵣ r₁) (~APPᵣ r₂) = cong₂ App (~>-det e _ _ r₁ r₂) refl | |
| ~>-det (App e e₁) v₁ v₂ (~APPβ x) (~APPβ x₁) = trans x (sym x₁) | |
| ~>-det {n} (ITE e e₁ e₂) v₁ v₂ (~ITE r₁) (~ITE r₂) = ITE-inj (~>-det e _ _ r₁ r₂) refl refl | |
| ~>-det (ITE e e₁ e₂) v₁ v₂ ~ITEβ₁ ~ITEβ₁ = refl | |
| ~>-det (ITE e e₁ e₂) v₁ v₂ ~ITEβ₂ ~ITEβ₂ = refl | |
| ~>-step-det : ∀ {n} {e : Tm n} {v} → (r₁ : e ~> v) → (r₂ : e ~> v) → r₁ ≡ r₂ | |
| ~>-step-det (~ITE r₁) (~ITE r₂) = cong ~ITE (~>-step-det r₁ r₂) | |
| ~>-step-det ~ITEβ₁ ~ITEβ₁ = refl | |
| ~>-step-det ~ITEβ₂ ~ITEβ₂ = refl | |
| ~>-step-det (~APPᵣ r₁) (~APPᵣ r₂) = cong ~APPᵣ (~>-step-det r₁ r₂) | |
| ~>-step-det (~APPβ x) (~APPβ x₁) = cong ~APPβ UIP | |
| where | |
| UIP : ∀ {A : Set} {a b : A} {p q : a ≡ b} → p ≡ q | |
| UIP {A₁} {a} {b} {refl} {refl} = refl | |
| data Value : ∀ {n} → Tm n → Set where | |
| V/Unit : ∀ {n} → Value {n} Unit | |
| V/True : ∀ {n} → Value {n} True | |
| V/False : ∀ {n} → Value {n} False | |
| V/Lam : ∀ {n} (e : Tm (suc n)) → Value {n} (Lam e) | |
| Value¬~> : ∀ {n} {e : Tm n} → Value e → ¬ (Σ _ λ v → e ~> v) | |
| Value¬~> V/Unit () | |
| Value¬~> V/True () | |
| Value¬~> V/False () | |
| Value¬~> (V/Lam e) () | |
| Value-unique : ∀ {n} {e : Tm n} → (a b : Value e) → a ≡ b | |
| Value-unique {n} {Unit} V/Unit V/Unit = refl | |
| Value-unique {n} {Lam e} (V/Lam .e) (V/Lam .e) = refl | |
| Value-unique {n} {True} V/True V/True = refl | |
| Value-unique {n} {False} V/False V/False = refl | |
| record _↓ {n} (x : Tm n) : Set where | |
| constructor ↓[_,_,_] | |
| field | |
| value : Tm n | |
| reduces : x ~>* value | |
| is-value : Value value | |
| ↓-step : ∀ {n} (e e' : Tm n) → e ~> e' → e' ↓ → e ↓ | |
| ↓-step e e' r ↓[ value , reduces , is-value ] = ↓[ value , *tran r reduces , is-value ] | |
| postulate funext : ∀ {ℓ} {A B : Set ℓ} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g | |
| ι : ∀ {n} → Fin n → Tm n | |
| ι x = Var x | |
| extend-ι : ∀ {n} → extend (ι {n}) ≡ ι | |
| extend-ι = funext uh | |
| where | |
| uh : (x : Fin (suc _)) → extend ι x ≡ ι x | |
| uh zero = refl | |
| uh (suc x) = refl | |
| is-ι : ∀ {n} (e : Tm n) → [σ ι ] e ≡ e | |
| is-ι Unit = refl | |
| is-ι (Var x) = refl | |
| is-ι (App a b) = cong₂ App (is-ι a) (is-ι b) | |
| is-ι (Lam e) = cong Lam (subst (λ l → ([σ l ] e) ≡ e) (sym extend-ι) (is-ι e)) | |
| is-ι True = refl | |
| is-ι False = refl | |
| is-ι (ITE e e₁ e₂) = ITE-inj (is-ι e) (is-ι e₁) (is-ι e₂) | |
| WN : ∀ {n} {Γ : Con n} (t : Ty) (e : Tm n) → Set | |
| WN' : ∀ {n} {Γ : Con n} → (t : Ty) (e : Tm n) → Set | |
| WN {n} {Γ} t e = e ↓ × Γ ⊢ e ⦂ t × WN' {n} {Γ} t e | |
| WN' top e = ⊤ | |
| WN' bot e = ⊤ | |
| WN' bool e = ⊤ | |
| WN' {n} {Γ} (a ⇒ b) e = ∀ v → (pv : Γ ⊢ v ⦂ a) → WN {n} {Γ} a v → WN {n} {Γ} b (App e v) | |
| [_⦂_] : ∀ {n} (σ : Fin n → Tm 0) (Γ : Con n) → Set | |
| [_⦂_] σ Γ = is-subst-wrt Γ [] σ | |
| WNc : ∀ {n} (Γ : Con n) σ → [ σ ⦂ Γ ] → Set | |
| WNc Γ σ x = ∀ j → WN {_} {[]} (lookup Γ j) (σ j) | |
| _⊨_⦂_ : ∀ {n} (Γ : Con n) (e : Tm n) (t : Ty) → Set | |
| _⊨_⦂_ Γ e t = ∀ (j : Γ ⊢ e ⦂ t) σ → (sub : [ σ ⦂ Γ ]) → WNc Γ σ sub → WN {_} {[]} t ([σ σ ] e) | |
| wn : ∀ {n} (Γ : Con n) (t : Ty) (e : Tm n) → Γ ⊨ e ⦂ t | |
| wn Γ t Unit (U .Γ) σ sub ren = ↓[ Unit , *refl ([σ σ ] Unit) , V/Unit ] , U [] , tt | |
| wn Γ t (Var k) (V .Γ .k .(lookup Γ k) refl) σ sub ren = ren k | |
| wn Γ r (App a b) (A .Γ l .r .a .b j₁ j₂) σ sub ren with wn Γ (l ⇒ r) a j₁ σ sub ren | wn Γ l b j₂ σ sub ren | |
| ... | ar | br = ar .snd .snd ([σ σ ] b) (br .snd .fst) br | |
| wn {n} Γ τ (Lam e) (L .Γ t₁ t₂ .e j) σ sub ren = ↓[ [σ σ ] Lam e , *refl ([σ σ ] Lam e) , V/Lam ([σ extend σ ] e) ] | |
| , [σ]! Γ [] σ sub (Lam e) (L Γ t₁ t₂ e j) , wn' | |
| where | |
| bad : is-subst-wrt [] [] (λ ()) | |
| bad () x | |
| wn' : WN' (t₁ ⇒ t₂) ([σ σ ] Lam e) | |
| wn' v pv rv = ↓[ one ._↓.value , *tran (~APPβ refl) (one ._↓.reduces) , one ._↓.is-value ] | |
| , A [] t₁ t₂ ([σ σ ] Lam e) v (L [] t₁ t₂ ([σ extend σ ] e) ([σ]! (t₁ ∷ Γ) (t₁ ∷ []) (extend σ) (extend! Γ [] σ t₁ sub) e j)) pv , {!!} | |
| where | |
| uh : WN t₂ ([σ ι ] (([σ extend σ ] e) [:= v ])) | |
| uh = wn [] t₂ (([σ extend σ ] e) [:= v ]) | |
| ([:=]! [] ([σ extend σ ] e) v t₁ t₂ | |
| ([σ]! (t₁ ∷ Γ) (t₁ ∷ []) (extend σ) (extend! Γ [] σ t₁ sub) e j) pv) | |
| ι (λ ()) λ () | |
| ya : WN t₂ (([σ extend σ ] e) [:= v ]) | |
| ya = subst (λ l → WN t₂ l) (is-ι (([σ extend σ ] e) [:= v ])) uh | |
| one : (([σ extend σ ] e) [:= v ]) ↓ | |
| one = ya .fst | |
| two : [] ⊢ ([σ extend σ ] e) [:= v ] ⦂ t₂ | |
| two = ya .snd .fst | |
| thr : WN' t₂ (([σ extend σ ] e) [:= v ]) | |
| thr = ya .snd .snd | |
| wn Γ t True Tb σ sub ren = ↓[ True , *refl ([σ σ ] True) , V/True ] , Tb , tt | |
| wn Γ t False Fb σ sub ren = ↓[ False , *refl ([σ σ ] False) , V/False ] , Fb , tt | |
| wn Γ t (ITE e e₁ e₂) (ITE .Γ .e .e₁ .e₂ .t j j₁ j₂) σ sub ren = {!!} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment