Library ut_typ_eq

Definition of PTS with Judgmental Equality (PTSe)

Here we will define what is a judgmental equality and some basic results.

The main difference between PTS and PTSe is that we do not rely here on bare beta-conversion, but we also check that every step of the conversion is welltyped.

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

Module Type ut_typ_eq_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)
(SRM: ut_sr_mod X Y TM EM RM).
Import X Y TM EM RM SRM.

Typing Rules.

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

Inductive wf : Env -> Prop :=
| wfe_nil : nil ⊣e
| wfe_cons : forall Γ A s, Γ ⊢e A : !s -> A::Γ ⊣e
where "Γ ⊣e" := (wf Γ) : UT_scope
with typ : Env -> Term -> Term -> Prop :=
| cSort : forall Γ s t, Ax s t -> Γ ⊣e -> Γ ⊢e !s : !t
| cVar : forall Γ A v, Γ ⊣e -> A ↓ v ⊂ Γ -> Γ ⊢e #v : A
| cPi : forall Γ A B s t u,
     Rel s t u -> Γ ⊢e A : !s -> A::Γ ⊢e B : !t -> Γ ⊢e Π (A), B : !u
| cLa : forall Γ A b B s1 s2 s3, Rel s1 s2 s3 -> Γ ⊢e A : !s1 -> A::Γ ⊢e B : !s2 ->
     A::Γ ⊢e b : B -> Γ ⊢e λ [A], b: Π (A), B
| cApp : forall Γ a b A B , Γ ⊢e a : Π (A), B -> Γ ⊢e b : A -> Γ ⊢e a·b : B[←b]
| Cnv : forall Γ a A B s,
      Γ ⊢e A = B : !s -> Γ ⊢e a : A -> Γ ⊢e a : B
