Library CoC_Preservation

Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_Conversion.

Inversion Lemmas for Subtyping


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).

Inversion Lemmas for Typing


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.

Subtyping preserved by Substitution


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).