# Library Infer

``` Require Import Strong_Norm. Require Import Conv_Dec.   Lemma is_sort : forall t, {s : _ | t = Srt s} + {(forall s, t <> Srt s)}. simple destruct t; intros; try (right; red in |- *; intros; discriminate). left; exists s; trivial. Qed.   Lemma is_prod :    forall t,    {p : _ * _ | let (T, U) := p in t = Prod T U} +    {(forall T U, t <> Prod T U)}. simple destruct t; intros; try (right; red in |- *; intros; discriminate). left; exists (t0, t1); trivial. Qed.   Lemma red_to_sort :    forall t, sn t -> {s:_| red t (Srt s)} + {forall s, ~ conv t (Srt s)}. Proof. intros t sn_t. elim (compute_nf t); auto with coc; intros nt t_red t_norm. elim (is_sort nt). intros (s, eq_s). left; exists s. elim eq_s; trivial. intros not_s; right; red in |- *; intros. elim church_rosser with (Srt s) nt; intros. apply red_sort_sort with s nt; trivial. rewrite red_normal with (1 := H1); trivial. apply trans_conv_conv with t; auto with coc. Qed.   Lemma red_to_prod :    forall t,    sn t ->    {p:term*term| let (u,v):= p in red t (Prod u v)} +    {forall u v, ~ conv t (Prod u v)}. intros t sn_t. elim (compute_nf t); auto with coc; intros nt t_red t_norm. elim (is_prod nt). intros ((T, U), eq_pi). left; exists (T, U). elim eq_pi; trivial. intros diff_pi; right; red in |- *; intros. elim church_rosser with (Prod u v) nt; intros. apply red_prod_prod with u v nt; auto; intros. rewrite red_normal with (1 := H1); trivial. elim diff_pi with (1 := H2). apply trans_conv_conv with t; auto with coc. Qed. Section Decidabilite_typage.   Theorem infer :    forall e t, wf e -> {T : _ | typ e t T} + {(forall T, ~ typ e t T)}. intros e t. generalize e; clear e. elim t; clear t. intros [| ] e wfe. right; red in |- *; intros. elim inv_typ_kind with e T; auto. left; exists (Srt kind). apply type_prop; trivial. intros n e wfe. elim (list_item e n). intros (t, t_item). left; exists (lift (S n) t). apply type_var; auto. exists t; auto. right; red in |- *; intros. apply inv_typ_ref with (1 := H); intros. elim b with U; auto. intros t typ_t b typ_b e wfe. elim (typ_t e); trivial. intros (T, ty_t). elim (red_to_sort T). intros (s1, T_srt). elim (typ_b (t :: e)). intros (B, ty_b). elim (eqterm (Srt kind) B). intros B_kind. right; red in |- *; intros. apply inv_typ_abs with (1 := H); intros. elim inv_typ_conv_kind with (2 := H2). rewrite B_kind. apply typ_unique with (1 := H1); trivial. intros B_not_kind. left; exists (Prod t B). elim type_case with (1 := ty_b); intros. inversion_clear H. apply type_abs with s1 x; auto. apply type_reduction with T; auto. elim B_not_kind; auto. intros b_not_ty. right; red in |- *; intros. apply inv_typ_abs with (1 := H); intros. elim b_not_ty with T1; auto. apply wf_var with s1. apply type_reduction with T; auto. intros T_not_s. right; red in |- *; intros. apply inv_typ_abs with (1 := H); intros. elim T_not_s with s1. apply typ_unique with e t; auto. apply type_sn with e t; auto. intros t_not_ty. right; red in |- *; intros. apply inv_typ_abs with (1 := H); intros. elim t_not_ty with (Srt s1); auto. intros t typ_t b typ_b e wfe. elim (typ_t e); trivial. intros (T, ty_t). elim (red_to_prod T). intros ((V, Ur), red_T). elim (typ_b e); trivial. intros (B, ty_b). elim (is_conv V B). intros ty_conv. left; exists (subst b Ur). elim type_case with (1 := ty_t); intros. inversion_clear H. apply type_app with V; auto. apply inv_typ_prod with (1 := subject_reduction _ _ _ red_T _ H0); intros. apply type_conv with B s1; auto with coc. apply type_reduction with T; auto. elim conv_sort_prod with kind V Ur. elim H; auto with coc. intros not_conv. right; red in |- *; intros. apply not_conv. apply inv_typ_app with (1 := H); intros. apply trans_conv_conv with V0. apply inv_conv_prod_l with Ur Ur0. apply typ_unique with e t; auto. apply type_reduction with T; auto. apply typ_unique with e b; auto. apply subterm_sn with (Prod V Ur); auto with coc. apply sn_red_sn with T; auto. apply type_sn with e t; auto. apply type_sn with e b; auto. intros not_ty_b. right; red in |- *; intros. apply inv_typ_app with (1 := H); intros. elim not_ty_b with V0; auto. intros not_prod. right; red in |- *; intros. apply inv_typ_app with (1 := H); intros. elim not_prod with V Ur. apply typ_unique with e t; auto. apply type_sn with e t; auto. intros not_ty_t. right; red in |- *; intros. apply inv_typ_app with (1 := H); intros. elim not_ty_t with (Prod V Ur); auto. intros t typ_t b typ_b e wfe. elim (typ_t e); trivial. intros (T, ty_t). elim (red_to_sort T). intros (s1, T_srt). elim (typ_b (t :: e)). intros (B, ty_b). elim (red_to_sort B). intros (s2, B_srt). left; exists (Srt s2). apply type_prod with s1. apply type_reduction with (1 := T_srt); trivial. apply type_reduction with (1 := B_srt); trivial. intros B_not_s. right; red in |- *; intros. apply inv_typ_prod with (1 := H); intros. elim B_not_s with s2; auto. apply typ_unique with (t :: e) b; auto. apply type_sn with (1 := ty_b). intros b_not_ty. right; red in |- *; intros. apply inv_typ_prod with (1 := H); intros. elim b_not_ty with (Srt s2); auto. apply wf_var with s1; auto. apply type_reduction with (1 := T_srt); trivial. intros T_not_s. right; red in |- *; intros. apply inv_typ_prod with (1 := H); intros. elim T_not_s with s1. apply typ_unique with e t; auto. apply type_sn with (1 := ty_t). intros t_not_ty. right; red in |- *; intros. apply inv_typ_prod with (1 := H); intros. elim t_not_ty with (Srt s1); auto. Qed.   Lemma check_typ : forall e t tp, wf e -> {typ e t tp} + {~ typ e t tp}. intros e t tp wfe. elim (infer e t); trivial. intros (tp', ty_t). elim (eqterm tp' (Srt kind)). intros is_knd'. elim (eqterm tp (Srt kind)). intros is_knd. left. rewrite is_knd; rewrite is_knd' in ty_t; trivial. intros not_knd. right; red in |- *; intros; apply not_knd. apply type_kind_not_conv with (1 := H). elim is_knd'; trivial. intros not_knd'. elim (infer e tp); trivial. intros (U, ty_tp). elim (is_conv tp' tp). intros is_cnv. left. elim red_to_sort with U; intros. inversion_clear a. apply type_conv with tp' x; trivial. apply type_reduction with (1 := H); trivial. elim type_case with (1 := ty_t); intros. inversion_clear H. elim b with x. apply sym_conv. apply typ_conv_conv with (1 := H0) (3 := is_cnv); trivial. elim not_knd'; trivial. apply type_sn with (1 := ty_tp). intros not_conv. right; red in |- *; intros; apply not_conv. apply typ_unique with (1 := ty_t); trivial. apply type_sn with (1 := ty_t). apply strong_norm with (1 := ty_tp). intros tp_not_ty. right; red in |- *; intros. elim type_case with (1 := H); intros. inversion_clear H0. elim tp_not_ty with (1 := H1). apply not_knd'. apply type_kind_not_conv with (1 := ty_t); auto. elim H0; trivial. intros t_not_ty. right; auto. Qed.   Lemma add_typ : forall e t, wf e -> {wf (t :: e)} + {~ wf (t :: e)}. intros e t wfe. elim (infer e t); trivial. intros (u, ty_t). elim (red_to_sort u); auto. intros (s, u_srt). left. apply wf_var with s. apply type_reduction with (1 := u_srt); trivial. intros not_sort. right; red in |- *; intros. inversion_clear H. elim not_sort with s. apply typ_unique with (1 := ty_t); trivial. 4br/>apply type_sn with (1 := ty_t). intros t_not_ty. right; red in |- *; intros. inversion_clear H. elim t_not_ty with (1 := H0). Qed.   Lemma decide_wf : forall e, {wf e} + {~ wf e}. simple induction e; intros. left; apply wf_nil. elim H; intros. elim add_typ with l a; auto; intros. right; red in |- *; intros; apply b. inversion_clear H0. apply typ_wf with a (Srt s); auto. Qed.   Lemma decide_typ : forall e t tp, {typ e t tp} + {~ typ e t tp}. intros. elim decide_wf with e; intros. apply check_typ; auto. right; red in |- *; intros; apply b. apply typ_wf with t tp; auto. Qed. End Decidabilite_typage. ```