Library final_result

Final Result : PTS <-> PTSe

Here we use PTS{atr} as an intermediate system to prove that any judgement in PTS can be lifted in PTSe, which means that we can build a valid equality judgement from a Beta conversion.

Then we will use this equivalence to prove that PTSe enjoys the Subject Reduction property.

Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.

Require Import base.
Require Import ut_term.
Require Import ut_red.
Require Import ut_env.
Require Import ut_red ut_typ.
Require Import ut_sr ut_typ_eq.
Require Import term.
Require Import red env.
Require Import typ_annot.
Require Import glue.
Require Import List.
Require Import strip.

Module final_mod (X:term_sig) (Y:pts_sig X)
  (TM:term_mod X) (EM: env_mod X TM) (RM: red_mod X TM)
  (UTM:ut_term_mod X) (UEM: ut_env_mod X UTM) (URM: ut_red_mod X UTM)
  (PTS : ut_sr_mod X Y UTM UEM URM) (PTSe : ut_typ_eq_mod X Y UTM UEM URM PTS)
  (PTS_ATR: glue_mod X Y TM EM RM UTM UEM URM).
Import X Y UTM UEM URM TM EM RM PTS PTSe PTS_ATR.

Open Scope Typ_scope.

Now that we know how to glue types and contexts together, we can annotate a PTS judgement into a PTS{atr} one.

Lemma FromPTS_to_PTSATR : (forall Γ M A , PTS.typ Γ M A -> exists Γ', exists M', exists A', strip_env Γ' = Γ /\
strip M' = M /\ strip A' = A /\ Γ' ⊢ M' ▹ M' : A') /\
(forall Γ , PTS.wf Γ -> exists Γ', strip_env Γ' = Γ /\ wf Γ').

Easy part of the translation: by stripping the application of their annotations, we prove that:

a valid PTS{atr} judgement can be stripped to a valide PTS judgement
a valid PTS{atr} judgement can be stripped to a valide PTSe judgement

Lemma FromPTSATR_to_PTS : (forall Γ M N T, Γ ⊢ M ▹ N : T -> (strip_env Γ) ⊢ (strip M) : (strip T) /\
(strip_env Γ) ⊢ (strip N) : (strip T) /\ (strip M) ≡ (strip N)) /\
(forall Γ M N T, Γ ⊢ M ▹▹ N : T -> (strip_env Γ) ⊢ (strip M) : (strip T) /\
(strip_env Γ) ⊢ (strip N) : (strip T) /\ (strip M) ≡ (strip N)) /\
(forall Γ, Γ ⊣ -> ((strip_env Γ) ⊣)%UT).

Lemma FromPTSATR_to_PTSe : (forall Γ M N T, Γ ⊢ M ▹ N : T -> (strip_env Γ) ⊢e (strip M) = (strip N) : (strip T)) /\
(forall Γ M N T, Γ ⊢ M ▹▹ N : T -> (strip_env Γ) ⊢e (strip M) = (strip N) : (strip T)) /\
(forall Γ, (PTS_ATR.wf Γ) -> ((strip_env Γ) ⊣e)%UT).

Lemma FromPTSATR_to_PTSe_trans : forall Γ M N T, Γ ⊢ M ▹▹ N : T -> (strip_env Γ) ⊢e (strip M) = (strip N) : (strip T).

With the previous result, we can complete the following chart:

ut_typ_eq.v : PTSe -> PTS
: PTS -> PTS{atr}
: PTS{atr} -> PTS
: PTS{atr} -> PTSe

So PTSe -> PTS -> PTS{atr} -> PTSe which prove that PTSe <-> PTS.

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

Print Assumptions PTS_equiv_PTSe.

Lemma PTSe_SR : forall Γ M N T, Γ ⊢e M : T -> (M → N)%UT -> Γ ⊢e M = N : T.

Lemma PTSe_SR_trans : forall Γ M N T, Γ ⊢e M : T -> (M →→ N)%UT -> Γ ⊢e M = N : T.

End final_mod.

Module Type Theory (X:term_sig) (Y:pts_sig X) .
Module PTSATR.
  Include term_mod X.
  Include env_mod X.
  Include red_mod X.
End PTSATR.

Module PTS.
  Include ut_term_mod X.
  Include ut_env_mod X.
  Include ut_red_mod X.
  Include ut_sr_mod X Y.
End PTS.

Module PTSe.
Include ut_typ_eq_mod X Y PTS PTS PTS PTS.
End PTSe.

Include glue_mod X Y PTSATR PTSATR PTSATR PTS PTS PTS.
Include final_mod X Y PTSATR PTSATR PTSATR PTS PTS PTS PTS PTSe.

Export PTSATR PTS PTSe.
End Theory.