proposition: Lemma rpo_mul_dec: forall bb k l, {rpo_mul bb k l}+{~ rpo_mul bb k l}.
proof: Proof. intros. assert (H' := remove_equiv_list_is_sound k l). revert H'; destruct (remove_equiv_list k l) as [k' l']; intro H'. destruct H' as [lc [Pk [Pl D]]]. assert (Rem : rpo_mul bb0 k l -> rpo_mul bb0 k' l'). generalize l k l' k' Pk Pl; clear l k l' k' Pk Pl D. 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 bb0 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 bb0 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 bb0 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 bb0 u v) in assert (H' : {P} + {~ P}). assert (IH' : forall u v, mem equiv u k' -> mem equiv v l' -> {rpo bb0 u v}+{~rpo bb0 u v}). intros u v u_mem_k' v_mem_l'. apply rpo_dec. generalize l' IH'; clear l k 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 bb0 u' v) in assert (H : {v | mem equiv v l' /\ rpo bb0 u' v}+{P}). assert (IH'' : forall v, mem equiv v l' -> {rpo bb0 u' v}+{~rpo bb0 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. assert (rpo_mul bb0 k' []). apply Rem. trivial. inversion H. inversion H1. destruct H' as [Ok | Ko]. left; apply (@List_mul bb0 v' l' k' lc); trivial. right. intro. contradict Ko. assert (rpo_mul bb0 k' (v' :: l')). apply Rem. trivial. inversion H0 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. Qed.
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)