```(*************************************************************************** * Calculus of Constructions - Properties of Conversion * * Arthur Charguéraud, April 2007, Coq v8.1 * ***************************************************************************) Set Implicit Arguments. Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_BetaStar CoC_ChurchRosser. (* ********************************************************************** *) (** ** Some Properties of Conversion *) Lemma conv_red_out : red_out conv. Proof. introz. puts beta_red_out. induction* H0. Qed. Lemma conv_from_beta_star : (beta star) simulated_by (conv). Proof. introz. induction* H. Qed. Lemma conv_from_beta_star_trans : forall T U1 U2, (beta star) U1 T -> (beta star) U2 T -> conv U1 U2. Proof. introv R1 R2. apply (@equiv_trans beta T). apply* conv_from_beta_star. apply equiv_sym. apply* conv_from_beta_star. Qed. Lemma conv_from_open_beta : forall u u' t, body t -> beta u u' -> conv (t ^^ u') (t ^^ u). Proof. introv B R. destruct B as [L Fr]. pick_fresh x. rewrite* (@subst_intro x t u). rewrite* (@subst_intro x t u'). unfold conv. apply equiv_sym. apply conv_from_beta_star. apply* beta_star_red_in. Qed. (* ********************************************************************** *) (** ** 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). Proof. introv H. gen_eq (trm_prod U1 T1) as Q. gen U1 T1. induction H; intros; subst. inversions H. helper*. destructi~ (IHstar_1 U1 T1) as [U3 [T3 [EQ3 [H3 [L3 R3]]]]]. subst. destructi~ (IHstar_2 U3 T3) as [U2 [T2 [EQ2 [H2 [L2 R2]]]]]. subst. helper*. inversions H; helper*. Qed. End ProdInv. Lemma beta_star_type_any_inv : forall P i, (beta star) (trm_type i) P -> P = trm_type i. Proof. introv R. gen_eq (trm_type i) as T. induction R; intros EQ; subst. auto. destructi* IHR1. subst. auto. inversion H. Qed. 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). Proof. unfold conv. introv C. destruct (church_rosser_beta C) as [P3 [Red1 Red2]]. destruct (beta_star_prod_any_inv Red1) as [P3_11 [P3_12 [EQ1 [R1 [L1 S1]]]]]. destruct (beta_star_prod_any_inv Red2) as [P3_21 [P3_22 [EQ2 [R2 [L2 S2]]]]]. subst. inversions EQ2. split. apply* conv_from_beta_star_trans. exists_fresh. intros x Fr. forward~ (S1 x) as K1. forward~ (S2 x) as K2. apply* conv_from_beta_star_trans. Qed. Lemma conv_type_type_inv : forall i j, conv (trm_type i) (trm_type j) -> i = j. Proof. unfold conv. introv C. destruct (church_rosser_beta C) as [T [Red1 Red2]]. rewrite (beta_star_type_any_inv Red1) in Red2. poses K (beta_star_type_any_inv Red2). inversions* K. Qed. Lemma conv_type_prod_inv : forall U1 U2 i, conv (trm_type i) (trm_prod U1 U2) -> False. Proof. unfold conv. introv C. destruct (church_rosser_beta C) as [P3 [Red1 Red2]]. destruct (beta_star_prod_any_inv Red2) as [P3_11 [P3_12 [EQ1 [R1 [L1 S1]]]]]. rewrite (beta_star_type_any_inv Red1) in *. contradictions. Qed. ```