Inversion of typing

In this module we prove that presuppositions hold of typing judgments: e.g. if E ∣ Γ ⊢[l] t : A then WfCtx Γ and E ∣ Γ ⊢[l] A. Note that E.Wf does not necessarily hold.

Helper lemmas

theorem InvProof.eqSb_snoc' {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t t' : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} : EqSb E Δ σ σ' Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] t : Expr.subst σ A → E ∣ Δ ⊢[l] t' : Expr.subst σ' A → E ∣ Δ ⊢[l] t ≡ t' : Expr.subst σ A → EqSb E Δ (Expr.snoc σ t) (Expr.snoc σ' t') ((A, l) :: Γ)

theorem InvProof.wfSb_conv_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → WfSb E ((A', l) :: Γ) Expr.bvar ((A, l) :: Γ)

theorem InvProof.tp_conv_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ (A', l) :: Γ ⊢[l'] B

theorem InvProof.tm_conv_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B t : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] t : B → E ∣ (A', l) :: Γ ⊢[l'] t : B

Instantiation

theorem InvProof.tp_inst {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[l'] Expr.subst t.toSb B

theorem InvProof.tm_inst {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t b : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ (A, l) :: Γ ⊢[l'] b : B → E ∣ Γ ⊢[l'] Expr.subst t.toSb b : Expr.subst t.toSb B

theorem InvProof.eqtp_inst {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B B' t t' : Expr χ} {l l' : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] t' : A → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[l'] Expr.subst t.toSb B ≡ Expr.subst t'.toSb B'

theorem InvProof.inv_all {χ : Type u_1} {E : Axioms χ} : (∀ {Γ : Ctx χ} {l : ℕ} {A : Expr χ}, E ∣ Γ ⊢[l] A → WfCtx E Γ) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A B : Expr χ}, E ∣ Γ ⊢[l] A ≡ B → WfCtx E Γ ∧ (E ∣ Γ ⊢[l] A) ∧ (E ∣ Γ ⊢[l] B)) ∧ (∀ {Γ : Ctx χ} {l : ℕ} {A t : Expr χ}, E ∣ Γ ⊢[l] t : A → WfCtx E Γ ∧ (E ∣ Γ ⊢[l] A)) ∧ ∀ {Γ : Ctx χ} {l : ℕ} {A t u : Expr χ}, E ∣ Γ ⊢[l] t ≡ u : A → WfCtx E Γ ∧ (E ∣ Γ ⊢[l] A) ∧ (E ∣ Γ ⊢[l] t : A) ∧ (E ∣ Γ ⊢[l] u : A)

General inversion lemmas

theorem WfCtx.inv_snoc {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : WfCtx E ((A, l) :: Γ) → E ∣ Γ ⊢[l] A

theorem WfTp.wf_ctx {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → WfCtx E Γ

theorem EqTp.wf_left {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ B → E ∣ Γ ⊢[l] A

theorem EqTp.wf_right {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ B → E ∣ Γ ⊢[l] B

theorem EqTp.wf_ctx {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ B → WfCtx E Γ

theorem WfTm.wf_tp {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] A

theorem WfTm.wf_ctx {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → WfCtx E Γ

theorem EqTm.wf_left {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ u : A → E ∣ Γ ⊢[l] t : A

theorem EqTm.wf_right {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ u : A → E ∣ Γ ⊢[l] u : A

theorem EqTm.wf_tp {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ u : A → E ∣ Γ ⊢[l] A

theorem EqTm.wf_ctx {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ u : A → WfCtx E Γ

theorem WfTp.wf_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l l' : ℕ} : E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[l] A

theorem EqTp.wf_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B B' : Expr χ} {l l' : ℕ} : E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[l] A

theorem WfTm.wf_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t : Expr χ} {l l' : ℕ} : E ∣ (A, l) :: Γ ⊢[l'] t : B → E ∣ Γ ⊢[l] A

theorem EqTm.wf_binder {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l l' : ℕ} : E ∣ (A, l) :: Γ ⊢[l'] t ≡ u : B → E ∣ Γ ⊢[l] A

Substitution

theorem WfSb.mk {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ : ℕ → Expr χ} : WfCtx E Δ → WfCtx E Γ → (∀ {i : ℕ} {A : Expr χ} {l : ℕ}, Lookup Γ i A l → E ∣ Δ ⊢[l] σ i : Expr.subst σ A) → WfSb E Δ σ Γ

theorem WfSb.wk {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → WfSb E ((A, l) :: Γ) Expr.wk Γ

theorem WfSb.terminal {χ : Type u_1} {E : Axioms χ} {Δ : Ctx χ} (σ : ℕ → Expr χ) : WfCtx E Δ → WfSb E Δ σ []

theorem WfSb.comp {χ : Type u_1} {E : Axioms χ} {Θ Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : WfSb E Θ σ Δ → WfSb E Δ σ' Γ → WfSb E Θ (Expr.comp σ σ') Γ

theorem WfSb.toSb {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → WfSb E Γ t.toSb ((A, l) :: Γ)

theorem EqSb.mk {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {σ σ' : ℕ → Expr χ} : WfCtx E Δ → WfCtx E Γ → (∀ {i : ℕ} {A : Expr χ} {l : ℕ}, Lookup Γ i A l → (E ∣ Δ ⊢[l] Expr.subst σ A ≡ Expr.subst σ' A) ∧ (E ∣ Δ ⊢[l] σ i ≡ σ' i : Expr.subst σ A)) → EqSb E Δ σ σ' Γ

theorem EqSb.snoc {χ : Type u_1} {E : Axioms χ} {Δ Γ : Ctx χ} {A t t' : Expr χ} {σ σ' : ℕ → Expr χ} {l : ℕ} : EqSb E Δ σ σ' Γ → E ∣ Γ ⊢[l] A → E ∣ Δ ⊢[l] t ≡ t' : Expr.subst σ A → EqSb E Δ (Expr.snoc σ t) (Expr.snoc σ' t') ((A, l) :: Γ)

theorem EqSb.terminal {χ : Type u_1} {E : Axioms χ} {Δ : Ctx χ} (σ σ' : ℕ → Expr χ) : WfCtx E Δ → EqSb E Δ σ σ' []

theorem EqSb.toSb {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t t' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ t' : A → EqSb E Γ t.toSb t'.toSb ((A, l) :: Γ)