Library ut_strengh
Strenghthening
The Strenghthening property is about getting rid of useless hypothesis: if Γ(x:A)Γ' ⊢ M : T and x does not appear in M or T, then ΓΓ' ⊢ M : T.
This is true for all PTS, but the proof is quite subtle. This formalization
has been done from a paper for Jutting in 1993.
The following is not usefull for the proof PTS <-> PTSe but it's still an interesting part of the metatheory of PTSs
The following is not usefull for the proof PTS <-> PTSe but it's still an interesting part of the metatheory of PTSs
Require Import base.
Require Import ut_term.
Require Import ut_red.
Require Import ut_env.
Require Import ut_typ.
Require Import ut_sr.
Require Import List Le Lt Gt.
Module ut_strengh_mod (X:term_sig) (Y:pts_sig X) (TM:ut_term_mod X) (EM:ut_env_mod X TM) (RM: ut_red_mod X TM).
Include (ut_sr_mod X Y TM EM RM).
Import X Y TM EM RM.
Open Scope UT_scope.
Require Import ut_term.
Require Import ut_red.
Require Import ut_env.
Require Import ut_typ.
Require Import ut_sr.
Require Import List Le Lt Gt.
Module ut_strengh_mod (X:term_sig) (Y:pts_sig X) (TM:ut_term_mod X) (EM:ut_env_mod X TM) (RM: ut_red_mod X TM).
Include (ut_sr_mod X Y TM EM RM).
Import X Y TM EM RM.
Open Scope UT_scope.
Tv Ts and Sigma are notation find in Jutting93
We do a partition of Term in two families, one build around vars and the other around sorts and Pi-types.
We do a partition of Term in two families, one build around vars and the other around sorts and Pi-types.
Inductive Tv : Term -> Prop :=
| Tv_intro : forall x, Tv #x
| Tv_la: forall M A, Tv M -> Tv (λ[A],M)
| Tv_app :forall M N, Tv M -> Tv (M·N)
.
Inductive Ts : Term -> Prop :=
| Ts_intro : forall s, Ts !s
| Ts_pi : forall A B, Ts (Π(A),B)
| Ts_la : forall A M, Ts M -> Ts (λ[A],M)
| Ts_app : forall M N, Ts M -> Ts (M·N)
.
| Tv_intro : forall x, Tv #x
| Tv_la: forall M A, Tv M -> Tv (λ[A],M)
| Tv_app :forall M N, Tv M -> Tv (M·N)
.
Inductive Ts : Term -> Prop :=
| Ts_intro : forall s, Ts !s
| Ts_pi : forall A B, Ts (Π(A),B)
| Ts_la : forall A M, Ts M -> Ts (λ[A],M)
| Ts_app : forall M N, Ts M -> Ts (M·N)
.
Telescopes are just a way to talk about n-ary Lam/Pi -terms:
Tels (A1,...,An)M ::= Π(A1),...,Π(An),M
Fixpoint Tels (Γ : Env) (M : Term) {struct Γ } : Term :=
match Γ with
| nil => M
| cons A Δ => Π(A),(Tels Δ M)
end.
Fixpoint Tels' (Γ : Env) (M : Term) {struct Γ } : Term :=
match Γ with
| nil => M
| cons A Δ => λ[A],(Tels' Δ M)
end.
Hint Constructors Tv Ts.
Require Import Compare_dec Peano_dec.
match Γ with
| nil => M
| cons A Δ => Π(A),(Tels Δ M)
end.
Fixpoint Tels' (Γ : Env) (M : Term) {struct Γ } : Term :=
match Γ with
| nil => M
| cons A Δ => λ[A],(Tels' Δ M)
end.
Hint Constructors Tv Ts.
Require Import Compare_dec Peano_dec.
Some basic properties of Tv and Ts.
Lemma Tv_lift : forall M n m, Tv M <-> Tv (M ↑ n # m).
Lemma Ts_lift : forall M n m, Ts M <-> Ts (M ↑ n # m).
Lemma Tx_ok : forall t, Tv t \/ Ts t.
Lemma fun_item_lift : forall A A' v Γ , A ↓ v ⊂ Γ -> A' ↓ v ⊂ Γ -> A = A'.
Lemma Ts_lift : forall M n m, Ts M <-> Ts (M ↑ n # m).
Lemma Tx_ok : forall t, Tv t \/ Ts t.
Lemma fun_item_lift : forall A A' v Γ , A ↓ v ⊂ Γ -> A' ↓ v ⊂ Γ -> A = A'.
First result: if a term is in Tv, then all of his types are convertible.
Some properties over Tels (reduction, substitutions, ...).
Lemma Beta_Tels_inv : forall Γ M N, Tels Γ M → N -> (exists Γ', N = Tels Γ' M /\ Γ →e Γ') \/
(exists M', N = Tels Γ M' /\ M → M').
Lemma Betas_Tels_inv : forall Γ M N, Tels Γ M →→ N -> exists Γ', exists M', N = Tels Γ' M' /\ Γ →→e Γ' /\ M →→ M'.
Lemma Betas_Tels : forall Γ Γ' M M', Γ →→e Γ' -> M →→ M' -> Tels Γ M →→ Tels Γ' M'.
Lemma Betas_not_Pi_to_Sort : forall A B s, ~ (Π (A), B →→ !s).
Fixpoint env_subst Γ n N {struct Γ} := match Γ with
| nil => nil
| A::Γ' => (A[n ← N]) :: (env_subst Γ' (S n) N)
end.
Notation "E [[ n ← N ]]" := (env_subst E n N) (at level 80).
Lemma Tels_subst : forall Γ M n N, (Tels Γ M) [n ← N] = Tels (Γ [[n ← N]]) (M [(length Γ + n) ← N]).
Lemma Tels'_subst : forall Γ M n N, (Tels' Γ M) [n ← N] = Tels' (Γ [[n ← N]]) (M [(length Γ + n) ← N]).
(exists M', N = Tels Γ M' /\ M → M').
Lemma Betas_Tels_inv : forall Γ M N, Tels Γ M →→ N -> exists Γ', exists M', N = Tels Γ' M' /\ Γ →→e Γ' /\ M →→ M'.
Lemma Betas_Tels : forall Γ Γ' M M', Γ →→e Γ' -> M →→ M' -> Tels Γ M →→ Tels Γ' M'.
Lemma Betas_not_Pi_to_Sort : forall A B s, ~ (Π (A), B →→ !s).
Fixpoint env_subst Γ n N {struct Γ} := match Γ with
| nil => nil
| A::Γ' => (A[n ← N]) :: (env_subst Γ' (S n) N)
end.
Notation "E [[ n ← N ]]" := (env_subst E n N) (at level 80).
Lemma Tels_subst : forall Γ M n N, (Tels Γ M) [n ← N] = Tels (Γ [[n ← N]]) (M [(length Γ + n) ← N]).
Lemma Tels'_subst : forall Γ M n N, (Tels' Γ M) [n ← N] = Tels' (Γ [[n ← N]]) (M [(length Γ + n) ← N]).
Second Results: if a term is in Ts, then all of its types are almost
convertible: they all reduce to a telescope that ends with a sort,
and the body of the telescope is the same for everyone (but not the final
sort.
Theorem Shape_of_Type_Ts : forall Γ M T, Γ ⊢ M : T -> forall T', Γ ⊢ M : T' -> Ts M ->
exists s, exists s', exists Γ, T →→ (Tels Γ !s) /\ T' →→ (Tels Γ !s').
exists s, exists s', exists Γ, T →→ (Tels Γ !s) /\ T' →→ (Tels Γ !s').
Definition of the set Sigma for terms in Ts. It's almost the set
of all possible sorts that may appear at the end of the telescope, but
that not totally true, just a hint.
Inductive Sigma : Env -> Term -> Sorts -> Prop :=
| Sigma_sorts : forall Γ s s', Ax s s' -> Sigma Γ !s s'
| Sigma_pi : forall Γ A B s t u, Rel s t u ->
( Tv A -> Γ ⊢ A : !s) -> (Ts A -> Sigma Γ A s) ->
( Tv B -> A::Γ ⊢ B : !t) -> (Ts B -> Sigma (A::Γ) B t) -> Sigma Γ (Π(A),B) u
| Sigma_la : forall Γ A M s, Sigma (A::Γ) M s -> Sigma Γ (λ[A],M) s
| Sigma_app : forall Γ M N s, Sigma Γ M s -> Sigma Γ (M· N) s.
Hint Constructors Sigma.
| Sigma_sorts : forall Γ s s', Ax s s' -> Sigma Γ !s s'
| Sigma_pi : forall Γ A B s t u, Rel s t u ->
( Tv A -> Γ ⊢ A : !s) -> (Ts A -> Sigma Γ A s) ->
( Tv B -> A::Γ ⊢ B : !t) -> (Ts B -> Sigma (A::Γ) B t) -> Sigma Γ (Π(A),B) u
| Sigma_la : forall Γ A M s, Sigma (A::Γ) M s -> Sigma Γ (λ[A],M) s
| Sigma_app : forall Γ M N s, Sigma Γ M s -> Sigma Γ (M· N) s.
Hint Constructors Sigma.
Some handy functions.
Lemma Tels_tool : forall Γ Γ' s t, Tels Γ !s →→ Tels Γ' !t -> s = t /\ length Γ = length Γ'.
Lemma ins_in_env_Sigma : forall a T Δ A n Γ Γ' sa, Γ ⊢ a : T -> Δ ⊢ A : !sa -> Ts a -> ins_in_env Δ A n Γ Γ' ->
forall s , Sigma Γ a s <-> Sigma Γ' (a↑1#n) s.
Lemma In_Sigma_tool : forall Γ a A, Γ ⊢ a : A -> forall Δ s, Ts a -> A →→ Tels Δ !s -> Sigma Γ a s.
Lemma In_Sigma : forall Γ A s, Γ ⊢ A : !s -> Ts A -> Sigma Γ A s.
Lemma env_subst_tool : forall Γ n M, length (Γ[[n ← M]]) = length Γ.
Fixpoint env_subst_down Γ N n {struct Γ } := match Γ with
| nil => nil
| A::Γ' => (A[length Γ' + n ← N]) :: (env_subst_down Γ' N n)
end.
Lemma env_subst_down_app :forall Γ Γ' t n, env_subst_down (Γ++Γ') t n = (env_subst_down Γ t (length Γ' + n))++(env_subst_down Γ' t n).
Lemma env_subst_down_rev : forall Θ t n, rev (Θ [[n ← t]]) = env_subst_down (rev Θ) t n.
Lemma env_subst_down_sub_in_env : forall Θ Γ t A, sub_in_env Γ t A (length Θ) (Θ ++ A :: Γ) (env_subst_down Θ t 0 ++ Γ).
Lemma sub_in_env_rev_append : forall Θ Γ t A , sub_in_env Γ t A (length Θ) (rev (A :: Θ) ++ Γ) (rev (Θ [[0 ←t]]) ++ Γ).
Lemma Betas_env_length : forall Γ Γ', Γ →→e Γ' -> length Γ = length Γ'.
Lemma ins_in_env_Sigma : forall a T Δ A n Γ Γ' sa, Γ ⊢ a : T -> Δ ⊢ A : !sa -> Ts a -> ins_in_env Δ A n Γ Γ' ->
forall s , Sigma Γ a s <-> Sigma Γ' (a↑1#n) s.
Lemma In_Sigma_tool : forall Γ a A, Γ ⊢ a : A -> forall Δ s, Ts a -> A →→ Tels Δ !s -> Sigma Γ a s.
Lemma In_Sigma : forall Γ A s, Γ ⊢ A : !s -> Ts A -> Sigma Γ A s.
Lemma env_subst_tool : forall Γ n M, length (Γ[[n ← M]]) = length Γ.
Fixpoint env_subst_down Γ N n {struct Γ } := match Γ with
| nil => nil
| A::Γ' => (A[length Γ' + n ← N]) :: (env_subst_down Γ' N n)
end.
Lemma env_subst_down_app :forall Γ Γ' t n, env_subst_down (Γ++Γ') t n = (env_subst_down Γ t (length Γ' + n))++(env_subst_down Γ' t n).
Lemma env_subst_down_rev : forall Θ t n, rev (Θ [[n ← t]]) = env_subst_down (rev Θ) t n.
Lemma env_subst_down_sub_in_env : forall Θ Γ t A, sub_in_env Γ t A (length Θ) (Θ ++ A :: Γ) (env_subst_down Θ t 0 ++ Γ).
Lemma sub_in_env_rev_append : forall Θ Γ t A , sub_in_env Γ t A (length Θ) (rev (A :: Θ) ++ Γ) (rev (Θ [[0 ←t]]) ++ Γ).
Lemma Betas_env_length : forall Γ Γ', Γ →→e Γ' -> length Γ = length Γ'.
Terms in Ts have a particular shape: they are build around sorts and
pi-types, two families of terms that cannot be type by a pi-type. Hence, if an
application is in Ts, it will reduce to some lambda-telescope whose head
is a sort or a pi-team.
(we don't talk of weak head normal form since not all PTS are normalizing
and we still want to be fully general.
Lemma Shape_of_Ts_Term : forall Γ a A, Γ ⊢ a : A -> forall Δ s s1, Ts a -> A →→ Tels Δ !s1 -> Sigma Γ a s ->
exists Δ', exists a1, length Δ = length Δ' /\ a →→ Tels' Δ' a1 /\ rev Δ'++Γ ⊢ a1 : !s.
Lemma Ts_Sigma_Shape : forall Γ A s, Γ ⊢ A : !s -> forall s', Ts A -> Sigma Γ A s' -> exists A', A →→ A' /\ Γ ⊢ A' : !s'.
exists Δ', exists a1, length Δ = length Δ' /\ a →→ Tels' Δ' a1 /\ rev Δ'++Γ ⊢ a1 : !s.
Lemma Ts_Sigma_Shape : forall Γ A s, Γ ⊢ A : !s -> forall s', Ts A -> Sigma Γ A s' -> exists A', A →→ A' /\ Γ ⊢ A' : !s'.
To prove strenghthening, we will first prove that if the hypothesis is not
used in the term, we can safely remove it, but we may need to beta reduce the
term in order to be still valid.
Theorem WeakStrenghthening : (forall Γ' M T, Γ' ⊢ M : T -> forall m n Δ A Γ, M = m ↑ 1 # n ->
ins_in_env Δ A n Γ Γ' -> exists T', T →→ T'↑ 1 # n /\ Γ ⊢ m : T' ) /\
(forall Γ', Γ' ⊣ -> forall n Δ A Γ, ins_in_env Δ A n Γ Γ' -> Γ ⊣).
ins_in_env Δ A n Γ Γ' -> exists T', T →→ T'↑ 1 # n /\ Γ ⊢ m : T' ) /\
(forall Γ', Γ' ⊣ -> forall n Δ A Γ, ins_in_env Δ A n Γ Γ' -> Γ ⊣).
With the previous lemma and Type Correctness, we can prove the full lemma:
if an hypothesis is not used in the term and it's type, we can simply remove
it.
Theorem Strenghthening: forall Γ' M n T, Γ' ⊢ M ↑ 1 # n: T ↑ 1 # n -> forall Δ A Γ, ins_in_env Δ A n Γ Γ' ->
Γ ⊢ M : T.
End ut_strengh_mod.
Γ ⊢ M : T.
End ut_strengh_mod.