# Library Conv_Dec

``` Require Import Transitive_Closure. Require Import Union. Require Export Peano_dec. Require Export Conv. Hint Unfold transp union: core. Hint Resolve t_step: core.   Definition ord_norm1 := union _ subterm (transp _ red1).   Definition ord_norm := clos_trans _ ord_norm1.   Hint Unfold ord_norm1 ord_norm: coc.   Lemma subterm_ord_norm : forall a b, subterm a b -> ord_norm a b. auto 10 with coc. Qed.   Hint Resolve subterm_ord_norm: coc.   Lemma red_red1_ord_norm :    forall a b, red a b -> forall c, red1 b c -> ord_norm c a. red in |- *. simple induction 1; intros; auto with coc. apply t_trans with N; auto with coc. Qed.   Lemma wf_subterm : well_founded subterm. red in |- *. simple induction a; intros; apply Acc_intro; intros. inversion_clear H. inversion_clear H. inversion_clear H1; auto with coc. inversion_clear H1; auto with coc. inversion_clear H1; auto with coc. Qed.   Lemma wf_ord_norm1 : forall t, sn t -> Acc ord_norm1 t. unfold ord_norm1 in |- *. intros. apply Acc_union; auto with coc. exact commut_red1_subterm. intros. apply wf_subterm. Qed.   Theorem wf_ord_norm : forall t, sn t -> Acc ord_norm t. unfold ord_norm in |- *. intros. apply Acc_clos_trans. apply wf_ord_norm1; auto with coc. Qed.   Definition norm_body a norm :=     match a with     | Srt s => Srt s     | Ref n => Ref n     | Abs T t => Abs (norm T) (norm t)     | App u v =>         match norm u return term with         | Abs _ b => norm (subst (norm v) b)         | t => App t (norm v)         end     | Prod T U => Prod (norm T) (norm U)     end.   Theorem compute_nf : forall t, sn t -> {u : _ | red t u & normal u}. intros. elimtype (Acc ord_norm t). intros [s| n| T t0| u v| T U] _ norm. exists (Srt s); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. exists (Ref n); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. elim (norm T); auto with coc; intros nT T_red T_norm. elim (norm t0); auto with coc; intros nt0 t0_red t0_norm. exists (Abs nT nt0); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. apply (T_norm M'); auto with coc. apply (t0_norm M'); auto with coc. elim (norm v); auto with coc; intros nv v_red v_norm. elim (norm u); auto with coc; intros [s| n| T b| u0 v0| T U] u_red u_norm. exists (App (Srt s) nv); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. inversion_clear H1. apply (v_norm N2); auto with coc. exists (App (Ref n) nv); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. inversion_clear H1. apply (v_norm N2); auto with coc. elim (norm (subst nv b)). intros nt t_red t_norm. exists nt; auto with coc. apply trans_red_red with (subst nv b); auto with coc. apply trans_red with (App (Abs T b) nv); auto with coc. apply red_red1_ord_norm with (App (Abs T b) nv); auto with coc. exists (App (App u0 v0) nv); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. elim u_norm with N1; auto with coc. elim v_norm with N2; auto with coc. exists (App (Prod T U) nv); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. elim u_norm with N1; auto with coc. elim v_norm with N2; auto with coc. elim (norm T); auto with coc; intros nT T_red T_norm. elim (norm U); auto with coc; intros nU U_red U_norm. exists (Prod nT nU); auto with coc. red in |- *; red in |- *; intros. inversion_clear H0. apply (T_norm N1); auto with coc. apply (U_norm N2); auto with coc. apply wf_ord_norm; auto with coc. Qed.   Lemma eqterm : forall u v : term, {u = v} + {u <> v}. Proof. decide equality. decide equality s s0. apply eq_nat_dec. Qed.   Theorem is_conv : forall u v, sn u -> sn v -> {conv u v} + {~ conv u v}. intros u v sn_u sn_v. elim (compute_nf u); auto with coc; intros nu u_red u_norm. elim (compute_nf v); auto with coc; intros nv v_red v_norm. elim (eqterm nu nv). intros eq_nf. left. rewrite eq_nf in u_red. apply trans_conv_conv with nv; auto with coc. apply sym_conv; auto with coc. intros diff_nf. right; red in |- *; intro; apply diff_nf. elim church_rosser with nu nv; intros. rewrite red_normal with (1 := H0); trivial. rewrite red_normal with (1 := H1); trivial. apply trans_conv_conv with u; auto with coc. apply sym_conv; auto with coc. apply trans_conv_conv with v; auto with coc. Qed. ```