Library ut_typ_eq_inj

Definition of a weaker form a Pi injectivity for PTSe

Since Strong Pi injectivity is wrong in the general case, we define here a weaker form of Pi injectivity, which is informative enought to directly prove Subject Reduction. However, we still don't know if this injectivity is provable without using PTS{atr} and the general equivalence.

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

Module ut_typ_eq_inj_mod (X:term_sig) (Y:pts_sig X).
  Include Theory X Y.
  Import X Y.

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

Inductive wtyp_eq : Env -> Term -> Term -> Prop :=
| wtyp_eq_intro : forall Γ A B s, Γ ⊢e A = B : !s -> Γ ⊢e A = B
| wtyp_eq_intro2 : forall Γ A B s, Γ ⊢e A = B : !s -> Γ ⊢e B = A
| wtyp_eq_trans : forall Γ A B C, Γ ⊢e A = B -> Γ ⊢e B = C -> Γ ⊢e A = C
where "Γ ⊢e M = N" := (wtyp_eq Γ M N): UT_scope.

Hint Constructors wtyp_eq.

Open Scope UT_scope.

Lemma wtyp_eq_sym: forall Γ A B, Γ ⊢e B = A -> Γ ⊢e A = B.

Hint Resolve wtyp_eq_sym.

Lemma weak_to_PTSe : forall Γ A B, Γ ⊢e A = B -> exists a, exists b, Γ ⊢e A : !a /\ Γ ⊢e B : !b.

Lemma weak_to_PTS : forall Γ A B, Γ ⊢e A = B -> A ≡ B.

Lemma wconv_in_env : forall Γ A B, Γ ⊢e A = B -> forall M T, A::Γ ⊢e M : T -> B::Γ ⊢e M : T.

Lemma Cnv_wtyp_eq : forall Γ M T, Γ ⊢e M : T -> forall T', Γ ⊢e T = T' -> Γ ⊢e M : T'.

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

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

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

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

Lemma wPiInj : forall Γ A B C D, Γ ⊢e Π (A),B = Π (C),D -> Γ ⊢e A = C /\ A::Γ ⊢e B = D.

Lemma wtyp_eq_subst : forall Γ M N , Γ ⊢e M = N -> forall Δ P A, Δ ⊢e P : A ->
forall Γ' n , sub_in_env Δ P A n Γ Γ' -> Γ' ⊢e M [ n ←P ] = N [ n ←P ].

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

End ut_typ_eq_inj_mod.