Library typ_annot

Definition of PTS{atr} and proof of Confluence

In order to prove the equivalence between PTS and PTSe, Adams built a system called Typed Parallel One Step Reduction that mimics the usual parallel reduction to prove that a typed equality judgement is confluent. He emphasises the use of an additionnal annotation (the co-domain (x)B) in order to be able to track typing information, and prove that PTS{atr} enjoys the diamon property.

His result is restricted to "functional" PTS. To extend it to all PTS, we added a second annotation (the domain A) and prove that every PTS is equivalent to its PTSe counterpart.

Require Import base term.
Require Import red.
Require Import env.
Require Import base.
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt Plus Minus.

Module PTS_ATR_mod (X:term_sig) (Y:pts_sig X) (TM:term_mod X) (EM: env_mod X TM) (RM: red_mod X TM).
Import X Y TM EM RM.

PTS{atr} typind definition: we define at the same time the one step and the multistep in order to keep track of some well-typed path between two possible domains in the typ_beta case.

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

Inductive wf : Env -> Prop :=
  | wf_nil : nil ⊣
  | wf_cons : forall Γ A A' s, Γ ⊢ A ▹ A' : !s -> A::Γ ⊣
where "Γ ⊣" := (wf Γ) : Typ_scope
with typ : Env -> Term -> Term -> Term -> Prop :=
| typ_var : forall Γ x A, Γ ⊣ -> A ↓ x ⊂ Γ -> Γ ⊢ #x ▹ #x : A
| typ_sort : forall Γ s1 s2, Ax s1 s2 -> Γ ⊣ -> Γ ⊢ !s1 ▹ !s1 : !s2
| typ_pi : forall Γ s1 s2 s3 A A' B B', Rel s1 s2 s3 ->
    Γ ⊢ A ▹ A' : !s1 -> A::Γ ⊢ B ▹ B' : !s2 -> Γ ⊢ Π (A),B ▹ Π (A'),B' : !s3
| typ_la : forall Γ A A' B B' M M' s1 s2 s3, Rel s1 s2 s3 ->
    Γ ⊢ A ▹ A' : !s1 -> A::Γ ⊢ B ▹ B' : !s2 -> A::Γ ⊢ M ▹ M' : B ->
    Γ ⊢ λ [A],M ▹ λ [A'],M' : Π (A),B
| typ_app : forall Γ M M' N N' A A' B B' s1 s2 s3, Rel s1 s2 s3 ->
   Γ ⊢ A ▹ A' : !s1 -> A::Γ ⊢ B ▹ B' : !s2 -> Γ ⊢ M ▹ M' : Π (A),B -> Γ ⊢ N ▹ N' : A ->
    Γ ⊢ (M ·(A,B) N) ▹ (M'·(A',B') N') : B[ ←N]
| typ_beta : forall Γ M M' N N' A A' A'' A''' A0 B B' s1 s2 s3, Rel s1 s2 s3 ->
   Γ ⊢ A ▹ A' : !s1 -> Γ ⊢ A'' ▹ A''' : !s1 -> Γ ⊢ A0 ▹▹ A : !s1 -> Γ ⊢ A0 ▹▹ A'' : !s1 ->
   A::Γ ⊢ B ▹ B' : !s2 -> A::Γ ⊢ M ▹ M' : B -> Γ ⊢ N ▹ N' : A ->
    Γ ⊢ ((λ [A],M) ·(A'',B) N) ▹ M'[ ← N'] : B[ ←N]
| typ_red : forall Γ M N A B s, Γ ⊢ M ▹ N : A -> Γ ⊢ A ▹ B : !s -> Γ ⊢ M ▹ N : B
| typ_exp : forall Γ M N A B s, Γ ⊢ M ▹ N : B -> Γ ⊢ A ▹ B : !s -> Γ ⊢ M ▹ N : A
where "Γ ⊢ M ▹ N : T" := (typ Γ M N T) : Typ_scope
with typ_reds : Env -> Term -> Term -> Term -> Prop :=
| typ_reds_intro : forall Γ s t T, Γ ⊢ s ▹ t : T -> Γ ⊢ s ▹▹ t : T
| typ_reds_trans : forall Γ s t u T , Γ ⊢ s ▹▹ t : T -> Γ ⊢ t ▹▹ u : T -> Γ ⊢ s ▹▹ u : T
where "Γ ⊢ s ▹▹ t : T " := (typ_reds Γ s t T) : Typ_scope.

Open Scope Typ_scope.

Weakening property for PTS{atr} .

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

app with annot

beta with annot

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

Theorem thinning_reds :
   forall Γ M N T A A' s,
      Γ ⊢ M ▹▹ N : T ->
   Γ ⊢ A ▹ A' : !s ->
   A::Γ ⊢ M ↑ 1 ▹▹ N ↑ 1 : T ↑ 1.

Lemma wf_from_typ : forall Γ M N T, Γ ⊢ M ▹ N : T -> Γ ⊣.

Lemma wf_from_typ_reds : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> Γ ⊣.

Hint Resolve wf_from_typ wf_from_typ_reds.

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

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

In order to prove substitution for PTS{atr}, we first need to prove some context conversion lemmas, because of the new annotation we added. We will first prove some weak form of conversion, where the ending context is supposed to be welltyped. As soon as we will have the substitution property, we will be able to prove that it's in fact always the case.

Reduction in context definition .

Inductive env_red1 : Env -> Env -> Prop :=
| red1_intro : forall Γ A B s , Γ ⊢ A ▹ B : !s -> env_red1 (A::Γ) (B::Γ)
| red1_next : forall A Γ Γ', env_red1 Γ Γ' -> env_red1 (A::Γ) (A::Γ')
.

Hint Constructors env_red1.

Inductive env_red : Env -> Env -> Prop :=
| r_step : forall Γ Γ', env_red1 Γ Γ' -> env_red Γ Γ'
| r_refl : forall Γ , env_red Γ Γ
| r_trans : forall Γ Γ' Γ'', env_red Γ Γ' -> env_red Γ' Γ'' -> env_red Γ Γ''.

Hint Constructors env_red.

Lemma red_item : forall n A Γ Γ' , A ↓ n ⊂ Γ -> env_red1 Γ Γ' -> Γ' ⊣ -> A ↓ n ⊂ Γ' \/
(forall Γ'', trunc (S n) Γ Γ'' -> trunc (S n) Γ' Γ'') /\ (exists B, exists s, Γ' ⊢ A ▹ B : !s /\ B ↓ n ⊂ Γ').

Lemma red1_in_env : (forall Γ M N T, Γ ⊢ M ▹ N : T -> forall Γ', Γ' ⊣ -> env_red1 Γ Γ'-> Γ' ⊢ M ▹ N : T ) /\
(forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall Γ', Γ' ⊣ -> env_red1 Γ Γ'-> Γ' ⊢ M ▹▹ N : T ) /\
(forall Γ, Γ ⊣ -> True ).

Reflexive, Transitive, Symetric closure of PTS{atr}. Since we are not functional, we can't inforce the fact that every step is typed by the same type. But we only need the equality at the type level, so we will check that every step is welltyped, by a sort, but we will forget about this sort.

Reserved Notation "Γ ⊢ s ≡' t " (at level 80, s, t, T at level 30, no associativity) .

Inductive typ_peq : Env -> Term -> Term -> Prop :=
| typ_peq_intro : forall Γ A B s, Γ ⊢ A ▹ B : !s -> Γ ⊢ A ≡' B
| typ_peq_intro2 : forall Γ A B s, Γ ⊢ B ▹ A : !s -> Γ ⊢ A ≡' B
| typ_peq_trans : forall Γ A B C , Γ ⊢ A ≡' B -> Γ ⊢ B ≡' C -> Γ ⊢ A ≡' C
where "Γ ⊢ s ≡' t " := (typ_peq Γ s t) : Typ_scope.

Hint Constructors typ_peq.

Lemma typ_peq_sym : forall Γ A B , Γ ⊢ A ≡' B -> Γ ⊢ B ≡' A .

Hint Resolve typ_peq_sym.

Lemma reds_to_conv : forall Γ M N s, Γ ⊢ M ▹▹ N : !s -> Γ ⊢ M ≡' N.

Hint Resolve reds_to_conv.

Conversion in Context definition .

Inductive env_conv1 : Env -> Env -> Prop :=
| conv1_intro : forall Γ A B , Γ ⊢ A ≡' B -> env_conv1 (A::Γ) (B::Γ)
| conv1_next : forall A Γ Γ', env_conv1 Γ Γ' -> env_conv1 (A::Γ) (A::Γ')
.

Hint Constructors env_conv1.

Inductive env_conv : Env -> Env -> Prop :=
| c_step : forall Γ Γ', env_conv1 Γ Γ' -> env_conv Γ Γ'
| c_refl : forall Γ , env_conv Γ Γ
| c_trans : forall Γ Γ' Γ'', env_conv Γ Γ' -> env_conv Γ' Γ'' -> env_conv Γ Γ''.

Hint Constructors env_conv.

Lemma c1_sym : forall Γ Γ', env_conv1 Γ Γ' -> env_conv1 Γ' Γ.

Lemma c_sym : forall Γ Γ', env_conv Γ Γ' -> env_conv Γ' Γ.

Hint Resolve c_sym.

Lemma env_red1_to_conv1 : forall Γ Γ', env_red1 Γ Γ' -> env_conv1 Γ Γ'.

Lemma env_red_to_conv : forall Γ Γ', env_red Γ Γ' -> env_conv Γ Γ'.

Hint Resolve env_red_to_conv.

Lemma peq_thinning : forall Γ A B, Γ ⊢ A ≡' B -> forall C C' s, Γ ⊢ C ▹ C' : !s
-> C::Γ ⊢ A ↑ 1 ≡' B ↑ 1.

Lemma peq_thinning_n : forall n Δ Δ',
trunc n Δ Δ' ->
forall A B , Δ' ⊢ A ≡' B -> Δ ⊣ -> Δ ⊢ A ↑ n ≡' B ↑ n .

Type manipulation functions

Lemma typ_pcompat : forall Γ M N A, Γ ⊢ M ▹ N : A -> forall B , Γ ⊢ A ≡' B -> Γ ⊢ M ▹ N : B.

Lemma typ_red_trans : forall Γ M N A B s, Γ ⊢ M ▹ N : A -> Γ ⊢ A ▹▹ B : !s -> Γ ⊢ M ▹ N : B.

Lemma typ_exp_trans : forall Γ M N A B s, Γ ⊢ M ▹ N : B -> Γ ⊢ A ▹▹ B : !s -> Γ ⊢ M ▹ N : A.

  Lemma conv_item :
   forall n A Γ Γ', A ↓ n ⊂ Γ -> env_conv1 Γ Γ' -> Γ' ⊣ -> A ↓ n ⊂ Γ' \/
     (forall Γ'', trunc (S n) Γ Γ'' -> trunc (S n) Γ' Γ'') /\ (exists B, Γ' ⊢ A ≡' B /\ B ↓ n ⊂ Γ').

Lemma conv1_in_env : (forall Γ M N T, Γ ⊢ M ▹ N : T -> forall Γ', env_conv1 Γ Γ' -> Γ' ⊣ -> Γ' ⊢ M ▹ N : T) /\
  (forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall Γ', env_conv1 Γ Γ' -> Γ' ⊣ -> Γ' ⊢ M ▹▹ N : T) /\
  (forall Γ, Γ ⊣ -> True ).

Lemma sub_trunc : forall Γ0 a A n Γ Δ, sub_in_env Γ0 a A n Γ Δ -> trunc n Δ Γ0.

Lemma sub_in_env_item : forall Δ P A n Γ Γ', sub_in_env Δ P A n Γ Γ' -> A ↓ n ∈ Γ.

Left-Hand reflexivity: this ensure that a valid derivation starts from a well typed term.

Theorem red_refl_lt : forall Γ M N T, Γ ⊢ M ▹ N : T -> Γ ⊢ M ▹ M :T.

Lemma reds_refl_lt : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> Γ ⊢ M ▹ M :T.

Substitution Lemma

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

Right-Hand Reflexivity: this time, is the ending part of a judgment that's always valid.

Theorem red_refl_rt : forall Γ M N T, Γ ⊢ M ▹ N : T -> Γ ⊢ N ▹ N :T.

Lemma reds_refl_rt : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> Γ ⊢ N ▹ N :T.

With Left and Right reflexivity, we can finally prove that context conversion preserves validity of context.

Lemma env_red1_wf : forall Γ Γ' , env_red1 Γ Γ' -> Γ ⊣ -> Γ' ⊣.

Lemma env_red_wf : forall Γ Γ' , env_red Γ Γ' -> Γ ⊣ -> Γ' ⊣.

Lemma red_in_env : forall Γ M N T, Γ ⊢ M ▹ N : T -> forall Γ', env_red Γ Γ'-> Γ' ⊢ M ▹ N : T.

Lemma red_in_env_reds : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall Γ', env_red Γ Γ'-> Γ' ⊢ M ▹▹ N : T.

Lemma wf_from_peq : forall Γ M N , Γ ⊢ M ≡' N -> Γ⊣.

Hint Resolve wf_from_peq.

Every step of an equality is welltyped, by a sort, but we need to guess it.

Lemma typ_peq_to_red : forall Γ A B , Γ ⊢ A ≡' B -> exists s, exists t,
Γ ⊢ A ▹ A : !s /\ Γ ⊢ B ▹ B : !t.

Lemma env_conv1_wf : forall Γ Γ' , env_conv1 Γ Γ' -> Γ ⊣ -> Γ' ⊣.

Lemma env_conv_wf : forall Γ Γ' , env_conv Γ Γ' -> Γ ⊣ -> Γ' ⊣.

Final Conversion in Context.

Theorem conv_in_env : forall Γ M N T, Γ ⊢ M ▹ N : T -> forall Γ', env_conv Γ Γ'-> Γ' ⊢ M ▹ N : T.

Theorem conv_in_env_reds : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall Γ', env_conv Γ Γ'-> Γ' ⊢ M ▹▹ N : T.

Lemma env_red_cons : forall a b s Γ Γ', Γ ⊢ a ▹▹ b : !s -> env_red Γ Γ' ->
env_red (a::Γ) (b::Γ').

Lemma env_conv_cons : forall a b Γ Γ', Γ ⊢ a ≡' b -> env_conv Γ Γ' ->
env_conv (a::Γ) (b::Γ').
Theorem conv_in_env_peq : forall Γ A B, Γ ⊢ A ≡' B -> forall Γ', env_conv Γ Γ' ->
Γ' ⊢ A ≡' B.

Inversion lemma: as for PTS, if a term is well typed, we can infer a lot of information on its type, subterms, or reduce form.

Lemma pgen_sort : forall Γ s N T, Γ ⊢ !s ▹ N : T ->
  N = !s /\ ( exists t, Ax s t /\ (T = !t \/ Γ ⊢ T ≡' !t )).

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

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

Lemma pgen_var : forall Γ x N T, Γ ⊢ #x ▹ N : T ->
  N = #x /\ ( exists Z, Z ↓ x ⊂ Γ /\ Γ ⊢ T ≡' Z ).

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

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

Lemma pgen_app : forall Γ W P V X Y Z , Γ ⊢ (W ·(P,V) X) ▹ Y : Z -> exists U, exists U', exists V',
exists X', exists s1, exists s2, exists s3, Rel s1 s2 s3 /\ Γ ⊢ U ▹ U' : !s1 /\
U::Γ ⊢ V ▹ V' : !s2 /\ Γ ⊢ X ▹ X' : U /\ Γ ⊢ V[← X] ≡' Z /\
( (exists W', Γ ⊢ W ▹ W' : Π (U),V /\ P = U /\ Y = W' ·(U',V') X' ) \/
   (exists K0, exists K, exists K', exists T, exists T', P = K /\ W = λ [U],T /\ U::Γ ⊢ T ▹ T' : V /\ Y = T'[←X'] /\
  Γ ⊢ K0 ▹▹ K : !s1 /\ Γ ⊢ K0 ▹▹ U : !s1 /\ Γ ⊢ K ▹ K' : !s1 )).

Lemma fun_item_lift : forall A A' v Γ , A ↓ v ⊂ Γ -> A' ↓ v ⊂ Γ -> A = A'.

Correctness of typing.

Lemma typ_wf : forall Γ M N A , Γ ⊢ M ▹ N : A -> (exists s, A = !s) \/ (exists s, Γ ⊢ A ▹ A : !s).

Type Exchange: this property is critic. We need it to simulate a reduction we know valid in another of it's type. We will use it to reannotate some type reductions in the correct sorts, in order to be allowed by Rel to build Pi-types.

Theorem relocate : forall Γ M N A , Γ ⊢ M ▹ N : A -> forall P B, Γ ⊢ M ▹ P : B -> Γ ⊢ M ▹ N : B /\ Γ ⊢ M ▹ P : A.

Facts abouts Reds

Lemma typ_reds_trans_ : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall P T', Γ ⊢ N ▹ P : T' -> Γ ⊢ M ▹▹ P : T.

Lemma typ_reds_trans2 : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall P T', Γ ⊢ N ▹▹ P : T' -> Γ ⊢ M ▹▹ P : T.

Hint Resolve typ_reds_trans2.

Lemma typ_reds_relocate : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> forall P T', Γ ⊢ M ▹ P : T' -> Γ ⊢ M ▹▹ N : T'.

Lemma reds_typ_pcompat : forall Γ M N A , Γ ⊢ M ▹▹ N : A -> forall B , Γ ⊢ A ≡' B -> Γ ⊢ M ▹▹ N : B.

Another version of inversion lemmas: for multi-step reduction.

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

Lemma La_Reds : forall Γ A b N T, Γ ⊢ λ [A],b ▹▹ N : T -> exists A', exists b', exists D, exists D', exists s1, exists s2, exists s3,
Rel s1 s2 s3 /\ N = λ [A'],b' /\ Γ ⊢ A ▹▹ A' : !s1 /\ A::Γ ⊢ b ▹▹ b' : D /\ A::Γ ⊢ D ▹▹ D' : !s2 /\ Γ ⊢ T ≡' Π (A),D.

Lemma Sort_Reds : forall Γ s P T, Γ ⊢ !s ▹▹ P : T -> P = !s /\ exists t, Ax s t /\ (T = !t \/ ( Γ ⊢ T ≡' !t)).

Diamond Property: PTS{atr} is like Betap, it enjoys the diamond property. This is where half the magic happens (and mainly where the new annotation is needed.

Theorem OSDiamond : forall Γ M N A , Γ ⊢ M ▹ N : A -> forall P B, Γ ⊢ M ▹ P : B ->
exists Q, Γ ⊢ N ▹ Q : A /\ Γ ⊢ N ▹ Q : B /\ Γ ⊢ P ▹ Q: A /\ Γ ⊢ P ▹ Q : B.

YOUHHHHOU

Lemma SubDiam : forall Γ M N A, Γ ⊢ M ▹ N : A -> forall P B, Γ ⊢ M ▹▹ P : B -> exists Q, Γ ⊢ N ▹▹ Q : A /\ Γ ⊢ P ▹ Q : B.

Lemma ChurchRosser: forall Γ M N A , Γ ⊢ M ▹▹ N : A -> forall P B, Γ ⊢ M ▹▹ P : B -> exists Q, Γ ⊢ N ▹▹ Q : A /\ Γ ⊢ P ▹▹ Q: B.

Theorem Confluence : forall Γ A B, Γ ⊢ A ≡' B -> exists Q,exists s, exists t, Γ ⊢ A ▹▹ Q : !s /\ Γ ⊢ B ▹▹ Q : !t.

The holy graal: Weak Pi Injectivity is the key property to prove Typed SubjectReduction and the equivalence between PTS and PTSe.

Theorem PiInj : forall Γ A B C D , Γ ⊢ Π (A),B ≡' Π (C),D -> Γ ⊢ A ≡' C /\ A::Γ ⊢ B ≡' D.

Some congruence consequences of PiInj .

Lemma ConvSort : forall Γ s t, Γ ⊢ !s ≡' !t -> s = t.

Lemma reds_Pi : forall Γ A A' s, Γ ⊢ A ▹▹ A' : !s -> forall B B' t u, A::Γ ⊢ B ▹▹ B' :!t ->
  Rel s t u -> Γ ⊢ Π (A), B ▹▹ Π (A'), B' : !u.

Lemma reds_La : forall Γ A A' s, Γ ⊢ A ▹▹ A' : !s -> forall M M' B B' t u, A::Γ ⊢ M ▹▹ M' :B ->
  A::Γ ⊢ B ▹ B' : !t -> Rel s t u -> Γ ⊢ λ [A], M ▹▹ λ [A'], M' :Π (A), B .

Lemma reds_subst : forall A Γ M M' B , A::Γ ⊢ M ▹▹ M' : B -> forall N N' , Γ ⊢ N ▹ N' : A ->
   Γ ⊢ M[ ← N ] ▹▹ M' [ ← N' ] : B[ ← N ].

Lemma reds_subst_gen : forall A Γ M M' B , A::Γ ⊢ M ▹▹ M' : B -> forall N N' , Γ ⊢ N ▹▹ N' : A ->
   Γ ⊢ M[ ← N ] ▹▹ M' [ ← N' ] : B[ ← N ].

Lemma eq_subst_gen : forall A Γ M M' , A::Γ ⊢ M ≡' M' -> forall N N' N'' , Γ ⊢ N ▹▹ N' : A ->
Γ ⊢ N'' ▹▹ N' : A -> Γ ⊢ M[ ← N ] ≡' M' [ ← N'' ] .

Lemma reds_App_ : forall Γ M M' A B , Γ ⊢ M ▹▹ M' : Π (A),B -> forall N N' , Γ ⊢ N ▹▹ N' : A ->
  Γ ⊢ M ·(A,B) N ▹▹ M'·(A,B) N' : B[ ← N].

Lemma reds_App__ : forall Γ M M' A B , Γ ⊢ M ▹ M' : Π (A),B -> forall B' s N N' , Γ ⊢ N ▹ N' : A ->
A::Γ ⊢ B ▹▹ B' : !s -> Γ ⊢ M ·(A,B) N ▹▹ M·(A,B') N : B[ ← N].

Lemma reds_App___ : forall Γ M M' A B , Γ ⊢ M ▹ M' : Π (A),B -> forall A' s N N' , Γ ⊢ N ▹ N' : A ->
Γ ⊢ A ▹▹ A' : !s -> Γ ⊢ M ·(A,B) N ▹▹ M·(A',B) N : B[ ← N].

Lemma reds_App : forall Γ M M' A B , Γ ⊢ M ▹▹ M' : Π (A),B -> forall A' B' s t N N' , Γ ⊢ N ▹▹ N' : A ->
Γ ⊢ A ▹▹ A' : !s -> A::Γ ⊢ B ▹▹ B' : !t -> Γ ⊢ M ·(A,B) N ▹▹ M'·(A',B') N' : B[ ← N].

Subject Reduction: PTS{atr} can lift an untyped reduction from Betap to PTS{atr}. However, we prove here that a one-step Betap reduction can be lifted to a multi-step PTS{atr} judgment. This is because of our new annotation, we need some room to check the validity of the typing.

Theorem SR : (forall M N, Betap M N -> forall Γ P A, Γ ⊢ M ▹ P : A -> Γ ⊢ M ▹▹ N : A ).

Lemma SR_trans : (forall M N, Betaps M N -> forall Γ P A, Γ ⊢ M ▹ P : A -> Γ ⊢ M ▹▹ N : A ).

Lemma SR_trans' : forall M N, Betas M N -> forall Γ P A, Γ ⊢ M ▹ P : A -> Γ ⊢ M ▹▹ N : A.

Lemma peq_subst : forall A Γ B B' , A::Γ ⊢ B ≡' B' -> forall N N' , Γ ⊢ N ▹ N' : A ->
Γ ⊢ B [ ← N ] ≡' B'[ ← N].
End PTS_ATR_mod.