Library CoC_Conversion

Require Import Metatheory CoC_Definitions CoC_Infrastructure
 CoC_BetaStar CoC_ChurchRosser.

Some Properties of Conversion


Lemma conv_red_out : red_out conv.

Lemma conv_from_beta_star :
  (beta star) simulated_by (conv).

Lemma conv_from_beta_star_trans : forall T U1 U2,
  (beta star) U1 T -> (beta star) U2 T -> conv U1 U2.

Lemma conv_from_open_beta : forall u u' t,
  body t -> beta u u' -> conv (t ^^ u') (t ^^ u).

Inversion Lemmas for Conversion


Section ProdInv.

Tactic Notation "helper" :=
 match goal with |- ex (fun _ => ex (fun _ =>
  trm_prod ?A ?B = trm_prod _ _ /\ _)) =>
  exists A B; split3; [auto | | exists_fresh ] end.

Tactic Notation "helper" "*" := helper; eauto.

Lemma beta_star_prod_any_inv : forall P U1 T1,
  (beta star) (trm_prod U1 T1) P ->
  exists U2, exists T2, P = trm_prod U2 T2 /\
  (beta star) U1 U2 /\
  exists L, forall x, x \notin L ->
   (beta star) (T1 ^ x) (T2 ^ x).

End ProdInv.

Lemma beta_star_type_any_inv : forall P i,
  (beta star) (trm_type i) P -> P = trm_type i.

Lemma conv_prod_prod_inv : forall U1 T1 U2 T2,
  conv (trm_prod U1 T1) (trm_prod U2 T2) ->
     conv U1 U2
  /\ exists L, forall x, x \notin L -> conv (T1 ^ x) (T2 ^ x).

Lemma conv_type_type_inv : forall i j,
  conv (trm_type i) (trm_type j) -> i = j.

Lemma conv_type_prod_inv : forall U1 U2 i,
  conv (trm_type i) (trm_prod U1 U2) -> False.