proposition: Lemma remove_equiv_is_sound: forall l1 l2, match remove_equiv eq_bool l1 l2 with | (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\ (forall x, mem eq_A x l1' -> mem eq_A x l2' -> False) end.
proof: Proof. intros l1 l2; functional induction (remove_equiv eq_bool l1 l2) as [ | H1 l2 e1 l1 H2 l2' H H' | H1 l2 e1 l1 H2 H H' l1'' l2'' H'']. exists (@nil A); simpl; intuition. case_eq (remove_equiv eq_bool l1 l2'); intros l1'' l2'' H''; rewrite H'' in H'. revert H'; intros [l [P1 [P2 H']]]. exists (e1 :: l); simpl; split. apply (proj1 (permut_cons l1 (l ++ l1'') (equiv_refl _ _ eq_proof e1))); assumption. split; trivial. apply permut_trans with (e1 :: l2'). assert (H''' := remove_is_sound e1 l2); rewrite H in H'''; trivial. apply (proj1 (permut_cons l2' (l ++ l2'') (equiv_refl _ _ eq_proof e1))); assumption. case_eq (remove_equiv eq_bool l1 l2); intros l1' l2' H'''; rewrite H''' in H''; injection H''; clear H''; intros; subst l1'' l2''. rewrite H''' in H'; revert H'; intros [l [P1 [P2 H']]]; exists l; split. rewrite <- permut_cons_inside; trivial. reflexivity. split; trivial. intros x [x_eq_e1 | x_mem_l1'] x_mem_l2'. assert (H'' := remove_is_sound e1 l2); rewrite H in H''. absurd (mem eq_A e1 l2); trivial. apply (proj1 (mem_morph x_eq_e1 (permut_refl l2))). apply (proj2 (mem_permut_mem x P2)). rewrite <- mem_or_app; right; trivial. apply (H' x); trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)