Library BoundCompliantSubstitutions_proofs
Require Import List.
Require Import Arith.
Require Import Wf_nat.
Require Import MatchCompNat.
Require Import Util.
Require Syntax.
Module SetProgram(My_Program: Syntax.Program).
Import My_Program.
Require Progress_proofs.
Module My_Progress_proofs := Progress_proofs.SetProgram(My_Program).
Import My_Progress_proofs.
Import My_TransitivityElimination_proofs.
Import My_Normalization_proofs.
Import My_Subtyping_proofs.
Import My_Typing_proofs.
Import My_Confluence.
Import My_Auxiliary_proofs.
Import My_Substitutions_proofs.
Import My_Binders_proofs.
Import My_Semantics.
Import My_WellFormedness.
Import My_Typing.
Import My_Auxiliary.
Import My_Substitutions.
Import My_Binders.
Lemma Lifting_preserves_removeBounds:
forall (t t': TypeS) (k n: nat),
(removeBounds t t') ->
(removeBounds (lift_at_depth_in_type t n k) t')
.
Lemma removeBounds_invariant_by_lifting:
forall (t t': TypeS) (k n: nat),
(removeBounds t t') ->
(lift_at_depth_in_type t' n k) = t'
.
Lemma lift_of_some_inversion:
forall (t N: TypeS) (n k: nat),
(lift_at_depth_in_type t n k) = (Type_some N) ->
exists N0: TypeS,
t = (Type_some N0) /\
N = (lift_at_depth_in_type N0 n k)
.
Lemma lift_of_cons_inversion:
forall (t u us: TypeS) (n k: nat),
(lift_at_depth_in_type t n k) = (Type_cons u us) ->
exists u0: TypeS, exists us0: TypeS,
t = (Type_cons u0 us0) /\
u = (lift_at_depth_in_type u0 n k) /\
us = (lift_at_depth_in_type us0 n k)
.
Lemma TypeS_at_of_lift_inversion:
forall (t u: TypeS) (i n k: nat),
(TypeS_at (lift_at_depth_in_type t n k) i u) ->
exists u0: TypeS,
(TypeS_at t i u0) /\
u = (lift_at_depth_in_type u0 n k)
.
Lemma Weakening_of_param_satisfaction:
forall (D1 D2 D3: TypeEnv) (K P: TypeS),
(ParamSat (D1 ++ D3) K P) ->
(ParamSat (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
(lift_at_depth_in_type K (length D2) (length D3))
(lift_at_depth_in_type P (length D2) (length D3)))
.
Lemma Weakening_of_satisfaction:
forall (D1 D2 D3: TypeEnv) (R Pi: TypeS),
(SectionSat (D1 ++ D3) R Pi) ->
(SectionSat (D1 ++ D2 ++ (lift_in_typeEnv D3 (length D2)))
(lift_at_depth_in_type R (length D2) (length D3))
(lift_at_depth_in_type Pi (length D2) (length D3)))
.
Lemma Weakening_of_satisfaction_by_the_right:
forall (D D': TypeEnv) (R Pi: TypeS),
(SectionSat D R Pi) ->
(SectionSat (D ++ D')
(lift_in_type R (length D'))
(lift_in_type Pi (length D')))
.
Fixpoint size_of_kind (k: KindS): nat :=
match k with
| (Kind_tuple k1) => (size_of_kind k1) + 1
| (Kind_constr k1) => (size_of_kind k1) + 1
| Kind_nil => 0
| (Kind_cons k1 k2) => (size_of_kind k1) + (size_of_kind k2) + 1
end
.
Lemma typeSubst_of_class_type:
forall (C: ClassSym) (R R': TypeS) (n: nat),
(typeSubst_in_type (Class_type C R) n R') =
(Class_type C (typeSubst_in_type R n R'))
.
Lemma Substitution_in_closed_type_aux:
forall (D: TypeEnv) (t R: TypeS) (c: TypeC) (k: nat),
(Type_WK D t c) ->
(typeSubst_in_type t ((length D) + k) R) = t
.
Lemma removeBounds_is_idempotent:
forall (t t': TypeS),
(removeBounds t t') ->
(removeBounds t' t')
.
Lemma removeBounds_preserves_kind_of:
forall (t t': TypeS) (k: KindS),
(kind_of t k) ->
(removeBounds t t') ->
(kind_of t' k)
.
Lemma Substitution_preserves_removeBounds:
forall (t t' R: TypeS) (k: nat),
(removeBounds t t') ->
(removeBounds (typeSubst_in_type t k R) t')
.
Lemma removeBounds_then_substitution:
forall (t t' R: TypeS) (k: nat),
(removeBounds t t') ->
(typeSubst_in_type t' k R) = t'
.
Lemma removeBounds_invariant_by_substitution:
forall (t t' R: TypeS) (k: nat),
(removeBounds t t') ->
(typeSubst_in_type t' k R) = t'
.
Lemma TypeParamList_ind:
forall (D: TypeEnv) (Q: TypeS -> Prop),
(Q Type_nil) ->
(forall (P Ps: TypeS),
(Type_WK D P TypeParam) ->
(Type_WK D Ps TypeParamList) ->
(Q Ps) ->
(Q (Type_cons P Ps))
) ->
forall (Ps: TypeS),
(Type_WK D Ps TypeParamList) ->
(Q Ps)
.
Lemma kind_of_params_inversion:
forall (Ps P: TypeS) (k ks: KindS) (i: nat),
(kind_of Ps ks) ->
(TypeS_at Ps i P) ->
(KindS_at ks i k) ->
(kind_of P k)
.
Lemma kind_of_params_inversion_variant1:
forall (Ps P: TypeS) (ks: KindS) (i: nat),
(kind_of Ps ks) ->
(TypeS_at Ps i P) ->
exists k: KindS,
(KindS_at ks i k) /\
(kind_of P k)
.
Lemma removeBounds_of_params_inversion:
forall (Ps Ps' P': TypeS) (i: nat),
(removeBounds Ps Ps') ->
(TypeS_at Ps' i P') ->
exists P: TypeS,
(TypeS_at Ps i P) /\
(removeBounds P P')
.
Lemma removeBounds_and_kind_of_inversion:
forall (t t': TypeS) (k: KindS),
(removeBounds t t') ->
(kind_of t' k) ->
(kind_of t k)
.
Lemma kind_equality_implies_param_satisfaction:
forall (D: TypeEnv) (K P P' Pi N_opt: TypeS) (k: KindS),
P = (Type_param Pi N_opt) ->
(Type_WK D K (TypeConstr k)) ->
(removeBounds P P') ->
(kind_of P k) ->
(ParamSat D K P')
.
Theorem kind_equality_implies_poly_satisfaction:
forall (D: TypeEnv) (R Pi Pi': TypeS) (k: KindS),
(Type_WK D R (TypeTuple k)) ->
(Type_WK D Pi TypeSection) ->
(kind_of Pi k) ->
(removeBounds Pi Pi') ->
(SectionSat D R Pi')
.
Lemma TypeEnv_WK_inversion:
forall (D: TypeEnv) (i: nat) (Pi: TypeS),
(TypeEnv_WK D) ->
(TypeSection_at D i Pi) ->
(Type_WK D (lift_in_type Pi (S i)) TypeSection)
.
Lemma TypeEnv_WK_inversion_cor1:
forall (D: TypeEnv) (X: TypeVar) (Pi: TypeS),
(TypeEnv_WK D) ->
(decl_of_typeVar D X Pi) ->
(Type_WK D Pi TypeSection)
.
Lemma Var_expansion_preserves_well_kindedness_aux:
forall (Ps Pi N_opt: TypeS) (i: nat) (k ks: KindS),
(TypeS_at Ps i (Type_param Pi N_opt)) ->
(kind_of Ps ks) ->
(KindS_at ks i (Kind_constr k)) ->
(kind_of Pi k)
.
Theorem Var_expansion_preserves_well_kindedness:
forall (D: TypeEnv) (X: TypeVar) (R Ps Pi N: TypeS) (i: nat),
(TypeEnv_WK D) ->
(decl_of_typeVar D X (Type_section Ps)) ->
(TypeS_at (typeSubst_in_type Ps 0 (Type_var X)) i (Type_param Pi (Type_some N))) ->
(Type_WK D (Var_type X i R) Type_) ->
(Type_WK D (typeSubst_in_type N 0 R) Type_)
.
Lemma TypeEnv_WK_inversion_cor2:
forall (D1 D2: TypeEnv) (Pi: TypeS),
(TypeEnv_WK (D1 ++ (Pi :: D2))) ->
(Type_WK D1 Pi TypeSection)
.
Lemma KindS_at_and_size:
forall (k ks: KindS) (i: nat),
(KindS_at ks i k) ->
(size_of_kind k) < (size_of_kind ks)
.
Lemma Substitution_in_well_kinded_type_env:
forall (D1 D2: TypeEnv) (Pi R: TypeS) (k: KindS),
(TypeEnv_WK (D1 ++ Pi :: D2)) ->
(Type_WK D1 R (TypeTuple k)) ->
(kind_of Pi k) ->
(TypeEnv_WK (D1 ++ (typeSubst_in_typeEnv D2 0 R)))
.
Lemma removeBounds_preserves_well_kindedness:
forall (D: TypeEnv) (t t': TypeS) (c: TypeC),
(Type_WK D t c) ->
(removeBounds t t') ->
forall (D': TypeEnv),
(Type_WK D' t' c)
.
Lemma Type_substitution_preserves_subtyping_aux1:
forall (D1 D2: TypeEnv) (R Pi': TypeS) (i: nat) (k0 k1: KindS),
(Type_WK D1 R (TypeTuple (Kind_tuple k1))) ->
(KindS_at k1 i (Kind_constr k0)) ->
(kind_of Pi' k0) ->
(Type_WK (snoc (D1 ++ typeSubst_in_typeEnv D2 0 R) Pi')
(Type_apply (lift_in_type (Type_proj (lift_in_type R (length D2)) i) 1)
(Type_var 0)) Type_)
.
Theorem Type_substitution_preserves_subtyping:
forall (D1 D2: TypeEnv) (Pi R T U: TypeS) (k: KindS),
(Type_WK D1 R (TypeTuple k)) ->
(SectionSat D1 R Pi) ->
(TypeEnv_WK (D1 ++ (Pi :: D2))) ->
(Subtyping (D1 ++ (Pi :: D2)) T U) ->
(Type_WK (D1 ++ (Pi :: D2)) T Type_) ->
(Type_WK (D1 ++ (Pi :: D2)) U Type_) ->
(Subtyping (D1 ++ (typeSubst_in_typeEnv D2 0 R))
(typeSubst_in_type T (length D2) R)
(typeSubst_in_type U (length D2) R))
.
Theorem Type_substitution_preserves_subtyping_snoc:
forall (D1: TypeEnv) (Pi R T U: TypeS) (k: KindS),
(Type_WK D1 R (TypeTuple k)) ->
(SectionSat D1 R Pi) ->
(TypeEnv_WK (snoc D1 Pi)) ->
(Subtyping (snoc D1 Pi) T U) ->
(Type_WK (snoc D1 Pi) T Type_) ->
(Type_WK (snoc D1 Pi) U Type_) ->
(Subtyping D1 (typeSubst_in_type T 0 R) (typeSubst_in_type U 0 R))
.
Lemma Type_substitution_preserves_subtyping_cor1:
forall (Pi1 Pi2 R T U: TypeS) (k: KindS),
(Type_WK nil R (TypeTuple k)) ->
(SectionSat nil R Pi1) ->
let D := (Pi1 :: Pi2 :: nil) in
(TypeEnv_WK D) ->
(Type_WK D T Type_) ->
(Type_WK D U Type_) ->
(Subtyping D T U) ->
(Subtyping ((typeSubst_in_type Pi2 0 R) :: nil)
(typeSubst_in_type T 1 R)
(typeSubst_in_type U 1 R))
.
Lemma Type_substitution_preserves_subtyping_cor2:
forall (Pi R T U: TypeS) (k: KindS),
(Type_WK nil R (TypeTuple k)) ->
(SectionSat nil R Pi) ->
let D := (Pi :: nil) in
(TypeEnv_WK D) ->
(Type_WK D T Type_) ->
(Type_WK D U Type_) ->
(Subtyping D T U) ->
(Subtyping nil
(typeSubst_in_type T 0 R)
(typeSubst_in_type U 0 R))
.
Lemma typeSubst_of_some_inversion:
forall (D: TypeEnv) (t N R: TypeS) (k: nat),
(Type_WK D t TypeOption) ->
(typeSubst_in_type t k R) = (Type_some N) ->
exists N0: TypeS,
t = (Type_some N0) /\
N = (typeSubst_in_type N0 k R)
.
Lemma typeSubst_of_cons_inversion:
forall (D: TypeEnv) (t u us R: TypeS) (k: nat),
(Type_WK D t TypeParamList) ->
(typeSubst_in_type t k R) = (Type_cons u us) ->
exists u0: TypeS, exists us0: TypeS,
t = (Type_cons u0 us0) /\
u = (typeSubst_in_type u0 k R) /\
us = (typeSubst_in_type us0 k R)
.
Lemma TypeS_at_of_typeSubst_inversion:
forall (D: TypeEnv) (t u R: TypeS) (i k: nat),
(Type_WK D t TypeParamList) ->
(TypeS_at (typeSubst_in_type t k R) i u) ->
exists u0: TypeS,
(TypeS_at t i u0) /\
u = (typeSubst_in_type u0 k R)
.
Lemma Type_substitution_preserves_param_satisfaction:
forall (D1 D2: TypeEnv) (Pi R K P: TypeS) (k k': KindS),
let D := (D1 ++ (Pi :: D2)) in
(Type_WK D1 R (TypeTuple k)) ->
(SectionSat D1 R Pi) ->
(TypeEnv_WK D) ->
(ParamSat D K P) ->
(Type_WK D K (TypeConstr k')) ->
(Type_WK D P TypeParam) ->
(kind_of P k') ->
(ParamSat (D1 ++ (typeSubst_in_typeEnv D2 0 R))
(typeSubst_in_type K (length D2) R)
(typeSubst_in_type P (length D2) R))
.
Theorem Type_substitution_preserves_satisfaction:
forall (D1 D2: TypeEnv) (Pi R R' Pi': TypeS) (k: KindS),
let D := (D1 ++ (Pi :: D2)) in
(Type_WK D1 R (TypeTuple k)) ->
(SectionSat D1 R Pi) ->
(TypeEnv_WK D) ->
(SectionSat D R' Pi') ->
(Type_WK D Pi' TypeSection) ->
(SectionSat (D1 ++ (typeSubst_in_typeEnv D2 0 R))
(typeSubst_in_type R' (length D2) R)
(typeSubst_in_type Pi' (length D2) R))
.
Theorem Type_substitution_preserves_satisfaction_snoc:
forall (D1: TypeEnv) (Pi R R' Pi': TypeS) (k: KindS),
let D := (snoc D1 Pi) in
(Type_WK D1 R (TypeTuple k)) ->
(SectionSat D1 R Pi) ->
(TypeEnv_WK D) ->
(SectionSat D R' Pi') ->
(Type_WK D Pi' TypeSection) ->
(SectionSat D1 (typeSubst_in_type R' 0 R) (typeSubst_in_type Pi' 0 R))
.
End SetProgram.