Library glue

Validity of Annotations

In this file, we prove all the tools we need to show that a welltyped judgment of PTS can be annotated in a valid judgement of PTS{atr}. With this, we give a validity to the annotation system we chose.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt Plus Minus.

Require Import base.
Require Import term.
Require Import env red.
Require Import typ_annot.
Require Import List.
Require Import ut_term ut_env ut_red.
Require Import strip.

Module Type glue_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).
 Import X Y UTM UEM URM TM EM RM.
 Include (strip_mod X UTM TM UEM EM).
 Include (PTS_ATR_mod X Y TM EM RM).

Open Scope Typ_scope.

This lemma gives some partial information about a term, when its types are not convertible, it will be usefull to prove that annotation in application are safe.
Lemma weak_type_shape : forall Γ M N A, Γ M N : A -> forall P B, Γ M P : B ->
 Γ A ≡' B \/ (exists U,exists V, Γ M λ[U],V : A /\ Γ M λ[U],V : B) \/
 (exists s, Γ M !s : A /\ Γ M !s : B) \/
 (exists U, exists V, Γ M Π(U),V : A /\ Γ M Π(U),V : B).

Lemma peq_not_Pi_sort : forall Γ A B S, ~(Γ Π(A),B ≡' !S).

First step to prove the annotation valid: we need to find a path between two different annotated version of a same "stripped" term. We don't care that A is not equal to B here, since this results will mainly be used for types, so both A and B will be sorts, which is enough to build an equality.
This is the main point of proving annotations valid, and we need the full power of confluence and type exchange to be able to prove it.

Lemma ErasedTermConfluence : forall M N Γ M' A N' B, strip M = strip N -> Γ M M' : A -> Γ N N' : B ->
  exists P, Γ M ▹▹ P : A /\ Γ N ▹▹ P : B.
Phase 1 : Pi C D == Pi C' E
1 / 4
2 / 4
3 / 4
4 / 4
Phase 2 : RP -> λ
1 / 4
2 / 4
3 / 4
4 / 4
impossible cases

Next step: if there is a path for any term, there is path for types, so two version of a same "stripped" types are equivalent in PTS{atr}.
Lemma ErasedTypeConversion : forall A B Γ A' s B' t, strip A = strip B -> Γ A A' : !s -> Γ B B' : !t ->
  Γ A ≡' B.

And if it's true for types, its true for list of types, so for context.
Lemma L43_ : forall Γ Γ', strip_env Γ = strip_env Γ' -> wf Γ -> wf Γ' -> env_conv Γ Γ'.

Now that we know that two versions of a "stripped" context are equivalent, we can chose to use both version to build our judgment. This well be usefull to glue together the intermediate steps of the annotations process.
Lemma ErasedContextSwitch : (forall Γ M N T, Γ M N : T -> forall Γ', wf Γ' -> strip_env Γ = strip_env Γ' -> Γ' M N : T) /\
  (forall Γ M N T, Γ M ▹▹ N : T -> forall Γ', wf Γ' -> strip_env Γ = strip_env Γ' -> Γ' M ▹▹ N : T) /\
  (forall Γ, Γ -> True).

Some property of the stripping process and reduction .
Lemma L33 : forall M N', URM.Beta (strip M) N' ->exists N, strip N = N' /\ Beta M N.

Lemma L33' : forall M N', URM.Betas (strip M) N' ->exists N, strip N = N' /\ Betas M N.

End glue_mod.