proposition: Lemma rpo_dec : forall bb t1 t2, {rpo bb t1 t2}+{~rpo bb t1 t2}.
proof: Proof. intro bb. cut (forall p, match p with (t2,t1) => {rpo bb t1 t2}+{~rpo bb t1 t2} end). intros H t1 t2; apply (H (t2,t1)). intro p; pattern p; refine (well_founded_induction wf_size2 _ _ _); clear p. intros [[v | f l] t1] IH. right; intro t1_lt_t2; inversion t1_lt_t2. assert (H : {t | mem equiv t l /\ rpo_eq bb t1 t}+{~exists t, mem equiv t l /\ rpo_eq bb t1 t}). induction l as [ | s l]. right; intros [t [t_mem_nil _]]; contradiction. destruct (equiv_dec t1 s) as [t1_eq_s | t1_diff_s]. left; exists s; split. left; reflexivity. apply Equiv; trivial. destruct (IH (s,t1)) as [t1_lt_s | not_t1_lt_s]. apply size2_lex1; left; trivial. left; exists s; split. left; reflexivity. apply Lt; trivial. destruct IHl as [Ok | Ko]. intros [t2 t1'] H; apply (IH (t2,t1')). apply o_size2_trans with (Term f l, t1); trivial. apply size2_lex1_bis. destruct Ok as [t [t_mem_l t1_le_t]]. left; exists t; split; trivial. right; trivial. right; intros [t [[s_eq_t | t_mem_l] t1_le_t]]. destruct t1_le_t. apply t1_diff_s; transitivity t'; trivial; symmetry; trivial. apply not_t1_lt_s; rewrite <- (equiv_rpo_equiv_1 _ s_eq_t); trivial. apply Ko; exists t; split; trivial. destruct H as [[t [t_mem_l t1_le_t]] | H]. left; apply Subterm with t; trivial. revert IH H. destruct t1 as [v | g k]; intros IH H. right; intro v_lt_fl; inversion v_lt_fl; subst. apply H; exists s; split; trivial. case_eq (prec_eq_bool Prec g f); [intro g_eq_f | intro g_diff_f]. assert (f_eq_g: prec_eq Prec f g). assert (H1:= prec_eq_bool_ok). assert (H1':= H1 symbol Prec g f). rewrite g_eq_f in H1'. apply prec_eq_sym; trivial. assert (Sf_eq_Sg: status Prec g = status Prec f). apply prec_eq_status; apply prec_eq_sym; trivial. case_eq (status Prec f); intro Sf. assert (H' : {rpo_lex bb k l}+{~rpo_lex bb k l}). generalize k IH; clear k IH H; induction l as [ | t l]; intros k IH. right; intro k_lt_nil; inversion k_lt_nil. revert IH; destruct k as [ | s k]; intro IH. left; apply List_nil. destruct (IH (t,s)) as [s_lt_t | not_s_lt_t]. apply size2_lex1; left; trivial. left; apply List_gt; trivial. destruct (equiv_dec s t) as [s_eq_t | s_diff_t]. destruct (IHl k) as [k_lt_l | not_k_lt_l]. intros [t2 t1] H; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term g k); trivial. apply size2_lex1_bis. left; apply List_eq; trivial. right; intro sk_lt_tl; inversion sk_lt_tl; subst. absurd (rpo bb s t); trivial. absurd (rpo_lex bb k l); trivial. right; intro sk_lt_tl; inversion sk_lt_tl; subst. absurd (rpo bb s t); trivial. absurd (equiv s t); trivial. destruct H' as [k_lt_l | not_k_lt_l]. let P := constr:(forall (s:term), mem equiv s k -> rpo bb s (Term f l)) in assert (H'' : { P }+{~P}). clear k_lt_l H; revert IH; induction k as [ | s k IHk]; intro IH. left; intros s s_mem_nil; contradiction. destruct (IH (Term f l, s)) as [s_lt_fl | not_s_lt_fl]. apply size2_lex2; left; trivial. destruct IHk as [Ok | Ko]. intros [t2 t1] H'; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term f k); trivial. apply size2_lex2_bis_prec_eq with Prec; trivial. left; intros s' [s_eq_s' | s'_mem_k]. rewrite (equiv_rpo_equiv_2 _ s_eq_s'); trivial. apply Ok; trivial. right; intro H; apply Ko. intros s' s'_mem_k; apply H; right; trivial. right; intro H; apply not_s_lt_fl; apply H; left; reflexivity. destruct H'' as [Ok | Ko]. destruct (eq_nat_dec (length l) (length k)). left; apply Top_eq_lex; trivial. rewrite Sf_eq_Sg; trivial. apply prec_eq_sym; trivial. left; trivial. destruct (le_lt_dec (length k) bb). destruct (le_lt_dec (length l) bb). left; apply Top_eq_lex; trivial. rewrite Sf_eq_Sg; trivial. apply prec_eq_sym; trivial. right; split; assumption. right; intro fk_lt_fl; inversion fk_lt_fl; subst. apply H; exists s; split; assumption. apply prec_not_prec_eq with symbol Prec g f; trivial. apply prec_eq_sym; trivial. destruct H7 as [H7 | [H7 H7']]. apply n; assumption. apply Nat.lt_irrefl with bb. apply Nat.lt_le_trans with (length l); assumption. rewrite H5 in Sf; discriminate. right; intro fk_lt_fl; inversion fk_lt_fl; subst. apply H; exists s; split; assumption. apply (prec_antisym Prec f); trivial. assert (H6: False). apply prec_not_prec_eq with symbol Prec g f; trivial. apply prec_eq_sym; trivial. contradict H6. destruct H7 as [H7 | [H7 H7']]. apply n; assumption. apply Nat.lt_irrefl with bb. apply Nat.lt_le_trans with (length k); assumption. rewrite H5 in Sf; discriminate. right; intro fk_lt_fl; inversion fk_lt_fl; subst. apply Ko; intros s' s'_mem_k; apply rpo_trans with (Term g k); trivial. apply Subterm with s'; trivial. apply Equiv; reflexivity. apply (prec_antisym Prec f); trivial. contradict Ko; trivial. contradict Ko; trivial. rewrite H5 in Sf; discriminate. right ; intro fk_lt_fl; inversion fk_lt_fl; subst. apply H; exists s; split; trivial. apply (prec_antisym Prec f); trivial. assert (H6: False). apply prec_not_prec_eq with symbol Prec g f; trivial. apply prec_eq_sym; trivial. contradict H6. apply not_k_lt_l; trivial. rewrite H5 in Sf; discriminate. assert (H' := remove_equiv_list_is_sound k l). revert IH H H'; destruct (remove_equiv_list k l) as [k' l']; intros IH H H'; destruct H' as [lc [Pk [Pl D]]]. assert (Rem : rpo_mul bb k l -> rpo_mul bb k' l'). generalize l k l' k' Pk Pl; clear l k l' k' Pk Pl D IH H. induction lc as [ | c lc]; intros l k l' k' Pk Pl k_lt_l. inversion k_lt_l as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. apply (@List_mul bb a lg ls lc'); trivial. transitivity k; trivial; symmetry; rewrite <- app_nil_end in Pk; trivial. transitivity l; trivial; symmetry; rewrite <- app_nil_end in Pl; trivial. assert (H := IHlc l k (l' ++ c :: nil) (k' ++ c :: nil)). do 2 rewrite <- ass_app in H; simpl in H. generalize (H Pk Pl k_lt_l); clear H; intro H. apply (@rpo_mul_remove_equiv_aux bb k' l' c c). intros t _; apply rpo_antirefl. reflexivity. inversion H as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. apply (@List_mul bb a lg ls lc'); trivial. rewrite <- Rk; rewrite <- permut0_cons_inside;[|apply equiv_equiv|reflexivity]. rewrite <- app_nil_end; reflexivity || auto. rewrite <- Rl; rewrite <- permut0_cons_inside;[|apply equiv_equiv|reflexivity]. rewrite <- app_nil_end; reflexivity || auto. let P := constr:(forall u, mem equiv u k' -> exists v, mem equiv v l' /\ rpo bb u v) in assert (H' : {P} + {~ P}). assert (IH' : forall u v, mem equiv u k' -> mem equiv v l' -> {rpo bb u v}+{~rpo bb u v}). intros u v u_mem_k' v_mem_l'; apply (IH (v,u)). apply size2_lex1_mem. rewrite Pl; rewrite <- mem_or_app; left; trivial. generalize l' IH'; clear l k IH H l' lc Pk Pl D IH' Rem. induction k' as [ | u' k']; intros l' IH'. left; intros; contradiction. let P:=constr:(forall v, mem equiv v l' -> ~rpo bb u' v) in assert (H : {v | mem equiv v l' /\ rpo bb u' v}+{P}). assert (IH'' : forall v, mem equiv v l' -> {rpo bb u' v}+{~rpo bb u' v}). intros v v_mem_l'; apply (IH' u' v); trivial. left; reflexivity. clear IHk' IH'; induction l' as [ | v' l']. right; intros; contradiction. destruct IHl' as [Ok | Ko]. intros; apply IH''; right; trivial. destruct Ok as [v [v_mem_l' u'_lt_v]]; left; exists v; split; trivial. right; trivial. destruct (IH'' v') as [Ok' | Ko']. left; reflexivity. left; exists v'; split; trivial. left; reflexivity. right; intros v [v'_eq_v | v_mem_l']. intros u'_lt_v; apply Ko'. rewrite <- (equiv_rpo_equiv_1 _ v'_eq_v); trivial. apply Ko; trivial. destruct H as [[v [v_mem_l' u'_lt_v]] | Ko]. destruct (IHk' l') as [Ok' | Ko']. intros u v' u_mem_k' v'_mem_l'; apply IH'; trivial; right; trivial. left; intros u [u'_eq_u | u_mem_k']. exists v; split; trivial. rewrite (equiv_rpo_equiv_2 _ u'_eq_u); trivial. apply Ok'; trivial. right; intro H; apply Ko'. intros u u_mem_k'; apply H; right; trivial. right; intro H. destruct (H u') as [v [v_mem_l' u'_lt_v]]. left; reflexivity. apply (Ko v); trivial. destruct l' as [ | v' l']. right; intro fk_lt_fl. inversion fk_lt_fl as [f' l' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' g' k'' l'' Sf' Sg' f'_eq_g' L k''_lt_l'' l'_lt_t | f' g' k'' l'' Sf' Sg' f'_eq_g' k_lt_l ]; subst. apply H; exists t'; split; trivial. assert (H5:False). apply prec_not_prec_eq with symbol Prec g f; trivial. apply prec_eq_sym; trivial. contradict H5. rewrite Sf in Sg'; discriminate. assert (k'_lt_nil := Rem k_lt_l). inversion k'_lt_nil as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. assert (L := permut_length Rl); discriminate. destruct H' as [Ok | Ko]. left; apply Top_eq_mul; trivial. rewrite Sf_eq_Sg; trivial. apply prec_eq_sym; trivial. apply (@List_mul bb v' l' k' lc); trivial. right; intro fk_lt_fl. inversion fk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' L k''_lt_l'' l'_lt_t | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' k_lt_l ]; subst. rewrite Pl in t'_mem_l; rewrite <- mem_or_app in t'_mem_l. destruct t'_mem_l as [t'_mem_vl' | t'_mem_lc]. apply Ko; intros u u_mem_k'; exists t'; split; trivial. inversion fk_le_t'; subst. rewrite <- (@equiv_rpo_equiv_1 _ (Term g k) t'); trivial. apply Subterm with u. rewrite Pk; rewrite <- mem_or_app; left; trivial. apply Equiv; apply Eq. apply rpo_trans with (Term g k); trivial. apply Subterm with u. rewrite Pk; rewrite <- mem_or_app; left; trivial. apply Equiv; apply Eq. apply (@rpo_antirefl bb (Term g k)). inversion fk_le_t'; subst. rewrite (@equiv_rpo_equiv_2 _ (Term g k) t'); trivial. apply Subterm with t'. rewrite Pk; rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. apply rpo_trans with t'; trivial. apply Subterm with t'. rewrite Pk; rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. assert (H5:False). apply prec_not_prec_eq with symbol Prec g f; trivial. apply prec_eq_sym; trivial. contradict H5. rewrite Sf in Sf''; discriminate. assert (k'_lt_vl' := Rem k_lt_l). apply Ko. inversion k'_lt_vl' as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. intro u; rewrite Rk; rewrite <- mem_or_app. intros [u_mem_ls | u_mem_lc']. destruct (ls_lt_alg _ u_mem_ls) as [a' [a'_mem_alg u_lt_a']]; exists a'; split; trivial. rewrite Rl; rewrite app_comm_cons; rewrite <- mem_or_app; left; trivial. assert False. apply (D u u). rewrite Rk; rewrite <- mem_or_app; right; trivial. rewrite Rl; rewrite app_comm_cons; rewrite <- mem_or_app; right; trivial. reflexivity. contradiction. generalize (prec_bool_ok Prec g f); case (prec_bool Prec g f); [intro g_prec_f | intro not_g_prec_f]. let P:=constr:(forall t, mem equiv t k -> rpo bb t (Term f l)) in assert (H' : {P}+{~P}). clear H; revert IH; induction k as [ | s k]; intro IH. left; intros; contradiction. destruct (IH (Term f l,s)) as [s_lt_fl | not_s_lt_fl]. apply size2_lex2; left; trivial. destruct IHk as [Ok | Ko]. intros [t2 t1] St; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term g k); trivial. apply size2_lex2_bis. left; intros t [t_eq_s | t_mem_k]. rewrite (equiv_rpo_equiv_2 _ t_eq_s); trivial. apply Ok; trivial. right; intro sk_lt_fl; apply Ko; intros; apply sk_lt_fl; right; trivial. right; intro sk_lt_fl; apply not_s_lt_fl; intros; apply sk_lt_fl; left; reflexivity. destruct H' as [Ok | Ko]. left; apply Top_gt; trivial. right; intro gk_lt_fl; inversion gk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' L k''_lt_l'' l'_lt_t | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' k_lt_l ]; subst. apply H; exists t'; split; trivial. apply Ko; trivial. apply (prec_antisym Prec f); trivial. apply prec_eq_prec2 with g; trivial. apply (prec_antisym Prec f); trivial. apply prec_eq_prec2 with g; trivial. right; intro gk_lt_fl; inversion gk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' L k''_lt_l'' l'_lt_t | f' f'' k'' l'' Sf' Sf'' f'_eq_f'' k_lt_l ]; subst. apply H; exists t'; split; trivial. absurd (prec Prec g f); trivial. assert (H5:=prec_eq_bool_ok). assert (H5':= H5 symbol Prec g f). rewrite g_diff_f in H5'. contradict H5'; trivial. assert (H5:=prec_eq_bool_ok). assert (H5':= H5 symbol Prec g f). rewrite g_diff_f in H5'. contradict H5'; trivial. Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)