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.
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).
Γ ⊢ 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.
Γ ⊢ A ≡' B.
And if it's true for types, its true for list of types, so for context.
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).
(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 .