Typing rules

In this file we specify typing judgments of the type theory as Prop-valued relations.

def judgment.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.judgment : Category

Equations

• Lean.Parser.Category.judgment = { }

def judgment_ : Lean.ParserDescr

Equations

• judgment_ = Lean.ParserDescr.node `judgment_ 50 (Lean.ParserDescr.cat `term 51)

def «judgment_≡_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «judgment_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «judgment_≡_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def univMax : ℕ

The maximum l for which Γ ⊢[l] 𝒥 makes sense. When set to 0, types cannot be quantified over at all.

Equations

• univMax = 3

@[reducible, inline]

abbrev Axioms (χ : Type u_1) : Type u_1

An axiom environment is a (possibly infinite) set of closed term constants indexed by a type of names χ. χ is in general larger than necessary and not all names correspond to constants. We record the universe level and type of each constant.

We do not support type constants directly: they are just term constants in a universe. This does mean we cannot have type constants at level univMax.

We do not use Axioms for definitions; the native Lean Environment is used instead.

Equations

• Axioms χ = (χ → Option { Al : Expr χ × ℕ // Expr.isClosed 0 Al.fst = true ∧ Al.snd ≤ univMax })

@[reducible, inline]

abbrev Ctx (χ : Type u_1) : Type u_1

A typing context consisting of type expressions and their universe levels.

Equations

• Ctx χ = List (Expr χ × ℕ)

inductive Lookup {χ : Type u_1} : Ctx χ → ℕ → Expr χ → ℕ → Prop

Lookup Γ i A l means that A = A'[↑ⁱ⁺¹] where Γ[i] = (A', l). Together with ⊢ Γ, this implies Γ ⊢[l] .bvar i : A.

• zero {χ : Type u_1} (Γ : List (Expr χ × ℕ)) (A : Expr χ) (l : ℕ) : Lookup ((A, l) :: Γ) 0 (Expr.subst Expr.wk A) l
• succ {χ : Type u_1} {Γ : Ctx χ} {A : Expr χ} {i l : ℕ} (B : Expr χ) (l' : ℕ) : Lookup Γ i A l → Lookup ((B, l') :: Γ) (i + 1) (Expr.subst Expr.wk A) l

inductive WfCtx {χ : Type u_1} (E : Axioms χ) : Ctx χ → Prop

All types in the given context are well-formed.

