Library ut_typ

Typing rules for standard PTS.

Require Import ut_term.
Require Import ut_red.
Require Import ut_env.
Require Import base.
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt Plus Minus.

Module ut_typ_mod (X:term_sig) (Y:pts_sig X) (TM: ut_term_mod X) (EM: ut_env_mod X TM) (RM: ut_red_mod X TM).
Import X Y TM EM RM.

Typing judgements:

Reserved Notation "Γ ⊢ t : T" (at level 80, t, T at level 30, no associativity) .
Reserved Notation "Γ ⊣ " (at level 80, no associativity).

Inductive wf : Env -> Prop :=
| wf_nil : nil ⊣
| wf_cons : forall Γ A s, Γ ⊢ A : !s -> A::Γ ⊣
where "Γ ⊣" := (wf Γ) : UT_scope
with typ : Env -> Term -> Term -> Prop :=
| cSort : forall Γ s t, Ax s t -> Γ ⊣ -> Γ ⊢ !s : !t
| cVar : forall Γ A v, Γ ⊣ -> A ↓ v ⊂ Γ -> Γ ⊢ #v : A
| cPi : forall Γ A B s t u, Rel s t u -> Γ ⊢ A : !s -> A::Γ ⊢ B : !t ->
Γ ⊢ Π (A), B : !u
| cLa : forall Γ A B M s1 s2 s3, Rel s1 s2 s3 -> Γ ⊢ A : !s1 ->
A::Γ ⊢ B : !s2 -> A::Γ ⊢ M : B -> Γ ⊢ λ [A], M : Π (A), B
| cApp : forall Γ M N A B , Γ ⊢ M : Π (A), B -> Γ ⊢ N : A -> Γ ⊢ M · N : B[←N]
| Cnv : forall Γ M A B s, A ≡ B -> Γ ⊢ M : A -> Γ ⊢ B : !s -> Γ ⊢ M : B
where "Γ ⊢ t : T" := (typ Γ t T) : UT_scope.

Hint Constructors wf typ.

Open Scope UT_scope.

Basic properties of PTS. Context Validity: if a judgment is valid, its context is well-formed.

Lemma wf_typ : forall Γ t T, Γ ⊢ t : T -> Γ ⊣.

Hint Resolve wf_typ.

Inversion Lemmas , one for each kind of term from a typing derivation of some particular term, we can infer informations about its type and subterms.

Lemma gen_sort : forall Γ s T, Γ ⊢ !s : T -> exists t, T ≡ !t /\ Ax s t.

Lemma gen_var : forall Γ x A, Γ ⊢ #x : A -> exists A', A ≡ A' /\ A' ↓ x ⊂ Γ .

Lemma gen_pi : forall Γ A B T, Γ ⊢ Π (A),B : T -> exists s1, exists s2, exists s3,
T ≡ !s3 /\ Rel s1 s2 s3 /\ Γ ⊢ A : !s1 /\ A::Γ ⊢ B : !s2 .

Lemma gen_la : forall Γ A M T, Γ ⊢ λ [A],M : T -> exists s1, exists s2, exists s3, exists B,
T ≡ Π (A), B /\ Rel s1 s2 s3 /\ Γ ⊢ A : !s1 /\ A::Γ ⊢ M : B /\ A::Γ ⊢ B : !s2.

Lemma gen_app : forall Γ M N T, Γ ⊢ M · N : T -> exists A, exists B, T ≡ B[← N] /\ Γ ⊢ M : Π (A),B /\ Γ ⊢ N : A.

Weakening Property: if a judgement is valid, we can insert a well-typed term in the context, it will remain valid. This is where the type checking for inserting items in a context is done.

Theorem weakening: (forall Δ M T, Δ ⊢ M : T -> forall Γ A s n Δ', ins_in_env Γ A n Δ Δ' -> Γ ⊢ A : !s ->
                 Δ' ⊢ M ↑ 1 # n : T ↑ 1 # n ) /\
(forall Γ, Γ ⊣ -> forall Δ Γ' n A , ins_in_env Δ A n Γ Γ' -> forall s, Δ ⊢ A : !s -> Γ' ⊣).

Theorem thinning :
   forall Γ M T A s,
      Γ ⊢ M : T ->
   Γ ⊢ A : !s ->
   A::Γ ⊢ M ↑ 1 : T ↑ 1.

Theorem thinning_n : forall n Δ Δ',
   trunc n Δ Δ' ->
   forall M T , Δ' ⊢ M : T -> Δ ⊣ ->
               Δ ⊢ M ↑ n : T ↑ n.

Substitution Property: if a judgment is valid and we replace a variable by a well-typed term of the same type, it will remain valid.

Theorem substitution : (forall Γ M T , Γ ⊢ M : T -> forall Δ P A, Δ ⊢ P : A ->
forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ ⊣ -> Γ' ⊢ M [ n ←P ] : T [ n ←P ] ) /\
(forall Γ , Γ ⊣ -> forall Δ P A n Γ' , Δ ⊢ P : A ->
sub_in_env Δ P A n Γ Γ' -> Γ' ⊣).

Well-formation of contexts: if a context is valid, every term inside is well-typed by a sort.

Lemma wf_item : forall Γ A n, A ↓ n ∈ Γ ->
forall Γ', Γ ⊣ -> trunc (S n) Γ Γ' -> exists s, Γ' ⊢ A : !s.

Lemma wf_item_lift : forall Γ A n ,Γ ⊣ -> A ↓ n ⊂ Γ ->
exists s, Γ ⊢ A : !s.

Type Correction: if a judgment is valid, the type is either welltyped itself, or syntacticaly a sort. This distinction comes from the fact that we abstracted the typing of sorts with Ax and that they may be some untyped sorts (also called top-sorts).

Theorem TypeCorrect : forall Γ M T, Γ ⊢ M : T ->
(exists s, T = !s) \/ (exists s, Γ ⊢ T : !s).

End ut_typ_mod.