Library CoC_Preservation
Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_Conversion.
Lemma less_type_any_inv : forall T1 T2,
less T1 T2 -> forall i1, conv T1 (trm_type i1) ->
exists i2, i1 <= i2 /\ conv T2 (trm_type i2).
Lemma less_type_type_inv : forall i j,
less (trm_type i) (trm_type j) -> i <= j.
Lemma less_prod_any_inv : forall P1 P2,
less P1 P2 -> forall U1 T1, conv P1 (trm_prod U1 T1) ->
exists U2, exists T2, conv P2 (trm_prod U2 T2)
/\ conv U1 U2
/\ exists L, forall x, x \notin L -> less (T1 ^ x) (T2 ^ x).
Lemma less_prod_prod_inv : forall U1 T1 U2 T2,
less (trm_prod U1 T1) (trm_prod U2 T2) ->
conv U1 U2
/\ exists L, forall x, x \notin L -> less (T1 ^ x) (T2 ^ x).
Lemma typing_prod_inv : forall E U T P,
typing E (trm_prod U T) P -> exists i, exists k,
less (trm_type i) P
/\ typing E U (trm_type k)
/\ (i = k \/ i = 0)
/\ exists L, forall x, x \notin L -> typing (E & x ~ U) (T ^ x) (trm_type i).
Lemma typing_abs_inv : forall E V t P,
typing E (trm_abs V t) P -> exists T, exists i,
typing E (trm_prod V T) (trm_type i)
/\ less (trm_prod V T) P
/\ exists L, forall x, x \notin L -> typing (E & x ~ V) (t ^ x) (T ^ x).
Lemma typing_prod_type_inv : forall E U T i,
typing E (trm_prod U T) (trm_type i) ->
exists L, forall x, x \notin L ->
typing (E & x ~ U) (T ^ x) (trm_type i).
Typing preserved by Weakening
Lemma typing_weaken : forall G E F t T,
typing (E & G) t T ->
wf (E & F & G) ->
typing (E & F & G) t T.
Lemma less_red_out : red_out less.
Typing preserved by Substitution
Lemma typing_substitution : forall V F v E x t T,
typing E v V ->
typing (E & x ~ V & F) t T ->
typing (E & (map (subst x v) F)) (subst x v t) (subst x v T).
Types are Themselves Well-typed
Lemma typing_wf_from_context : forall x U E,
binds x U E ->
wf E ->
exists i, typing E U (trm_type i).
Lemma typing_wf_from_typing : forall E t T,
typing E t T ->
exists i, typing E T (trm_type i).
Typing preserved by Subtyping in Environment
Inductive env_less : env -> env -> Prop :=
| env_less_head : forall E U U' x,
less U U' ->
env_less (E & x ~ U) (E & x ~ U')
| env_less_tail : forall E E' x U,
term U -> env_less E E' -> env_less (E & x ~ U) (E' & x ~ U).
Hint Constructors env_less.
Lemma env_less_binds : forall x U E E',
env_less E' E -> wf E -> wf E' -> binds x U E ->
binds x U E'
\/ exists U', exists i,
binds x U' E' /\ less U' U /\ typing E' U (trm_type i).
Lemma typing_sub_env : forall E E' t T,
typing E t T ->
env_less E' E ->
wf E' ->
typing E' t T.
Subject Reduction - Induction
Lemma subject_reduction_ind : forall E t t' T,
typing E t T -> beta t t' -> typing E t' T.
Subject Reduction - Beta preserves typing
Lemma subject_reduction_result : subject_reduction beta.
Subject Reduction - Beta Star preserves typing
Lemma subject_reduction_star_result :
subject_reduction (beta star).