proposition: Lemma permut_dec : forall (A B : Type) (R : A -> B -> Prop), forall l1 l2, (forall a1 a2, In a1 l1 -> In a2 l2 -> {R a1 a2}+{~R a1 a2}) -> {permut0 R l1 l2}+{~permut0 R l1 l2}.
proof: Proof. intros A B R l1; induction l1 as [ | a1 l1]; intros l2 R_dec. revert R_dec. destruct l2 as [ | a2 l2]. left; apply Pnil. right; intro P; inversion P. assert (P_dec : forall a : B * (list B * list B), In a (split_all l2) -> {(fun bll' : B * (list B * list B) => let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut0 R l1 (l ++ l')) a} + {~ (fun bll' : B * (list B * list B) => let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut0 R l1 (l ++ l')) a}). intros [b [l l']] H; rewrite split_all_is_sound in H. destruct (R_dec a1 b) as [a1_R_b | not_a1_R_b]. left; trivial. subst l2; apply in_or_app; right; left; trivial. destruct (IHl1 (l ++ l')) as [P | not_P]. intros; apply R_dec. right; trivial. subst l2; apply in_insert; trivial. left; split; trivial. right; intros [_ P]; apply not_P; trivial. right; intros [a1_R_b _]; apply not_a1_R_b; trivial. assert (H := list_exists_rest_is_sound (fun bll' => match bll' with | (b,(l,l')) => R a1 b /\ permut0 R l1 (l ++ l') end) (split_all l2) P_dec). destruct (list_exists_rest (fun bll' : B * (list B * list B) => let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut0 R l1 (l ++ l')) (split_all l2) P_dec). left. destruct ((proj1 H) (eq_refl _)) as [[b [l l']] [H' [a1_R_b P]]]. rewrite split_all_is_sound in H'; subst l2; apply Pcons; trivial. right; intro P; inversion P; subst. assert (false = true). rewrite H; exists (b,(l0,l3)); split; trivial. rewrite split_all_is_sound; trivial. split; trivial. discriminate. Defined.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)