module TypeSound.Target where
open import TypeSound.Common
infixr 5 ƛ_⇒_
infixl 7 _·_
infix 9 `_
data Record : Set
data Term : Set
data Term where
lit : ℕ → Term
flt : 𝔽 → Term
`_ : Id → Term
ƛ_⇒_ : Id → Term → Term
_·_ : Term → Term → Term
+ : Term
+i : ℕ → Term
+f : 𝔽 → Term
𝕣_ : Record → Term
_𝕡_ : Term → Label → Term
data Record where
rnil : Record
r⟦_↦_⟧_ : Label → Term → Record → Record
infix 4 _≤_
data _≤_ : Type → Type → Set where
s-int :
Int ≤ Int
s-flt :
Float ≤ Float
s-arr : ∀ {A B C D}
→ C ≤ A
→ B ≤ D
→ A ⇒ B ≤ C ⇒ D
s-top : ∀ {A}
→ A ≤ Top
s-and-l : ∀ {A B C}
→ A ≤ C
→ A & B ≤ C
s-and-r : ∀ {A B C}
→ B ≤ C
→ A & B ≤ C
s-and : ∀ {A B C}
→ A ≤ B
→ A ≤ C
→ A ≤ B & C
s-rcd : ∀ {l A B}
→ A ≤ B
→ τ⟦ l ↦ A ⟧ ≤ τ⟦ l ↦ B ⟧
s-refl : ∀ {A}
→ A ≤ A
s-refl {Top} = s-top
s-refl {Int} = s-int
s-refl {Float} = s-flt
s-refl {A ⇒ A₁} = s-arr s-refl s-refl
s-refl {A & A₁} = s-and (s-and-l s-refl) (s-and-r s-refl)
s-refl {τ⟦ x ↦ A ⟧} = s-rcd s-refl
inv-&-l : ∀ {A B C}
→ A ≤ B & C
→ A ≤ B
inv-&-r : ∀ {A B C}
→ A ≤ B & C
→ A ≤ C
inv-&-l (s-and-l A≤BC) = s-and-l (inv-&-l A≤BC)
inv-&-l (s-and-r A≤BC) = s-and-r (inv-&-l A≤BC)
inv-&-l (s-and A≤BC A≤BC₁) = A≤BC
inv-&-r (s-and-l A≤BC) = s-and-l (inv-&-r A≤BC)
inv-&-r (s-and-r A≤BC) = s-and-r (inv-&-r A≤BC)
inv-&-r (s-and A≤BC A≤BC₁) = A≤BC₁
≤-trans : ∀ {A B C}
→ A ≤ B
→ B ≤ C
→ A ≤ C
≤-trans {B = Top} A≤B s-top = A≤B
≤-trans {B = Top} A≤B (s-and B≤C B≤C₁) = s-and (≤-trans A≤B B≤C) (≤-trans A≤B B≤C₁)
≤-trans {Int} {Int} x x₁ = x₁
≤-trans {B = Int} (s-and-l A≤B) B≤C = s-and-l (≤-trans A≤B B≤C)
≤-trans {B = Int} (s-and-r A≤B) B≤C = s-and-r (≤-trans A≤B B≤C)
≤-trans {Float} {Float} x x₁ = x₁
≤-trans {B = Float} (s-and-l A≤B) B≤C = s-and-l (≤-trans A≤B B≤C)
≤-trans {B = Float} (s-and-r A≤B) B≤C = s-and-r (≤-trans A≤B B≤C)
≤-trans {B = B ⇒ B₁} (s-arr A≤B A≤B₁) (s-arr B≤C B≤C₁) = s-arr (≤-trans B≤C A≤B) (≤-trans A≤B₁ B≤C₁)
≤-trans {B = B ⇒ B₁} (s-arr A≤B A≤B₁) s-top = s-top
≤-trans {B = B ⇒ B₁} (s-arr A≤B A≤B₁) (s-and B≤C B≤C₁) = s-and (≤-trans (s-arr A≤B A≤B₁) B≤C)
(≤-trans (s-arr A≤B A≤B₁) B≤C₁)
≤-trans {B = B ⇒ B₁} (s-and-l A≤B) B≤C = s-and-l (≤-trans A≤B B≤C)
≤-trans {B = B ⇒ B₁} (s-and-r A≤B) B≤C = s-and-r (≤-trans A≤B B≤C)
≤-trans {B = B & B₁} A≤B s-top = s-top
≤-trans {B = B & B₁} A≤B (s-and-l B≤C) = ≤-trans (inv-&-l A≤B) B≤C
≤-trans {B = B & B₁} A≤B (s-and-r B≤C) = ≤-trans (inv-&-r A≤B) B≤C
≤-trans {B = B & B₁} A≤B (s-and B≤C B≤C₁) = s-and (≤-trans A≤B B≤C) (≤-trans A≤B B≤C₁)
≤-trans {B = τ⟦ x₁ ↦ B ⟧} x s-top = s-top
≤-trans {B = τ⟦ x₁ ↦ B ⟧} x (s-and x₂ x₃) = s-and (≤-trans x x₂) (≤-trans x x₃)
≤-trans {B = τ⟦ x₁ ↦ B ⟧} (s-and-l x) (s-rcd s) = s-and-l (≤-trans x (s-rcd s))
≤-trans {B = τ⟦ x₁ ↦ B ⟧} (s-and-r x) (s-rcd s) = s-and-r (≤-trans x (s-rcd s))
≤-trans {B = τ⟦ x₁ ↦ B ⟧} (s-rcd x) (s-rcd s) = s-rcd (≤-trans x s)
infix 4 _⊢_⦂_
infix 4 _⊢r_⦂_
data _⊢_⦂_ : Context → Term → Type → Set
data _⊢r_⦂_ : Context → Record → Type → Set
data _⊢_⦂_ where
⊢n : ∀ {Γ n}
→ Γ ⊢ (lit n) ⦂ Int
⊢m : ∀ {Γ m}
→ Γ ⊢ (flt m) ⦂ Float
⊢` : ∀ {Γ x A}
→ Γ ∋ x ⦂ A
→ Γ ⊢ ` x ⦂ A
⊢ƛ : ∀ {Γ x N A B}
→ Γ , x ⦂ A ⊢ N ⦂ B
→ Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B
⊢· : ∀ {Γ L M A B}
→ Γ ⊢ L ⦂ A ⇒ B
→ Γ ⊢ M ⦂ A
→ Γ ⊢ L · M ⦂ B
⊢& : ∀ {Γ M A B}
→ Γ ⊢ M ⦂ A
→ Γ ⊢ M ⦂ B
→ Γ ⊢ M ⦂ (A & B)
⊢+ : ∀ {Γ}
→ Γ ⊢ + ⦂ (Int ⇒ Int ⇒ Int) & (Float ⇒ Float ⇒ Float)
⊢+i : ∀ {Γ n}
→ Γ ⊢ (+i n) ⦂ Int ⇒ Int
⊢+f : ∀ {Γ m}
→ Γ ⊢ (+f m) ⦂ Float ⇒ Float
⊢rcd : ∀ {Γ rs As}
→ Γ ⊢r rs ⦂ As
→ Γ ⊢ (𝕣 rs) ⦂ As
⊢prj : ∀ {Γ e l A}
→ Γ ⊢ e ⦂ τ⟦ l ↦ A ⟧
→ Γ ⊢ e 𝕡 l ⦂ A
⊢sub : ∀ {Γ M A B}
→ Γ ⊢ M ⦂ A
→ A ≤ B
→ Γ ⊢ M ⦂ B
data _⊢r_⦂_ where
⊢r-nil : ∀ {Γ}
→ Γ ⊢r rnil ⦂ Top
⊢r-one : ∀ {Γ e A l}
→ Γ ⊢ e ⦂ A
→ Γ ⊢r r⟦ l ↦ e ⟧ rnil ⦂ τ⟦ l ↦ A ⟧
⊢r-cons : ∀ {Γ l e rs A As}
→ (⊢e : Γ ⊢ e ⦂ A)
→ Γ ⊢r rs ⦂ As
→ Γ ⊢r r⟦ l ↦ e ⟧ rs ⦂ (τ⟦ l ↦ A ⟧ & As)
infix 9 _[_:=_]
_[_:=_] : Term → Id → Term → Term
_[_:=_]r : Record → Id → Term → Record
(` x) [ y := V ] with x ≟ y
... | yes _ = V
... | no _ = ` x
(ƛ x ⇒ e) [ y := V ] with x ≟ y
... | yes _ = ƛ x ⇒ e
... | no _ = ƛ x ⇒ e [ y := V ]
(e₁ · e₂) [ y := V ] = e₁ [ y := V ] · e₂ [ y := V ]
(lit n) [ y := V ] = lit n
(flt m) [ y := V ] = flt m
+ [ x := x₁ ] = +
+i n [ x := x₁ ] = +i n
+f m [ x := x₁ ] = +f m
(𝕣 rs) [ y := V ] = 𝕣 (rs [ y := V ]r)
(e 𝕡 l) [ y := V ] = (e [ y := V ]) 𝕡 l
rnil [ y := V ]r = rnil
(r⟦ l ↦ e ⟧ rs) [ y := V ]r = r⟦ l ↦ (e [ y := V ]) ⟧ (rs [ y := V ]r)
select : Record → Label → Maybe Term
select rnil l = nothing
select (r⟦ l₁ ↦ e ⟧ rs) l₂ with l₁ ≟n l₂
... | yes p = just e
... | no ¬p = select rs l₂
data Value : Term → Set
data ValueR : Record → Set
data ValueR where
VR-0 : ValueR rnil
VR-S : ∀ {v rs l}
→ Value v
→ ValueR rs
→ ValueR (r⟦ l ↦ v ⟧ rs)
data Value where
V-n : ∀ {n}
→ Value (lit n)
V-m : ∀ {m}
→ Value (flt m)
V-ƛ : ∀ {x e}
→ Value (ƛ x ⇒ e)
V-+ :
Value (+)
V-+i : ∀ {n}
→ Value (+i n)
V-+f : ∀ {m}
→ Value (+f m)
V-r : ∀ {rs}
→ ValueR rs
→ Value (𝕣 rs)
infix 4 _—→_
data _—→_ : Term → Term → Set
data _→r_ : Record → Record → Set
data _→r_ where
rstep-1 : ∀ {e e' l rs}
→ e —→ e'
→ (r⟦ l ↦ e ⟧ rs) →r (r⟦ l ↦ e' ⟧ rs)
rstep-2 : ∀ {v rs rs' l}
→ Value v
→ rs →r rs'
→ (r⟦ l ↦ v ⟧ rs) →r (r⟦ l ↦ v ⟧ rs')
data _—→_ where
ξ-·₁ : ∀ {L L′ M}
→ L —→ L′
→ L · M —→ L′ · M
ξ-·₂ : ∀ {V M M′}
→ Value V
→ M —→ M′
→ V · M —→ V · M′
ξ-prj : ∀ {M M' l}
→ M —→ M'
→ (M 𝕡 l) —→ (M' 𝕡 l)
ξ-rcd : ∀ {rs rs'}
→ rs →r rs'
→ (𝕣 rs) —→ (𝕣 rs')
β-ƛ : ∀ {x N V}
→ Value V
→ (ƛ x ⇒ N) · V —→ N [ x := V ]
β-+-i : ∀ {n}
→ + · (lit n) —→ +i n
β-+-f : ∀ {m}
→ + · (flt m) —→ +f m
β-+i : ∀ {n₁ n₂}
→ (+i n₁) · (lit n₂) —→ (lit (n₁ ++n n₂))
β-+f : ∀ {m₁ m₂}
→ (+f m₁) · (flt m₂) —→ (flt (m₁ ++f m₂))
β-prj : ∀ {rs l e}
→ ValueR rs
→ select rs l ≡ just e
→ (𝕣 rs) 𝕡 l —→ e
data Progress (M : Term) : Set where
step : ∀ {N}
→ M —→ N
→ Progress M
done :
Value M
→ Progress M
elim-int : ∀ {Γ n A B C}
→ Γ ⊢ lit n ⦂ A
→ A ≤ B ⇒ C
→ ⊥
elim-int (⊢& ⊢e ⊢e₁) (s-and-l A≤B) = elim-int ⊢e A≤B
elim-int (⊢& ⊢e ⊢e₁) (s-and-r A≤B) = elim-int ⊢e₁ A≤B
elim-int (⊢sub ⊢e x) A≤B = elim-int ⊢e (≤-trans x A≤B)
elim-int' : ∀ {Γ n A B}
→ Γ ⊢ lit n ⦂ A ⇒ B
→ ⊥
elim-int' (⊢sub ⊢e x) = elim-int ⊢e x
elim-flt : ∀ {Γ n A B C}
→ Γ ⊢ flt n ⦂ A
→ A ≤ B ⇒ C
→ ⊥
elim-flt (⊢& ⊢e ⊢e₁) (s-and-l A≤B) = elim-flt ⊢e A≤B
elim-flt (⊢& ⊢e ⊢e₁) (s-and-r A≤B) = elim-flt ⊢e₁ A≤B
elim-flt (⊢sub ⊢e x) A≤B = elim-flt ⊢e (≤-trans x A≤B)
elim-flt' : ∀ {Γ n A B}
→ Γ ⊢ flt n ⦂ A ⇒ B
→ ⊥
elim-flt' (⊢sub ⊢e x) = elim-flt ⊢e x
elim-int-rcd : ∀ {Γ rs A}
→ Γ ⊢r rs ⦂ A
→ A ≤ Int
→ ⊥
elim-int-rcd (⊢r-cons x ⊢r) (s-and-r A≤Int) = elim-int-rcd ⊢r A≤Int
elim-flt-rcd : ∀ {Γ rs A}
→ Γ ⊢r rs ⦂ A
→ A ≤ Float
→ ⊥
elim-flt-rcd (⊢r-cons x ⊢r) (s-and-r A≤Flo) = elim-flt-rcd ⊢r A≤Flo
canonical-int : ∀ {Γ M A}
→ Γ ⊢ M ⦂ A
→ A ≤ Int
→ Value M
→ ∃[ n ](M ≡ lit n)
canonical-int {A = Int} (⊢n {n = n}) x₁ x₂ = ⟨ n , refl ⟩
canonical-int {A = Int} (⊢sub x x₃) x₁ x₂ = canonical-int x x₃ x₂
canonical-int (⊢& ⊢M ⊢M₁) (s-and-l A≤Int) VM = canonical-int ⊢M A≤Int VM
canonical-int (⊢sub ⊢M x) (s-and-l A≤Int) VM = canonical-int ⊢M (≤-trans (inv-&-l x) A≤Int) VM
canonical-int (⊢& ⊢M ⊢M₁) (s-and-r A≤Int) VM = canonical-int ⊢M₁ A≤Int VM
canonical-int (⊢sub ⊢M x) (s-and-r A≤Int) VM = canonical-int ⊢M (≤-trans (inv-&-r x) A≤Int) VM
canonical-int (⊢rcd ⊢r) (s-and-l A≤Int) VM = ⊥-elim (elim-int-rcd ⊢r (s-and-l A≤Int))
canonical-int (⊢rcd ⊢r) (s-and-r A≤Int) VM = ⊥-elim (elim-int-rcd ⊢r (s-and-r A≤Int))
canonical-flt : ∀ {Γ M A}
→ Γ ⊢ M ⦂ A
→ A ≤ Float
→ Value M
→ ∃[ m ](M ≡ flt m)
canonical-flt (⊢m {m = m}) s-flt VM = ⟨ m , refl ⟩
canonical-flt (⊢sub ⊢M x) s-flt VM = canonical-flt ⊢M x VM
canonical-flt (⊢& ⊢M ⊢M₁) (s-and-l A≤F) VM = canonical-flt ⊢M A≤F VM
canonical-flt (⊢sub ⊢M x) (s-and-l A≤F) VM = canonical-flt ⊢M (≤-trans (inv-&-l x) A≤F) VM
canonical-flt (⊢& ⊢M ⊢M₁) (s-and-r A≤F) VM = canonical-flt ⊢M₁ A≤F VM
canonical-flt (⊢sub ⊢M x) (s-and-r A≤F) VM = canonical-flt ⊢M (≤-trans (inv-&-r x) A≤F) VM
canonical-flt (⊢rcd x₁) (s-and-l x₂) x = ⊥-elim (elim-flt-rcd x₁ (s-and-l x₂))
canonical-flt (⊢rcd x₁) (s-and-r x₂) x = ⊥-elim (elim-flt-rcd x₁ (s-and-r x₂))
inv-arr-l : ∀ {A B C D}
→ A ⇒ B ≤ C ⇒ D
→ C ≤ A
inv-arr-r : ∀ {A B C D}
→ A ⇒ B ≤ C ⇒ D
→ B ≤ D
inv-arr-l (s-arr AB≤CD AB≤CD₁) = AB≤CD
inv-arr-r (s-arr AB≤CD AB≤CD₁) = AB≤CD₁
progress-+' : ∀ {M T A B}
→ ∅ ⊢ + ⦂ T
→ T ≤ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+ · M)
progress-+' (⊢& ⊢T ⊢T₁) (s-and-l T≤AB) ⊢M VM = progress-+' ⊢T T≤AB ⊢M VM
progress-+' (⊢& ⊢T ⊢T₁) (s-and-r T≤AB) ⊢M VM = progress-+' ⊢T₁ T≤AB ⊢M VM
progress-+' ⊢+ (s-and-l (s-arr T≤AB T≤AB₁)) ⊢M VM with canonical-int ⊢M T≤AB VM
... | ⟨ n , eq ⟩ rewrite eq = step β-+-i
progress-+' ⊢+ (s-and-r (s-arr T≤AB T≤AB₁)) ⊢M VM with canonical-flt ⊢M T≤AB VM
... | ⟨ m , eq ⟩ rewrite eq = step β-+-f
progress-+' (⊢sub ⊢T x) AB≤T ⊢M VM = progress-+' ⊢T (≤-trans x AB≤T) ⊢M VM
progress-+ : ∀ {M A B}
→ ∅ ⊢ + ⦂ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+ · M)
progress-+ (⊢sub ⊢N x) ⊢M VM = progress-+' ⊢N x ⊢M VM
progress-+i' : ∀ {T M A B n}
→ ∅ ⊢ +i n ⦂ T
→ T ≤ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+i n · M)
progress-+i' (⊢& ⊢T ⊢T₁) (s-and-l T≤A⇒B) ⊢M VM = progress-+i' ⊢T T≤A⇒B ⊢M VM
progress-+i' (⊢& ⊢T ⊢T₁) (s-and-r T≤A⇒B) ⊢M VM = progress-+i' ⊢T₁ T≤A⇒B ⊢M VM
progress-+i' ⊢+i (s-arr T≤A⇒B T≤A⇒B₁) ⊢M VM with canonical-int ⊢M T≤A⇒B VM
... | ⟨ n , eq ⟩ rewrite eq = step β-+i
progress-+i' (⊢sub ⊢T x) T≤A⇒B ⊢M VM = progress-+i' ⊢T (≤-trans x T≤A⇒B) ⊢M VM
progress-+i : ∀ {M A B n}
→ ∅ ⊢ +i n ⦂ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+i n · M)
progress-+i ⊢+i ⊢M VM with canonical-int ⊢M s-int VM
... | ⟨ n , eq ⟩ rewrite eq = step β-+i
progress-+i (⊢sub ⊢N x) ⊢M VM = progress-+i' ⊢N x ⊢M VM
progress-+f' : ∀ {T M A B n}
→ ∅ ⊢ +f n ⦂ T
→ T ≤ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+f n · M)
progress-+f' (⊢& ⊢T ⊢T₁) (s-and-l T≤A⇒B) ⊢M VM = progress-+f' ⊢T T≤A⇒B ⊢M VM
progress-+f' (⊢& ⊢T ⊢T₁) (s-and-r T≤A⇒B) ⊢M VM = progress-+f' ⊢T₁ T≤A⇒B ⊢M VM
progress-+f' ⊢+f (s-arr T≤A⇒B T≤A⇒B₁) ⊢M VM with canonical-flt ⊢M T≤A⇒B VM
... | ⟨ n , eq ⟩ rewrite eq = step β-+f
progress-+f' (⊢sub ⊢T x) T≤A⇒B ⊢M VM = progress-+f' ⊢T (≤-trans x T≤A⇒B) ⊢M VM
progress-+f : ∀ {M A B n}
→ ∅ ⊢ +f n ⦂ A ⇒ B
→ ∅ ⊢ M ⦂ A
→ Value M
→ Progress (+f n · M)
progress-+f ⊢+f ⊢M VM with canonical-flt ⊢M s-flt VM
... | ⟨ n , eq ⟩ rewrite eq = step β-+f
progress-+f (⊢sub ⊢N x) ⊢M VM = progress-+f' ⊢N x ⊢M VM
elim-rcd-arr-r : ∀ {Γ rs A B C}
→ Γ ⊢r rs ⦂ C
→ C ≤ A ⇒ B
→ ⊥
elim-rcd-arr-r (⊢r-cons x ⊢r) (s-and-r sub) = elim-rcd-arr-r ⊢r sub
elim-rcd-arr : ∀ {Γ rs A B C}
→ Γ ⊢ 𝕣 rs ⦂ C
→ C ≤ A ⇒ B
→ ⊥
elim-rcd-arr (⊢& ⊢r ⊢r₁) (s-and-l sub) = elim-rcd-arr ⊢r sub
elim-rcd-arr (⊢& ⊢r ⊢r₁) (s-and-r sub) = elim-rcd-arr ⊢r₁ sub
elim-rcd-arr (⊢rcd x) sub = elim-rcd-arr-r x sub
elim-rcd-arr (⊢sub ⊢r x) sub = elim-rcd-arr ⊢r (≤-trans x sub)
infix 3 _∉_
data _∉_ : Label → Record → Set where
notin-empty : ∀ {l}
→ l ∉ rnil
notin-cons : ∀ {l₁ l₂ rs e}
→ l₁ ≢ l₂
→ l₁ ∉ rs
→ l₁ ∉ r⟦ l₂ ↦ e ⟧ rs
data WFE : Term → Set
data WFR : Record → Set
data WFE where
wfe-n : ∀ {n} → WFE (lit n)
wfe-m : ∀ {m} → WFE (flt m)
wfe-+i : ∀ {m} → WFE (+i m)
wfe-+f : ∀ {n} → WFE (+f n)
wfe-+ : WFE +
wfe-var : ∀ {x} → WFE (` x)
wfe-lam : ∀ {x e} → WFE e → WFE (ƛ x ⇒ e)
wfe-app : ∀ {e₁ e₂} → WFE e₁ → WFE e₂ → WFE (e₁ · e₂)
wfe-rcd : ∀ {rs} → WFR rs → WFE (𝕣 rs)
wfe-prj : ∀ {e l} → WFE e → WFE (e 𝕡 l)
data WFR where
wfr-nil : WFR rnil
wfr-cons : ∀ {e l rs}
→ WFE e
→ WFR rs
→ l ∉ rs
→ WFR (r⟦ l ↦ e ⟧ rs)
false-case : ∀ {l rs e}
→ l ∉ rs
→ select rs l ≡ just e
→ ⊥
false-case {l = l} (notin-cons {l₂ = l₂} x notin) eq with l₂ ≟n l
... | yes p = x (sym p)
... | no ¬p = false-case notin eq
select-v-r-wf : ∀ {rs A l A₁}
→ WFR rs
→ ValueR rs
→ ∅ ⊢r rs ⦂ A₁
→ A₁ ≤ τ⟦ l ↦ A ⟧
→ ∃[ e ](select rs l ≡ just e × (∅ ⊢ e ⦂ A))
select-v-r-wf {l = l} wfr vr (⊢r-one {e = e} x) (s-rcd s) with l ≟n l
... | yes p = ⟨ e , ⟨ refl , ⊢sub x s ⟩ ⟩
... | no ¬p = ⊥-elim (¬p refl)
select-v-r-wf {l = l} wfr (VR-S x vr) (⊢r-cons {e = e} ⊢e ⊢r) (s-and-l (s-rcd s)) with l ≟n l
... | yes p = ⟨ e , ⟨ refl , ⊢sub ⊢e s ⟩ ⟩
... | no ¬p = ⊥-elim (¬p refl)
select-v-r-wf {l = l} (wfr-cons x wfr x₁) (VR-S {v = v} x₂ vr) (⊢r-cons {l = l'} ⊢e ⊢r) (s-and-r s) with select-v-r-wf wfr vr ⊢r s
select-v-r-wf {l = l} (wfr-cons x wfr x₁) (VR-S {v = v} x₂ vr) (⊢r-cons {l = l'} ⊢e ⊢r) (s-and-r s) | ⟨ e , ⟨ eq , ⊢e' ⟩ ⟩ with l' ≟n l
... | yes p rewrite p = ⊥-elim (false-case x₁ eq)
... | no ¬p = ⟨ e , ⟨ eq , ⊢e' ⟩ ⟩
select-value' : ∀ {rs l A A₁}
→ WFR rs
→ ValueR rs
→ ∅ ⊢ 𝕣 rs ⦂ A₁
→ A₁ ≤ τ⟦ l ↦ A ⟧
→ ∃[ e ](select rs l ≡ just e × (∅ ⊢ e ⦂ A))
select-value' wfr vr (⊢& ⊢e ⊢e₁) (s-and-l s) = select-value' wfr vr ⊢e s
select-value' wfr vr (⊢& ⊢e ⊢e₁) (s-and-r s) = select-value' wfr vr ⊢e₁ s
select-value' wfr vr (⊢rcd x) s = select-v-r-wf wfr vr x s
select-value' wfr vr (⊢sub ⊢e x) s = select-value' wfr vr ⊢e (≤-trans x s)
select-value : ∀ {rs l A}
→ WFR rs
→ ValueR rs
→ ∅ ⊢ 𝕣 rs ⦂ τ⟦ l ↦ A ⟧
→ ∃[ e ](select rs l ≡ just e × (∅ ⊢ e ⦂ A))
select-value {l = l} wfr vr (⊢rcd (⊢r-one {e = e} {l = l} x)) with l ≟n l
... | yes p = ⟨ e , ⟨ refl , x ⟩ ⟩
... | no ¬p = ⊥-elim (¬p refl)
select-value wfr vr (⊢sub ⊢e x) = select-value' wfr vr ⊢e x
inv-n-rcd : ∀ {n l A B}
→ ∅ ⊢ lit n ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-n-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-n-rcd ⊢e s
inv-n-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-n-rcd ⊢e₁ s
inv-n-rcd (⊢sub ⊢e x) s = inv-n-rcd ⊢e (≤-trans x s)
inv-m-rcd : ∀ {m l A B}
→ ∅ ⊢ flt m ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-m-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-m-rcd ⊢e s
inv-m-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-m-rcd ⊢e₁ s
inv-m-rcd (⊢sub ⊢e x) s = inv-m-rcd ⊢e (≤-trans x s)
inv-lam-rcd : ∀ {x e l A B}
→ ∅ ⊢ ƛ x ⇒ e ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-lam-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-lam-rcd ⊢e s
inv-lam-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-lam-rcd ⊢e₁ s
inv-lam-rcd (⊢sub ⊢e x) s = inv-lam-rcd ⊢e (≤-trans x s)
inv-+-rcd : ∀ {l A B}
→ ∅ ⊢ + ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-+-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-+-rcd ⊢e s
inv-+-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-+-rcd ⊢e₁ s
inv-+-rcd ⊢+ (s-and-l ())
inv-+-rcd ⊢+ (s-and-r ())
inv-+-rcd (⊢sub ⊢e x) s = inv-+-rcd ⊢e (≤-trans x s)
inv-+i-rcd : ∀ {l n A B}
→ ∅ ⊢ +i n ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-+i-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-+i-rcd ⊢e s
inv-+i-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-+i-rcd ⊢e₁ s
inv-+i-rcd (⊢sub ⊢e x) s = inv-+i-rcd ⊢e (≤-trans x s)
inv-+f-rcd : ∀ {l n A B}
→ ∅ ⊢ +f n ⦂ A
→ A ≤ τ⟦ l ↦ B ⟧
→ ⊥
inv-+f-rcd (⊢& ⊢e ⊢e₁) (s-and-l s) = inv-+f-rcd ⊢e s
inv-+f-rcd (⊢& ⊢e ⊢e₁) (s-and-r s) = inv-+f-rcd ⊢e₁ s
inv-+f-rcd (⊢sub ⊢e x) s = inv-+f-rcd ⊢e (≤-trans x s)
wfr-inv : ∀ {rs}
→ WFE (𝕣 rs)
→ WFR rs
wfr-inv (wfe-rcd x) = x
progress : ∀ {e A}
→ WFE e
→ ∅ ⊢ e ⦂ A
→ Progress e
progress-r : ∀ {rs A}
→ WFR rs
→ ∅ ⊢r rs ⦂ A
→ Progress (𝕣 rs)
progress-r wfe ⊢r-nil = done (V-r VR-0)
progress-r (wfr-cons wfe wfr l∉) (⊢r-one ⊢e) with progress wfe ⊢e
... | step x = step (ξ-rcd (rstep-1 x))
... | done x = done (V-r (VR-S x VR-0))
progress-r (wfr-cons wfe wfr l∉) (⊢r-cons ⊢e ⊢r ) with progress wfe ⊢e | progress-r wfr ⊢r
... | step x | p2 = step (ξ-rcd (rstep-1 x))
... | done x | step (ξ-rcd x₁) = step (ξ-rcd (rstep-2 x x₁))
... | done x | done (V-r x₁) = done (V-r (VR-S x x₁))
progress wfe ⊢n = done V-n
progress wfe ⊢m = done V-m
progress wfe (⊢ƛ ⊢e) = done V-ƛ
progress (wfe-app wfe1 wfe2) (⊢· ⊢e₁ ⊢e₂) with progress wfe1 ⊢e₁ | progress wfe2 ⊢e₂
... | step s₁ | _ = step (ξ-·₁ s₁)
... | done v₁ | step s₂ = step (ξ-·₂ v₁ s₂)
... | done V-n | done v₂ = ⊥-elim (elim-int' ⊢e₁)
... | done V-m | done v₂ = ⊥-elim (elim-flt' ⊢e₁)
... | done V-ƛ | done v₂ = step (β-ƛ v₂)
... | done V-+ | done v₂ = progress-+ ⊢e₁ ⊢e₂ v₂
... | done V-+i | done v₂ = progress-+i ⊢e₁ ⊢e₂ v₂
... | done V-+f | done v₂ = progress-+f ⊢e₁ ⊢e₂ v₂
... | done (V-r vr) | done v₂ = ⊥-elim (elim-rcd-arr ⊢e₁ s-refl)
progress wfe (⊢& ⊢e ⊢e₁) = progress wfe ⊢e
progress wfe ⊢+ = done V-+
progress wfe ⊢+i = done V-+i
progress wfe ⊢+f = done V-+f
progress wfe (⊢sub ⊢e x) = progress wfe ⊢e
progress (wfe-rcd x) (⊢rcd ⊢r) = progress-r x ⊢r
progress (wfe-prj wfe) (⊢prj ⊢e) with progress wfe ⊢e
... | step x = step (ξ-prj x)
... | done V-n = ⊥-elim (inv-n-rcd ⊢e s-refl)
... | done V-m = ⊥-elim (inv-m-rcd ⊢e s-refl)
... | done V-ƛ = ⊥-elim (inv-lam-rcd ⊢e s-refl)
... | done V-+ = ⊥-elim (inv-+-rcd ⊢e s-refl)
... | done V-+i = ⊥-elim (inv-+i-rcd ⊢e s-refl)
... | done V-+f = ⊥-elim (inv-+f-rcd ⊢e s-refl)
... | done (V-r x) = let ⟨ e , ⟨ eq , ⊢e ⟩ ⟩ = select-value (wfr-inv wfe) x ⊢e
in step (β-prj x eq)
ext : ∀ {Γ Δ}
→ (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
→ (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z = Z
ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x)
rename : ∀ {Γ Δ}
→ (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
→ (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename-r : ∀ {Γ Δ}
→ (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
→ (∀ {M A} → Γ ⊢r M ⦂ A → Δ ⊢r M ⦂ A)
rename-r ρ ⊢r-nil = ⊢r-nil
rename-r ρ (⊢r-one x) = ⊢r-one (rename ρ x)
rename-r ρ (⊢r-cons ⊢e ⊢r) = ⊢r-cons (rename ρ ⊢e) (rename-r ρ ⊢r)
rename ρ ⊢n = ⊢n
rename ρ ⊢m = ⊢m
rename ρ (⊢` ∋w) = ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N) = ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢· ⊢L ⊢M) = ⊢· (rename ρ ⊢L) (rename ρ ⊢M)
rename ρ (⊢& ⊢L ⊢M) = ⊢& (rename ρ ⊢L) (rename ρ ⊢M)
rename ρ (⊢sub ⊢L s) = ⊢sub (rename ρ ⊢L) s
rename ρ ⊢+ = ⊢+
rename ρ ⊢+i = ⊢+i
rename ρ ⊢+f = ⊢+f
rename ρ (⊢rcd ⊢r) = ⊢rcd (rename-r ρ ⊢r)
rename ρ (⊢prj ⊢e) = ⊢prj (rename ρ ⊢e)
weaken : ∀ {Γ M A}
→ ∅ ⊢ M ⦂ A
→ Γ ⊢ M ⦂ A
weaken {Γ} ⊢M = rename ρ ⊢M
where
ρ : ∀ {z C}
→ ∅ ∋ z ⦂ C
→ Γ ∋ z ⦂ C
ρ ()
drop : ∀ {Γ x M A B C}
→ Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C
→ Γ , x ⦂ B ⊢ M ⦂ C
drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
where
ρ : ∀ {z C}
→ Γ , x ⦂ A , x ⦂ B ∋ z ⦂ C
→ Γ , x ⦂ B ∋ z ⦂ C
ρ Z = Z
ρ (S x≢x Z) = ⊥-elim (x≢x refl)
ρ (S z≢x (S _ ∋z)) = S z≢x ∋z
swap : ∀ {Γ x y M A B C}
→ x ≢ y
→ Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C
→ Γ , x ⦂ A , y ⦂ B ⊢ M ⦂ C
swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
where
ρ : ∀ {z C}
→ Γ , y ⦂ B , x ⦂ A ∋ z ⦂ C
→ Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
ρ Z = S x≢y Z
ρ (S z≢x Z) = Z
ρ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z)
subst : ∀ {Γ x N V A B}
→ ∅ ⊢ V ⦂ A
→ Γ , x ⦂ A ⊢ N ⦂ B
→ Γ ⊢ N [ x := V ] ⦂ B
subst-r : ∀ {Γ x N V A B}
→ ∅ ⊢ V ⦂ A
→ Γ , x ⦂ A ⊢r N ⦂ B
→ Γ ⊢r N [ x := V ]r ⦂ B
subst-r {x = y} ⊢V ⊢r-nil = ⊢r-nil
subst-r {x = y} ⊢V (⊢r-one ⊢e) = ⊢r-one (subst ⊢V ⊢e)
subst-r {x = y} ⊢V (⊢r-cons ⊢e ⊢r) = ⊢r-cons (subst ⊢V ⊢e) (subst-r ⊢V ⊢r)
subst {x = y} ⊢V ⊢n = ⊢n
subst {x = y} ⊢V ⊢m = ⊢m
subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y
... | yes _ = weaken ⊢V
... | no x≢y = ⊥-elim (x≢y refl)
subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y
... | yes refl = ⊥-elim (x≢y refl)
... | no _ = ⊢` ∋x
subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
... | yes refl = ⊢ƛ (drop ⊢N)
... | no x≢y = ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
subst ⊢V (⊢· ⊢L ⊢M) = ⊢· (subst ⊢V ⊢L) (subst ⊢V ⊢M)
subst ⊢V (⊢& ⊢L ⊢M) = ⊢& (subst ⊢V ⊢L) (subst ⊢V ⊢M)
subst ⊢V (⊢sub ⊢L s) = ⊢sub (subst ⊢V ⊢L) s
subst ⊢V ⊢+ = ⊢+
subst ⊢V ⊢+i = ⊢+i
subst ⊢V ⊢+f = ⊢+f
subst ⊢V (⊢rcd ⊢r) = ⊢rcd (subst-r ⊢V ⊢r)
subst ⊢V (⊢prj ⊢e) = ⊢prj (subst ⊢V ⊢e)
inv-lam' : ∀ {Γ x e A B T}
→ Γ ⊢ ƛ x ⇒ e ⦂ T
→ T ≤ A ⇒ B
→ ∃[ A' ]( ∃[ B' ] ((Γ , x ⦂ A' ⊢ e ⦂ B') × (A ≤ A') × (B' ≤ B)))
inv-lam' (⊢ƛ {A = A} {B} ⊢e) (s-arr T≤AB T≤AB₁) = ⟨ A , ⟨ B , ⟨ ⊢e , ⟨ T≤AB , T≤AB₁ ⟩ ⟩ ⟩ ⟩
inv-lam' (⊢sub ⊢e x) (s-arr T≤AB T≤AB₁) = inv-lam' ⊢e (≤-trans x (s-arr T≤AB T≤AB₁))
inv-lam' (⊢& ⊢e ⊢e₁) (s-and-l T≤AB) = inv-lam' ⊢e T≤AB
inv-lam' (⊢sub ⊢e x) (s-and-l T≤AB) = inv-lam' ⊢e (≤-trans (inv-&-l x) T≤AB)
inv-lam' (⊢& ⊢e ⊢e₁) (s-and-r T≤AB) = inv-lam' ⊢e₁ T≤AB
inv-lam' (⊢sub ⊢e x) (s-and-r T≤AB) = inv-lam' ⊢e (≤-trans (inv-&-r x) T≤AB)
inv-lam : ∀ {Γ x e A B}
→ Γ ⊢ ƛ x ⇒ e ⦂ A ⇒ B
→ ∃[ A' ]( ∃[ B' ] ((Γ , x ⦂ A' ⊢ e ⦂ B') × (A ≤ A') × (B' ≤ B)))
inv-lam {A = A} {B = B} (⊢ƛ ⊢e) = ⟨ A , ⟨ B , ⟨ ⊢e , ⟨ s-refl , s-refl ⟩ ⟩ ⟩ ⟩
inv-lam {A = A} {B = B} (⊢sub ⊢e x) = inv-lam' ⊢e x
inv-int : ∀ {Γ n A}
→ Γ ⊢ lit n ⦂ A
→ Int ≤ A
inv-int ⊢n = s-refl
inv-int (⊢& ⊢e ⊢e₁) = s-and (inv-int ⊢e) (inv-int ⊢e₁)
inv-int (⊢sub ⊢e x) = ≤-trans (inv-int ⊢e) x
inv-flt : ∀ {Γ m A}
→ Γ ⊢ flt m ⦂ A
→ Float ≤ A
inv-flt ⊢m = s-flt
inv-flt (⊢& ⊢M ⊢M₁) = s-and (inv-flt ⊢M) (inv-flt ⊢M₁)
inv-flt (⊢sub ⊢M x) = ≤-trans (inv-flt ⊢M) x
¬Int≤Float : Int ≤ Float → ⊥
¬Int≤Float ()
¬Float≤Int : Float ≤ Int → ⊥
¬Float≤Int ()
inv-+-i+' : ∀ {Γ T A B}
→ Γ ⊢ + ⦂ T
→ T ≤ A ⇒ B
→ Int ≤ A
→ Int ⇒ Int ≤ B
inv-+-i+' (⊢& ⊢T ⊢T₁) (s-and-l T≤AB) Int≤A = inv-+-i+' ⊢T T≤AB Int≤A
inv-+-i+' (⊢& ⊢T ⊢T₁) (s-and-r T≤AB) Int≤A = inv-+-i+' ⊢T₁ T≤AB Int≤A
inv-+-i+' ⊢+ (s-and-l (s-arr T≤AB T≤AB₁)) Int≤A = T≤AB₁
inv-+-i+' ⊢+ (s-and-r (s-arr T≤AB T≤AB₁)) Int≤A = ⊥-elim (¬Int≤Float (≤-trans Int≤A T≤AB))
inv-+-i+' (⊢sub ⊢T x) T≤AB Int≤A = inv-+-i+' ⊢T (≤-trans x T≤AB) Int≤A
inv-+-i+ : ∀ {Γ A B}
→ Γ ⊢ + ⦂ A ⇒ B
→ Int ≤ A
→ Int ⇒ Int ≤ B
inv-+-i+ (⊢sub ⊢M x) Int≤A = inv-+-i+' ⊢M x Int≤A
inv-+-f+' : ∀ {Γ T A B}
→ Γ ⊢ + ⦂ T
→ T ≤ A ⇒ B
→ Float ≤ A
→ Float ⇒ Float ≤ B
inv-+-f+' (⊢& ⊢T ⊢T₁) (s-and-l T≤AB) Int≤A = inv-+-f+' ⊢T T≤AB Int≤A
inv-+-f+' (⊢& ⊢T ⊢T₁) (s-and-r T≤AB) Int≤A = inv-+-f+' ⊢T₁ T≤AB Int≤A
inv-+-f+' ⊢+ (s-and-l (s-arr T≤AB T≤AB₁)) Int≤A = ⊥-elim (¬Float≤Int (≤-trans Int≤A T≤AB))
inv-+-f+' ⊢+ (s-and-r (s-arr T≤AB T≤AB₁)) Int≤A = T≤AB₁
inv-+-f+' (⊢sub ⊢T x) T≤AB Int≤A = inv-+-f+' ⊢T (≤-trans x T≤AB) Int≤A
inv-+-f+ : ∀ {Γ A B}
→ Γ ⊢ + ⦂ A ⇒ B
→ Float ≤ A
→ Float ⇒ Float ≤ B
inv-+-f+ (⊢sub ⊢M x) Int≤A = inv-+-f+' ⊢M x Int≤A
inv-+i' : ∀ {n A B T}
→ ∅ ⊢ +i n ⦂ T
→ T ≤ A ⇒ B
→ Int ≤ B
inv-+i' (⊢& ⊢M ⊢M₁) (s-and-l T≤AB) = inv-+i' ⊢M T≤AB
inv-+i' (⊢& ⊢M ⊢M₁) (s-and-r T≤AB) = inv-+i' ⊢M₁ T≤AB
inv-+i' ⊢+i (s-arr T≤AB T≤AB₁) = T≤AB₁
inv-+i' (⊢sub ⊢M x) T≤AB = inv-+i' ⊢M (≤-trans x T≤AB)
inv-+i : ∀ {n A B}
→ ∅ ⊢ +i n ⦂ A ⇒ B
→ Int ≤ B
inv-+i ⊢+i = s-int
inv-+i (⊢sub ⊢e x) = inv-+i' ⊢e x
inv-+f' : ∀ {m A B T}
→ ∅ ⊢ +f m ⦂ T
→ T ≤ A ⇒ B
→ Float ≤ B
inv-+f' (⊢& ⊢M ⊢M₁) (s-and-l T≤AB) = inv-+f' ⊢M T≤AB
inv-+f' (⊢& ⊢M ⊢M₁) (s-and-r T≤AB) = inv-+f' ⊢M₁ T≤AB
inv-+f' ⊢+f (s-arr T≤AB T≤AB₁) = T≤AB₁
inv-+f' (⊢sub ⊢M x) T≤AB = inv-+f' ⊢M (≤-trans x T≤AB)
inv-+f : ∀ {m A B}
→ ∅ ⊢ +f m ⦂ A ⇒ B
→ Float ≤ B
inv-+f ⊢+f = s-flt
inv-+f (⊢sub ⊢M x) = inv-+f' ⊢M x
rw-case : ∀ {e N A}
→ just e ≡ just N
→ ∅ ⊢ e ⦂ A
→ ∅ ⊢ N ⦂ A
rw-case refl ⊢e = ⊢e
preserve : ∀ {M N A}
→ WFE M
→ ∅ ⊢ M ⦂ A
→ M —→ N
→ ∅ ⊢ N ⦂ A
preserve-r : ∀ {rs rs' A}
→ WFR rs
→ ∅ ⊢r rs ⦂ A
→ rs →r rs'
→ ∅ ⊢r rs' ⦂ A
preserve-r (wfr-cons x₂ wfr x₃) (⊢r-one x) (rstep-1 x₁) = ⊢r-one (preserve x₂ x x₁)
preserve-r (wfr-cons x₁ wfr x₂) (⊢r-cons ⊢e ⊢r) (rstep-1 x) = ⊢r-cons (preserve x₁ ⊢e x) ⊢r
preserve-r (wfr-cons x₁ wfr x₂) (⊢r-cons ⊢e ⊢r) (rstep-2 x st) = ⊢r-cons ⊢e (preserve-r wfr ⊢r st)
preserve (wfe-app wfe wfe₁) (⊢· ⊢e ⊢e₁) (ξ-·₁ M→N) = ⊢· (preserve wfe ⊢e M→N) ⊢e₁
preserve (wfe-app wfe wfe₁) (⊢· ⊢e ⊢e₁) (ξ-·₂ x M→N) = ⊢· ⊢e (preserve wfe₁ ⊢e₁ M→N)
preserve wfe (⊢· ⊢e ⊢e₁) (β-ƛ x) with inv-lam ⊢e
... | ⟨ A' , ⟨ B' , ⟨ ⊢e' , ⟨ A≤A' , B'≤B ⟩ ⟩ ⟩ ⟩ = subst (⊢sub ⊢e₁ A≤A') (⊢sub ⊢e' B'≤B)
preserve wfe (⊢· ⊢e ⊢e₁) β-+-i = ⊢sub ⊢+i (inv-+-i+ ⊢e (inv-int ⊢e₁))
preserve wfe (⊢· ⊢e ⊢e₁) β-+-f = ⊢sub ⊢+f (inv-+-f+ ⊢e (inv-flt ⊢e₁))
preserve wfe (⊢· ⊢e ⊢e₁) β-+i = ⊢sub ⊢n (inv-+i ⊢e)
preserve wfe (⊢· ⊢e ⊢e₁) β-+f = ⊢sub ⊢m (inv-+f ⊢e)
preserve wfe (⊢& ⊢e ⊢e₁) M→N = ⊢& (preserve wfe ⊢e M→N) (preserve wfe ⊢e₁ M→N)
preserve wfe (⊢sub ⊢e x) M→N = ⊢sub (preserve wfe ⊢e M→N) x
preserve (wfe-prj wfe) (⊢prj ⊢e) (ξ-prj M→N) = ⊢prj (preserve wfe ⊢e M→N)
preserve (wfe-prj (wfe-rcd wfr)) (⊢prj ⊢e) (β-prj vr eq) with select-value wfr vr ⊢e
preserve (wfe-prj (wfe-rcd wfr)) (⊢prj ⊢e) (β-prj vr eq) | ⟨ e , ⟨ eq' , ⊢e' ⟩ ⟩ rewrite eq' = rw-case eq ⊢e'
preserve (wfe-rcd x) (⊢rcd ⊢r) (ξ-rcd x₁) = ⊢rcd (preserve-r x ⊢r x₁)