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.