proposition: Lemma int_typ_red1 : forall U V : term, red1 U V -> forall (e : env) (K : term), typ e U K -> forall ip : intP, cls_of_int ip = class_env e -> int_inv ip -> cl_term U (cls_of_int ip) <> Trm -> eq_can (skel_int U ip) (int_typ U ip _) (int_typ V ip _).
proof: Proof. simple induction 1; intros. unfold skel_int in |- *. apply inv_typ_app with e (Abs T M) N K; intros; auto with coc core arith datatypes. elim type_case with e (Abs T M) (Prod V0 Ur); intros; auto with coc core arith datatypes. inversion_clear H7. apply inv_typ_prod with e V0 Ur (Srt x); intros; auto with coc core arith datatypes. apply inv_typ_abs with e T M (Prod V0 Ur); intros; auto with coc core arith datatypes. cut (typ e N T); intros. cut (cl_term M (TCs _ (cl_term T (cls_of_int ip)) (cls_of_int ip)) = Typ (typ_skel (cl_term M (class_env (T :: e))))). cut (int_var_sound N ip (ext_ik T ip _ (int_typ N ip (skel_int N ip)))). simpl in |- *; unfold def_cons, int_cons, ext_ik in |- *; simpl in |- *; rewrite H1. cut (cl_term T (cls_of_int ip) = cl_term T (class_env e)). elim class_sound with e N T (Srt s0); intros; auto with coc core arith datatypes; rewrite H18. simpl in |- *. replace (typ_skel match typ_skel (cl_term M (TCs class (Typ PROP) (class_env e))) with | PROP => Typ (typ_skel (cl_term M (TCs _ (Typ PROP) (class_env e)))) | _ => Typ (typ_skel (cl_term M (TCs _ (Typ PROP) (class_env e)))) end) with (skel_int M (TCs Int_K iT ip)). unfold subst in |- *. apply subst_int_typ with ip iT (T :: e) T0; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. elim H16. elim H1; auto with coc core arith datatypes. red in |- *; intro; apply H3. simpl in |- *. replace (TCs class (cl_term T (cls_of_int ip)) (cls_of_int ip)) with (cls_of_int (TCs Int_K iT ip)). rewrite H19; auto with coc core arith datatypes. unfold cls_of_int at 1 in |- *. simpl in |- *. elim H16; auto with coc core arith datatypes. unfold skel_int in |- *. unfold cls_of_int in |- *. simpl in |- *. elim H1. unfold cls_of_int in |- *. elim (typ_skel (cl_term M (TCs class (Typ PROP) (Tmap Int_K class class_of_ik ip)))); auto with coc core arith datatypes. elim H18. unfold subst in |- *. replace (typ_skel (cl_term M (TCs class (Knd s) (class_env e)))) with (skel_int M (TCs Int_K (iK s (int_typ N ip s)) ip)). apply subst_int_typ with ip (iK s (int_typ N ip s)) (T :: e) T0; auto with coc core arith datatypes. apply ivs_K. generalize H16. rewrite H1. elim class_sound with e N T (Srt s0); auto with coc core arith datatypes; intros. discriminate H19. inversion_clear H19; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. elim H1. rewrite H16; auto with coc core arith datatypes. auto 10 with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. red in |- *; intro; apply H3. simpl in |- *. rewrite H16. unfold cls_of_int in |- *. rewrite H19; auto with coc core arith datatypes. unfold skel_int in |- *. unfold cls_of_int in |- *. simpl in |- *. elim H1; auto with coc core arith datatypes. elim H1; auto with coc core arith datatypes. unfold ext_ik in |- *. unfold skel_int in |- *. generalize (ivs_T N ip) (ivs_K N ip). rewrite H1. elim class_sound with e N T (Srt s0); auto with coc core arith datatypes; intros. generalize H3. simpl in |- *. rewrite H1. replace (TCs class (cl_term T (class_env e)) (class_env e)) with (class_env (T :: e)); auto with coc core arith datatypes. elim class_sound with (T :: e) M T0 (Srt s3); auto with coc core arith datatypes. simple induction 1; auto with coc core arith datatypes. apply type_conv with V0 s0; auto with coc core arith datatypes. apply inv_conv_prod_l with Ur T0; auto with coc core arith datatypes. discriminate H7. apply inv_typ_abs with e M N K; intros; auto with coc core arith datatypes. unfold skel_int in |- *. rewrite H3. simpl in |- *. unfold def_cons in |- *. replace (TCs _ (cl_term M (class_env e)) (class_env e)) with (class_env (M :: e)); auto with coc core arith datatypes. elim class_sound with (M :: e) N T (Srt s2); auto with coc core arith datatypes. simpl in |- *. unfold int_cons in |- *. unfold ext_ik in |- *. rewrite H3. elim class_red with e M M' (Srt s1); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. rewrite H3. elim class_red with e M M' (Srt s1); auto with coc core arith datatypes. cut (cl_term M (cls_of_int ip) = cl_term M (class_env e)). elim (cl_term M (class_env e)); simpl in |- *; intros; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. apply inv_typ_abs with e N M K; intros; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. rewrite H3. replace (TCs _ (cl_term M (class_env e)) (class_env e)) with (class_env (M :: e)); auto with coc core arith datatypes. replace (cl_term M (TCs class (cl_term N (class_env e)) (class_env e))) with (Typ (typ_skel (cl_term M (class_env (N :: e))))). cut (cl_term N (cls_of_int ip) = cl_term N (class_env e)). pattern (cl_term N (class_env e)) in |- *. apply class_typ_ord with s1; intros; auto with coc core arith datatypes. simpl in |- *. replace (typ_skel (cl_term M (TCs class (cl_term N (class_env e)) (class_env e)))) with (skel_int M (def_cons N ip)). apply H1 with (N :: e) T; auto with coc core arith datatypes. unfold def_cons, int_cons, ext_ik in |- *. simpl in |- *. rewrite H3. unfold cls_of_int in |- *. simpl in |- *. pattern (cl_term N (class_env e)) in |- *. apply class_typ_ord with s1; intros; auto with coc core arith datatypes. simpl in |- *. elim skel_sound with e N (Srt s1); simpl in |- *; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. simpl in |- *. elim H3; auto with coc core arith datatypes. unfold def_cons, int_cons, ext_ik in |- *. rewrite H3. pattern (cl_term N (class_env e)) in |- *. apply class_typ_ord with s1; auto with coc core arith datatypes. unfold def_cons in |- *. red in |- *; intro; apply H5. simpl in |- *. replace (TCs class (cl_term N (cls_of_int ip)) (cls_of_int ip)) with (cls_of_int (int_cons N ip (cv_skel (cl_term N (cls_of_int ip))) (default_can (cv_skel (cl_term N (cls_of_int ip)))))). rewrite H11; auto with coc core arith datatypes. replace (TCs class (cl_term N (cls_of_int ip)) (cls_of_int ip)) with (class_env (N :: e)); auto with coc core arith datatypes. rewrite H3. apply int_cons_equal with s1; auto with coc core arith datatypes. rewrite H3; auto with coc core arith datatypes. unfold skel_int in |- *. replace (cls_of_int (def_cons N ip)) with (TCs class (cl_term N (class_env e)) (class_env e)). auto with coc core arith datatypes. symmetry in |- *. unfold def_cons in |- *. replace (TCs class (cl_term N (class_env e)) (class_env e)) with (class_env (N :: e)); auto with coc core arith datatypes. rewrite H3. apply int_cons_equal with s1; auto with coc core arith datatypes. simpl in |- *. intros. replace (typ_skel (cl_term M (TCs class (cl_term N (class_env e)) (class_env e)))) with (skel_int M (TCs Int_K (iK (cv_skel (cl_term N (class_env e))) X2) ip)). apply eq_can_trans with (int_typ M (TCs _ (iK _ X2) ip) (skel_int M (TCs _ (iK _ X2) ip))); auto with coc core arith datatypes. apply H1 with (N :: e) T; auto with coc core arith datatypes. elim int_cons_equal with ip e N s1 X2; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. unfold ext_ik in |- *. rewrite H10; simpl in |- *; auto with coc core arith datatypes. unfold cls_of_int in |- *. simpl in |- *. red in |- *; intros; apply H5. simpl in |- *. rewrite H10. simpl in |- *. unfold cls_of_int in |- *. rewrite H14; auto with coc core arith datatypes. unfold skel_int in |- *. unfold cls_of_int in |- *. simpl in |- *. elim H3. rewrite H10; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. generalize H5. simpl in |- *. rewrite H3. replace (TCs class (cl_term N (class_env e)) (class_env e)) with (class_env (N :: e)); auto with coc core arith datatypes. elim class_sound with (N :: e) M T (Srt s2); simpl in |- *; intros; auto with coc core arith datatypes. elim H10; auto with coc core arith datatypes. apply inv_typ_app with e M1 M2 K; intros; auto with coc core arith datatypes. elim type_case with e M1 (Prod V0 Ur); intros; auto with coc core arith datatypes. inversion_clear H9. apply inv_typ_prod with e V0 Ur (Srt x); intros; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. rewrite H3. elim class_red with e M1 N1 (Prod V0 Ur); auto with coc core arith datatypes. cut (cl_term M1 (class_env e) = Typ (typ_skel (cl_term M1 (class_env e)))). intro. rewrite H13. cut (cl_term M2 (cls_of_int ip) = cl_term M2 (class_env e)). elim class_sound with e M2 V0 (Srt s1); auto with coc core arith datatypes; intros. replace (typ_skel match typ_skel (cl_term M1 (class_env e)) return class with | PROP => Typ (typ_skel (cl_term M1 (class_env e))) | PROD _ _ => Typ (typ_skel (cl_term M1 (class_env e))) end) with (skel_int M1 ip). apply H1 with e (Prod V0 Ur); auto with coc core arith datatypes. red in |- *; intro; apply H5. simpl in |- *. rewrite H15; auto with coc core arith datatypes. unfold skel_int in |- *. elim H3. elim (typ_skel (cl_term M1 (cls_of_int ip))); auto with coc core arith datatypes. generalize (H1 e (Prod V0 Ur) H6 ip H3 H4). replace (skel_int M1 ip) with (PROD s (typ_skel match typ_skel (cl_term M1 (class_env e)) with | PROP => Typ (typ_skel (cl_term M1 (class_env e))) | PROD _ s2 => Typ s2 end)). simpl in |- *; intros. apply H15; auto with coc core arith datatypes. red in |- *; intro; apply H5. simpl in |- *. rewrite H16; auto with coc core arith datatypes. unfold skel_int in |- *. rewrite H3. elim skel_sound with e M1 (Prod V0 Ur); auto with coc core arith datatypes. simpl in |- *. cut (cl_term V0 (class_env e) = Knd s); intros. cut (cl_term Ur (TCs class (cl_term V0 (class_env e)) (class_env e)) = Knd (cv_skel (cl_term Ur (class_env (V0 :: e))))); intros. rewrite H16. rewrite H15; simpl in |- *; auto with coc core arith datatypes. generalize (class_sound e M1 (Prod V0 Ur) H6 (Srt x) H10). simpl in |- *. rewrite H15. rewrite H13. elim (cl_term Ur (TCs class (Knd s) (class_env e))); intros; auto with coc core arith datatypes. inversion_clear H16. inversion_clear H16. generalize H14. rewrite H3. elim class_sound with e M2 V0 (Srt s1); intros; auto with coc core arith datatypes. discriminate H15. inversion_clear H15; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. generalize H5. simpl in |- *. rewrite H3. elim class_sound with e M1 (Prod V0 Ur) (Srt x); intros; auto with coc core arith datatypes. elim H13; auto with coc core arith datatypes. discriminate H9. cut (cl_term M1 (cls_of_int ip) <> Trm); intros. apply inv_typ_app with e M1 M2 K; intros; auto with coc core arith datatypes. elim type_case with e M1 (Prod V0 Ur); intros; auto with coc core arith datatypes. inversion_clear H10. apply inv_typ_prod with e V0 Ur (Srt x); intros; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. rewrite H3. elim class_red with e M2 N2 V0; auto with coc core arith datatypes. cut (cl_term M1 (class_env e) = Typ (typ_skel (cl_term M1 (class_env e)))). intro. rewrite H14. cut (cl_term M2 (cls_of_int ip) = cl_term M2 (class_env e)). elim class_sound with e M2 V0 (Srt s1); auto with coc core arith datatypes; intros. cut (eq_can _ (int_typ M1 ip (PROD s (typ_skel match typ_skel (cl_term M1 (class_env e)) with | PROP => Typ (typ_skel (cl_term M1 (class_env e))) | PROD _ s2 => Typ s2 end))) (int_typ M1 ip (PROD s (typ_skel match typ_skel (cl_term M1 (class_env e)) with | PROP => Typ (typ_skel (cl_term M1 (class_env e))) | PROD _ s2 => Typ s2 end)))). simpl in |- *; intros. apply H16; auto with coc core arith datatypes. replace s with (skel_int M2 ip). apply H1 with e V0; auto with coc core arith datatypes. rewrite H15. discriminate. unfold skel_int in |- *. generalize H15. rewrite H3. elim class_sound with e M2 V0 (Srt s1); intros; auto with coc core arith datatypes. discriminate H17. inversion_clear H17; auto with coc core arith datatypes. auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. generalize H6. rewrite H3. elim class_sound with e M1 (Prod V0 Ur) (Srt x); auto with coc core arith datatypes; intros. elim H14; auto with coc core arith datatypes. discriminate H10. red in |- *; intros; apply H5. simpl in |- *. rewrite H6; auto with coc core arith datatypes. apply inv_typ_prod with e M1 M2 K; intros; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. rewrite H3. elim class_red with e M1 N1 (Srt s1); auto with coc core arith datatypes. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. cut (skel_int M1 ip = PROP); intros. pattern (cl_term M2 (class_env (M1 :: e))) in |- *. apply class_typ_ord with s2; auto with coc core arith datatypes. elim skel_sound with (M1 :: e) M2 (Srt s2); simpl in |- *; auto with coc core arith datatypes. apply eq_can_Pi; auto with coc core arith datatypes. elim H9. apply H1 with e (Srt s1); auto with coc core arith datatypes. rewrite H3. apply class_typ_ord with s1; auto with coc core arith datatypes. discriminate. discriminate. simpl in |- *; intros. unfold int_cons, ext_ik in |- *. rewrite H3. elim class_red with e M1 N1 (Srt s1); auto with coc core arith datatypes. pattern (cl_term M1 (class_env e)) at 1 3 in |- *. elim (cl_term M1 (class_env e)); auto with coc core arith datatypes. intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. pattern (cl_term M1 (class_env e)) in |- *. apply class_typ_ord with s1; auto with coc core arith datatypes. simpl in |- *. apply eq_can_Pi; auto with coc core arith datatypes. elim H9. apply H1 with e (Srt s1); auto with coc core arith datatypes. rewrite H3. apply class_typ_ord with s1; auto with coc core arith datatypes. discriminate. discriminate. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply int_equiv_int_typ. unfold int_cons, ext_ik in |- *. rewrite H3. elim class_red with e M1 N1 (Srt s1); auto with coc core arith datatypes. elim (cl_term M1 (class_env e)); auto with coc core arith datatypes. simpl in |- *. apply eq_can_Pi; auto with coc core arith datatypes. elim H9. apply H1 with e (Srt s1); auto with coc core arith datatypes. rewrite H3. apply class_typ_ord with s1; auto with coc core arith datatypes. discriminate. discriminate. simpl in |- *; intros. change (eq_can PROP (int_typ M2 (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X1) PROP) (int_typ M2 (int_cons N1 ip (cv_skel (cl_term M1 (class_env e))) X2) PROP)) in |- *. unfold int_cons, ext_ik in |- *. rewrite H3. elim class_red with e M1 N1 (Srt s1); auto with coc core arith datatypes. pattern (cl_term M1 (class_env e)) at 1 3 in |- *. elim (cl_term M1 (class_env e)); auto with coc core arith datatypes. unfold skel_int in |- *. rewrite H3. elim skel_sound with e M1 (Srt s1); simpl in |- *; auto with coc core arith datatypes. apply inv_typ_prod with e M1 M2 K; intros; auto with coc core arith datatypes. unfold skel_int in |- *. simpl in |- *. rewrite H3. elim class_red with (M1 :: e) M2 N2 (Srt s2); auto with coc core arith datatypes. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. pattern (cl_term M2 (class_env (M1 :: e))) in |- *. apply class_typ_ord with s2; auto with coc core arith datatypes. elim skel_sound with (M1 :: e) M2 (Srt s2); simpl in |- *; auto with coc core arith datatypes. apply eq_can_Pi; auto with coc core arith datatypes. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply eq_can_trans with (int_typ M2 (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2) PROP); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. replace PROP with (skel_int M2 (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)). apply H1 with (M1 :: e) (Srt s2); auto with coc core arith datatypes. apply int_cons_equal with s1; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. red in |- *; intros. apply H5. simpl in |- *. replace (TCs class (cl_term M1 (cls_of_int ip)) (cls_of_int ip)) with (cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)). rewrite H12; auto with coc core arith datatypes. rewrite H3. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. apply int_cons_equal with s1; auto with coc core arith datatypes. unfold skel_int in |- *. replace (cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)) with (class_env (M1 :: e)). elim skel_sound with (M1 :: e) M2 (Srt s2); auto with coc core arith datatypes. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. symmetry in |- *. apply int_cons_equal with s1; auto with coc core arith datatypes. cut (cl_term M1 (cls_of_int ip) = cl_term M1 (class_env e)). pattern (cl_term M1 (class_env e)) in |- *. apply class_typ_ord with s1; auto with coc core arith datatypes. simpl in |- *; intros. apply eq_can_Pi; auto with coc core arith datatypes. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply eq_can_trans with (int_typ M2 (int_cons M1 ip PROP X2) PROP); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. pattern PROP at 1 3 5 in |- *. replace PROP with (skel_int M2 (int_cons M1 ip PROP X2)). cut (cv_skel (cl_term M1 (class_env e)) = PROP); intros. apply H1 with (M1 :: e) (Srt s2); auto with coc core arith datatypes. generalize X2 H12. change (forall X2 : Can PROP, eq_can PROP X2 X2 -> cls_of_int (int_cons M1 ip PROP X2) = class_env (M1 :: e)) in |- *. elim H13. intros. apply int_cons_equal with s1; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. replace (cls_of_int (int_cons M1 ip PROP X2)) with (class_env (M1 :: e)). red in |- *; intros; apply H5. simpl in |- *. rewrite H3. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. rewrite H14; auto with coc core arith datatypes. generalize X2 H12. change (forall X2 : Can PROP, eq_can PROP X2 X2 -> class_env (M1 :: e) = cls_of_int (int_cons M1 ip PROP X2)) in |- *. elim H13. intros. symmetry in |- *. apply int_cons_equal with s1; auto with coc core arith datatypes. elim H3. rewrite H9; simpl in |- *; auto with coc core arith datatypes. unfold skel_int in |- *. replace (cls_of_int (int_cons M1 ip PROP X2)) with (class_env (M1 :: e)). elim skel_sound with (M1 :: e) M2 (Srt s2); auto with coc core arith datatypes. generalize X2 H12. change (forall X2 : Can PROP, eq_can PROP X2 X2 -> class_env (M1 :: e) = cls_of_int (int_cons M1 ip PROP X2)) in |- *. replace PROP with (cv_skel (cl_term M1 (class_env e))). intros. symmetry in |- *. apply int_cons_equal with s1; auto with coc core arith datatypes. elim H3. rewrite H9; auto with coc core arith datatypes. intros. simpl in |- *. apply eq_can_Pi; auto with coc core arith datatypes. simpl in |- *; intros. replace eq_cand with (eq_can PROP); auto with coc core arith datatypes. apply eq_can_trans with (int_typ M2 (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2) PROP); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. replace PROP with (skel_int M2 (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)). apply H1 with (M1 :: e) (Srt s2); auto with coc core arith datatypes. apply int_cons_equal with s1; auto with coc core arith datatypes. unfold int_cons, ext_ik in |- *. elim (cl_term M1 (cls_of_int ip)); auto with coc core arith datatypes. red in |- *; intros. apply H5. simpl in |- *. replace (TCs class (cl_term M1 (cls_of_int ip)) (cls_of_int ip)) with (cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)). rewrite H13; auto with coc core arith datatypes. rewrite H3. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. apply int_cons_equal with s1; auto with coc core arith datatypes. unfold skel_int in |- *. replace (cls_of_int (int_cons M1 ip (cv_skel (cl_term M1 (class_env e))) X2)) with (class_env (M1 :: e)). elim skel_sound with (M1 :: e) M2 (Srt s2); auto with coc core arith datatypes. replace (TCs class (cl_term M1 (class_env e)) (class_env e)) with (class_env (M1 :: e)); auto with coc core arith datatypes. symmetry in |- *. apply int_cons_equal with s1; auto with coc core arith datatypes. elim H3; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class Can Int_typ