• nil {χ : Type u_1} {E : Axioms χ} : WfCtx E []
• snoc {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : WfCtx E Γ → E ∣ Γ ⊢[l] A → WfCtx E ((A, l) :: Γ)

inductive WfTp {χ : Type u_1} (E : Axioms χ) : Ctx χ → ℕ → Expr χ → Prop

The type is well-formed at the specified universe level.

Many of the inference rules have redundant premises ("presuppositions"); these rules are postfixed with a prime ('). This makes it easier to push syntactic metatheory through. After proving inversion lemmas, we define more efficient rules with fewer premises, named the same but without the prime. This is not just for usability: it also means the Lean kernel is checking smaller derivation trees.

Convention on order of implicit parameters: contexts, types, terms, de Bruijn indices, universe levels.

• pi' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] Expr.pi l l' A B
• sigma' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] Expr.sigma l l' A B
• Id' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t u : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] u : A → E ∣ Γ ⊢[l] Expr.Id l A t u
• univ {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {l : ℕ} : WfCtx E Γ → l < univMax → E ∣ Γ ⊢[l + 1] Expr.univ l
• el {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l + 1] A : Expr.univ l → E ∣ Γ ⊢[l] A.el

inductive EqTp {χ : Type u_1} (E : Axioms χ) : Ctx χ → ℕ → Expr χ → Expr χ → Prop

The two types are equal at the specified universe level.

• cong_pi' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B B' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[max l l'] Expr.pi l l' A B ≡ Expr.pi l l' A' B'
• cong_sigma' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B B' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[max l l'] Expr.sigma l l' A B ≡ Expr.sigma l l' A' B'
• cong_Id {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' t t' u u' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l] u ≡ u' : A → E ∣ Γ ⊢[l] Expr.Id l A t u ≡ Expr.Id l A' t' u'
• cong_el {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l + 1] A ≡ A' : Expr.univ l → E ∣ Γ ⊢[l] A.el ≡ A'.el
• el_code {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : l < univMax → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A.code.el ≡ A
• refl_tp {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A ≡ A
• symm_tp {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l] A' ≡ A
• trans_tp {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' A'' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l] A' ≡ A'' → E ∣ Γ ⊢[l] A ≡ A''

inductive WfTm {χ : Type u_1} (E : Axioms χ) : Ctx χ → ℕ → Expr χ → Expr χ → Prop

The term has the specified type at the specified universe level.

Note: the type is the first Expr argument.

• ax {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {c : χ} {Al : { Al : Expr χ × ℕ // Expr.isClosed 0 Al.fst = true ∧ Al.snd ≤ univMax }} : WfCtx E Γ → E c = some Al → E ∣ Γ ⊢[Al.val.snd] Al.val.fst → E ∣ Γ ⊢[Al.val.snd] Expr.ax c Al.val.fst : Al.val.fst
• bvar {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {i l : ℕ} : WfCtx E Γ → Lookup Γ i A l → E ∣ Γ ⊢[l] Expr.bvar i : A
• lam' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] t : B → E ∣ Γ ⊢[max l l'] Expr.lam l l' A t : Expr.pi l l' A B
• app' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B f a : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] f : Expr.pi l l' A B → E ∣ Γ ⊢[l] a : A → E ∣ Γ ⊢[l'] Expr.app l l' B f a : Expr.subst a.toSb B
• pair' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l'] u : Expr.subst t.toSb B → E ∣ Γ ⊢[max l l'] Expr.pair l l' B t u : Expr.sigma l l' A B
• fst' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B p : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] p : Expr.sigma l l' A B → E ∣ Γ ⊢[l] Expr.fst l l' A B p : A
• snd' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B p : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] p : Expr.sigma l l' A B → E ∣ Γ ⊢[l'] Expr.snd l l' A B p : Expr.subst (Expr.fst l l' A B p).toSb B
• refl' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] Expr.refl l t : Expr.Id l A t t
• idRec' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A M t r u h : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ (Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M → E ∣ Γ ⊢[l'] r : Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M → E ∣ Γ ⊢[l] u : A → E ∣ Γ ⊢[l] h : Expr.Id l A t u → E ∣ Γ ⊢[l'] Expr.idRec l l' t M r u h : Expr.subst (Expr.snoc u.toSb h) M
• code {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A : Expr χ} {l : ℕ} : l < univMax → E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l + 1] A.code : Expr.univ l
• conv {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l] t : A'

inductive EqTm {χ : Type u_1} (E : Axioms χ) : Ctx χ → ℕ → Expr χ → Expr χ → Expr χ → Prop

The two terms are equal at the specified type and universe level.

Note: the type is the first Expr argument in order to make gcongr work. We still pretty-print it last following convention.

• cong_lam' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B t t' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A' → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] t ≡ t' : B → E ∣ Γ ⊢[max l l'] Expr.lam l l' A t ≡ Expr.lam l l' A' t' : Expr.pi l l' A B
• cong_app' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B B' f f' a a' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[max l l'] f ≡ f' : Expr.pi l l' A B → E ∣ Γ ⊢[l] a ≡ a' : A → E ∣ Γ ⊢[l'] Expr.app l l' B f a ≡ Expr.app l l' B' f' a' : Expr.subst a.toSb B
• cong_pair' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B B' t t' u u' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l'] u ≡ u' : Expr.subst t.toSb B → E ∣ Γ ⊢[max l l'] Expr.pair l l' B t u ≡ Expr.pair l l' B' t' u' : Expr.sigma l l' A B
• cong_fst' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B B' p p' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[max l l'] p ≡ p' : Expr.sigma l l' A B → E ∣ Γ ⊢[l] Expr.fst l l' A B p ≡ Expr.fst l l' A' B' p' : A
• cong_snd' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' B B' p p' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] A ≡ A' → E ∣ (A, l) :: Γ ⊢[l'] B ≡ B' → E ∣ Γ ⊢[max l l'] p ≡ p' : Expr.sigma l l' A B → E ∣ Γ ⊢[l'] Expr.snd l l' A B p ≡ Expr.snd l l' A' B' p' : Expr.subst (Expr.fst l l' A B p).toSb B
• cong_refl' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t t' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l] Expr.refl l t ≡ Expr.refl l t' : Expr.Id l A t t
• cong_idRec' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A M M' t t' r r' u u' h h' : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ (Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' → E ∣ Γ ⊢[l'] r ≡ r' : Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M → E ∣ Γ ⊢[l] u ≡ u' : A → E ∣ Γ ⊢[l] h ≡ h' : Expr.Id l A t u → E ∣ Γ ⊢[l'] Expr.idRec l l' t M r u h ≡ Expr.idRec l l' t' M' r' u' h' : Expr.subst (Expr.snoc u.toSb h) M
• cong_code {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' : Expr χ} {l : ℕ} : l < univMax → E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l + 1] A.code ≡ A'.code : Expr.univ l
• app_lam' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ (A, l) :: Γ ⊢[l'] t : B → E ∣ Γ ⊢[l] u : A → E ∣ Γ ⊢[l'] Expr.app l l' B (Expr.lam l l' A t) u ≡ Expr.subst u.toSb t : Expr.subst u.toSb B
• fst_pair' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l'] u : Expr.subst t.toSb B → E ∣ Γ ⊢[l] Expr.fst l l' A B (Expr.pair l l' B t u) ≡ t : A
• snd_pair' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B t u : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l'] u : Expr.subst t.toSb B → E ∣ Γ ⊢[l'] Expr.snd l l' A B (Expr.pair l l' B t u) ≡ u : Expr.subst t.toSb B
• idRec_refl' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A M t r : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t : A → E ∣ (Expr.Id l (Expr.subst Expr.wk A) (Expr.subst Expr.wk t) (Expr.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M → E ∣ Γ ⊢[l'] r : Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M → E ∣ Γ ⊢[l'] Expr.idRec l l' t M r t (Expr.refl l t) ≡ r : Expr.subst (Expr.snoc t.toSb (Expr.refl l t)) M
• lam_app' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B f : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] f : Expr.pi l l' A B → E ∣ Γ ⊢[max l l'] f ≡ Expr.lam l l' A (Expr.app l l' (Expr.subst (Expr.up Expr.wk) B) (Expr.subst Expr.wk f) (Expr.bvar 0)) : Expr.pi l l' A B
• pair_fst_snd' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A B p : Expr χ} {l l' : ℕ} : E ∣ Γ ⊢[l] A → E ∣ (A, l) :: Γ ⊢[l'] B → E ∣ Γ ⊢[max l l'] p : Expr.sigma l l' A B → E ∣ Γ ⊢[max l l'] p ≡ Expr.pair l l' B (Expr.fst l l' A B p) (Expr.snd l l' A B p) : Expr.sigma l l' A B
• code_el {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {a : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l + 1] a : Expr.univ l → E ∣ Γ ⊢[l + 1] a ≡ a.el.code : Expr.univ l
• conv_eq {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A A' t t' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l] A ≡ A' → E ∣ Γ ⊢[l] t ≡ t' : A'
• refl_tm {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] t : A → E ∣ Γ ⊢[l] t ≡ t : A
• symm_tm' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t t' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l] t' ≡ t : A
• trans_tm' {χ : Type u_1} {E : Axioms χ} {Γ : Ctx χ} {A t t' t'' : Expr χ} {l : ℕ} : E ∣ Γ ⊢[l] A → E ∣ Γ ⊢[l] t ≡ t' : A → E ∣ Γ ⊢[l] t' ≡ t'' : A → E ∣ Γ ⊢[l] t ≡ t'' : A

Pretty-printers

def «term_∣_⊢[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def WfTp.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def EqTp.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def WfTm.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

def EqTm.unexpand : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

Well-formed axiom environments

@[reducible, inline]

abbrev Axioms.Wf {χ : Type u_1} (E : Axioms χ) : Prop

The given axiom environment is well-formed.

Unlike contexts that change via substitutions, there is usually one fixed axiom environment that definitions 'live' over.

Equations

• E.Wf = ∀ ⦃c : χ⦄ ⦃p : { Al : Expr χ × ℕ // Expr.isClosed 0 Al.fst = true ∧ Al.snd ≤ univMax }⦄, E c = some p → E ∣ [] ⊢[p.val.snd] p.val.fst