where "Γ ⊢e t : T" := (typ Γ t T) : UT_scope
with typ_eq : Env -> Term -> Term -> Term -> Prop :=
|cPi_eq : forall Γ A A' B B' s t u, Rel s t u -> Γ ⊢e A = A' : !s -> (A::Γ)⊢e B = B' : !t ->
   Γ ⊢e Π (A),B = Π (A'),B' : !u
| cLa_eq : forall Γ A A' B M M' s t u, Rel s t u -> Γ ⊢e A = A' : !s -> (A::Γ) ⊢e M = M' : B ->
   (A::Γ) ⊢e B : !t -> Γ ⊢e λ [A],M = λ [A'],M' : Π (A),B
| cApp_eq : forall Γ M M' N N' A B, Γ ⊢e M = M' : Π (A),B -> Γ⊢e N = N' : A ->
     Γ ⊢e M·N = M'·N' : B [← N]
| cRefl : forall Γ M A, Γ ⊢e M : A -> Γ ⊢e M = M : A
| cSym : forall Γ M N A , Γ ⊢e M = N : A -> Γ ⊢e N = M : A
| cTrans : forall Γ M N P A, Γ ⊢e M = N : A -> Γ ⊢e N = P : A -> Γ ⊢e M = P : A
| Cnv_eq : forall Γ M N A B s, Γ ⊢e A = B : !s -> Γ ⊢e M = N : A -> Γ ⊢e M = N : B
| cBeta : forall Γ A B M N s t u, Rel s t u -> Γ ⊢e A : !s -> (A::Γ) ⊢e B : !t ->
    (A::Γ) ⊢e M : B -> Γ ⊢e N : A -> Γ ⊢e (λ [A],M)·N = M[← N] : B[← N]
where "Γ ⊢e M = N : T":= (typ_eq Γ M N T) : UT_scope.

Hint Constructors wf typ typ_eq.

Open Scope UT_scope.

These lemmas are almost the same as for declarative PTS:

well formation of contexts
weakening
substitution
type correctness
...

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

Lemma wf_typ_eq : forall Γ M N T, Γ ⊢e M = N : T -> Γ ⊣e.

Hint Resolve wf_typ wf_typ_eq.

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

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

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

Theorem thinning_eq :
   forall Γ M N T A s,
      Γ ⊢e M = N : T ->
   Γ ⊢e A : !s ->
   A::Γ ⊢e M ↑ 1 = N ↑ 1 : T ↑ 1.

Theorem thinning_eq_n : forall n Δ Δ',
   trunc n Δ Δ' ->
   forall M N T , Δ' ⊢e M = N : T -> Δ ⊣e ->
               Δ ⊢e M ↑ n = N ↑ n: T ↑ n.

Lemma conv_in_env_var : forall C n Γ, C ↓ n ∈ Γ ->
  forall Γ1 Γ2 A B s, Γ = Γ2++(A::Γ1) -> Γ1 ⊢e A = B : !s -> n < List.length Γ2 ->
  C ↓ n ∈ Γ2++(B::Γ1).

Lemma conv_in_env_var2 : forall C n Γ, C ↓ n ∈ Γ ->
  forall Γ1 Γ2 A B s , Γ = Γ2++(A::Γ1) -> Γ1 ⊢e A = B : !s ->
  List.length Γ2 < n ->
  C ↓ n ∈ Γ2++(B::Γ1).

Lemma conv_in_env_var3 : forall Γ1 (B:Term) Γ2 , B ↓ (List.length Γ1) ∈ Γ1++(B::Γ2).

Lemma conv_in_env_var_lift : forall C n Γ, C ↓ n ⊂ Γ ->
  forall Γ1 Γ2 A B s, Γ = Γ2 ++(A::Γ1) -> Γ1 ⊢e A = B : !s -> n < List.length Γ2 ->
  C ↓ n ⊂ Γ2++(B::Γ1).

Lemma conv_in_env_var_lift2 : forall C n Γ, C ↓ n ⊂ Γ ->
  forall Γ1 Γ2 A B s, Γ = Γ2++(A::Γ1) -> Γ1 ⊢e A = B : !s ->
  List.length Γ2 < n -> C ↓ n ⊂ Γ2++(B::Γ1).

Lemma conv_in_env_var_lift3 : forall Γ1 (A:Term) Γ2 ,
  (A ↑ (S (List.length Γ1))) ↓ (List.length Γ1) ⊂ Γ1++(A::Γ2).

Lemma conv_in_env_aux_trunc : forall A (Γ1 Γ2:list A) B ,
  trunc (S (length Γ1)) (Γ1 ++ B :: Γ2) Γ2.

Conversion is the context is here provable without SR since every reduction step is checked valid.

Theorem conv_in_env : (forall Γ M T, Γ ⊢e M : T-> forall Γ1 Γ2 A B s, Γ = Γ1++(A::Γ2) -> Γ2 ⊢e A = B : !s ->
  Γ2 ⊢e B : !s -> (Γ1++(B::Γ2)) ⊢e M : T) /\
(forall Γ M N T, Γ ⊢e M = N : T-> forall Γ1 Γ2 A B s, Γ = Γ1++(A::Γ2) -> Γ2 ⊢e A = B : !s ->
  Γ2 ⊢e B : !s -> (Γ1++(B::Γ2)) ⊢e M = N : T ) /\
(forall Γ, Γ ⊣e -> forall Γ1 Γ2 A B s, Γ = Γ1++(A::Γ2) -> Γ2 ⊢e A = B : !s -> Γ2 ⊢e B : !s -> Γ1++(B::Γ2) ⊣e ).

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

Here is the generalization of the substitution

Lemma substitution2 : forall Γ t T , Γ ⊢e t : T -> forall Δ P P' A, Δ ⊢e P = P': A ->
  Δ ⊢e P : A -> forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ' ⊢e t [ n ←P ] = t [ n ← P'] : T [ n ←P ].

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

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

Lemma wgen_pi : forall Γ A B T, Γ ⊢e Π (A),B : T -> exists s, exists t, exists u, Rel s t u /\
Γ ⊢e A : !s /\ (A::Γ) ⊢e B : !t.

Reflexivity and Type Correctness: since we have symetry, and we did not check for the well formation of the function type in the app-eq rule, we need to prove all at once:

Type Correctness

Left-Hand Reflexivity

Right-Hand Reflexivity

Lemma TypeCorrect_Refl : (forall Γ M T, Γ ⊢e M : T -> exists s, T = !s \/ Γ ⊢e T : !s) /\
(forall Γ M N T, Γ ⊢e M = N : T -> Γ ⊢e M : T /\ Γ ⊢e N : T /\ exists s, T = !s \/ Γ ⊢e T : !s) /\
(forall Γ, Γ ⊣e -> True ).

Lemma TypeCorrect : forall Γ M T, Γ ⊢e M : T -> exists s, T = !s \/ Γ ⊢e T : !s.

Lemma TypeCorrect_eq : forall Γ M N T, Γ ⊢e M = N : T -> exists s, T = !s \/ Γ ⊢e T : !s.

Lemma left_reflexivity : forall Γ M N T, Γ ⊢e M = N : T -> Γ ⊢e M : T.

Lemma right_reflexivity : forall Γ M N T, Γ ⊢e M = N : T -> Γ ⊢e N : T.

We can easily prove that every judgement in PTSe is a valid one in PTS. It's just a matter of "forgetting" typing information during the conversion.

Lemma FromPTSe_to_PTS : (forall Γ M T, Γ ⊢e M : T -> Γ ⊢ M : T) /\
(forall Γ M N T, Γ ⊢e M = N : T -> Γ ⊢ M : T /\ Γ ⊢ N : T /\ M ≡ N) /\
(forall Γ, Γ ⊣e -> Γ ⊣).

End ut_typ_eq_mod.