Set Implicit Arguments.

Require Import decidable_set.
Require Import List.
Require Import more_list.
Require Import Multiset.
Require Import Arith.
Require Import Setoid.

Module Type Permut.

Declare Module DS : decidable_set.S.

Definition elt := DS.A.
Definition eq_elt_dec := DS.eq_A_dec.

Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt :=
  match l with
  | nil ⇒ EmptyBag elt
  | h :: tl ⇒
      munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl)
  end.

Definition list_permut (l1 l2:list elt) : Prop :=
  meq (list_to_multiset l1) (list_to_multiset l2).

End Permut.

Module Make (DS1 : decidable_set.S) <: Permut with Module DS:= DS1.

Module DS := DS1.
Import DS1.

Definition elt := DS.A.
Definition eq_elt_dec : ∀ t1 t2 : elt, {t1 = t2} + {t1 ≠ t2} := DS.eq_A_dec.

Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt :=
  match l with
  | nil ⇒ EmptyBag elt
  | h :: tl ⇒
      munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl)
  end.

Definition list_permut (l1 l2:list elt) : Prop :=
  meq (list_to_multiset l1) (list_to_multiset l2).

Lemma multiplicity_app :
 ∀ (l1 l2:list elt) (t : elt),
   multiplicity (list_to_multiset (l1 ++ l2)) t =
   multiplicity (list_to_multiset l1) t + multiplicity (list_to_multiset l2) t.
Proof.
induction l1; intros; trivial.
simpl; intros; rewrite (IHl1 l2 t); auto with arith.
Qed.

Lemma out_mult_O :
  ∀ (t : elt) (l:list elt), ¬ In t l → multiplicity (list_to_multiset l) t = 0.
Proof.
intro t; unfold list_to_multiset; induction l.
intros _; trivial.
intro H; simpl; elim (eq_elt_dec a t).
intro; subst t; absurd (In a (a :: l)); trivial; left; trivial.
intros _; apply IHl;
unfold not; intros; apply H;
simpl; right; assumption.
Qed.

Lemma in_mult_S :
 ∀ (t : elt) (l : list elt), In t l → multiplicity (list_to_multiset l) t ≥ 1.
Proof.
intro t; unfold list_to_multiset; induction l.
contradiction.
simpl; intro H; elim H; clear H.
intro H; subst t; elim (eq_elt_dec a a).
intros _ ; auto with arith.
intro; absurd (a=a); trivial.
elim (eq_elt_dec a t).
intros _ _; auto with arith.
intros; simpl; apply IHl; assumption.
Qed.

Theorem list_permut_refl :
 ∀ (l : list elt), list_permut l l.
Proof.
unfold list_permut, meq; intros; trivial.
Qed.

Theorem list_permut_sym :
 ∀ l1 l2 : list elt, list_permut l1 l2 → list_permut l2 l1.
Proof.
unfold list_permut, meq; intros; apply sym_eq; trivial.
Qed.

Hint Immediate list_permut_refl.
Hint Resolve list_permut_sym.

Theorem list_permut_trans :
  ∀ l1 l2 l3 : list elt, list_permut l1 l2 → list_permut l2 l3 → list_permut l1 l3.
Proof.
unfold list_permut, meq; intros;
apply trans_eq with (multiplicity (list_to_multiset l2) a); trivial.
Qed.

Add Relation (list elt) list_permut
reflexivity proved by list_permut_refl
symmetry proved by list_permut_sym
transitivity proved by list_permut_trans as LP.

Lemma list_permut_nil :
 ∀ l, list_permut l nil → l = nil.
Proof.
intro l; destruct l as [ | e l ]; trivial.
intros Abs; absurd (list_permut (e :: l) nil); trivial.
unfold not; unfold list_permut, meq; intro H;
generalize (H e); simpl; elim (eq_elt_dec e e).
intros _; discriminate.
intro; absurd (e=e); trivial.
Qed.

Lemma in_permut_in :
  ∀ l1 l2 e, In e l1 → list_permut l1 l2 → In e l2.
Proof.
unfold list_permut, meq; intros l1 l2 e Inel1 Pl1l2.
elim (In_dec eq_elt_dec e l2).
intros; trivial.
intro notInel2; generalize (Pl1l2 e);
rewrite (out_mult_O e l2 notInel2);
intro M0; generalize (in_mult_S e l1 Inel1);
rewrite M0; unfold ge;
intro Abs; absurd (1≤0); trivial; inversion Abs.
Save.

Add Morphism (In (A :=elt)) : in_morph.
Proof.
intros y x1 x2; split; intros.
apply in_permut_in with x1; trivial.
apply in_permut_in with x2; trivial; apply list_permut_sym; trivial.
Qed.

Lemma cons_permut_in :
  ∀ l1 l2 e, list_permut (e :: l1) l2 → In e l2.
Proof.
intros l1 l2 e P; setoid_rewrite <- P; left; trivial.
Qed.

Lemma context_list_permut_cons :
  ∀ e l1 l2, list_permut l1 l2 → list_permut (e :: l1) (e :: l2).
Proof.
intros e l1 l2; unfold list_permut, meq; simpl.
intros H a; rewrite (H a); trivial.
Save.

Add Morphism (List.cons (A:=elt)) : add_elt_morph.
Proof.
intros; apply context_list_permut_cons; trivial.
Qed.

Lemma list_permut_add_inside :
∀ a l1 l2 l3 l4,
  list_permut (l1 ++ l2) (l3 ++ l4) →
  list_permut (l1 ++ a :: l2) (l3 ++ a :: l4).
Proof.
intros a l1 l2 l3 l4; unfold list_permut, meq; simpl;
intros H b; generalize (H b); clear H;
repeat rewrite multiplicity_app; simpl;
intro H; rewrite plus_comm; rewrite <- plus_assoc; apply sym_eq;
rewrite plus_comm; rewrite <- plus_assoc;
apply (f_equal (fun n ⇒ match eq_elt_dec a b with
                         | left _ ⇒ 1
                         | right _ ⇒ 0 end + n));
rewrite plus_comm; rewrite <- H; apply plus_comm.
Qed.

Lemma list_permut_add_cons_inside :
∀ a l l1 l2,
  list_permut l (l1 ++ l2) →
  list_permut (a :: l) (l1 ++ a :: l2).
Proof.
intros;
replace (a :: l) with (nil ++ a :: l); trivial;
apply list_permut_add_inside; trivial.
Qed.

Lemma context_list_permut_app1 :
  ∀ l l1 l2, list_permut l1 l2 → list_permut (l ++ l1) (l ++ l2).
Proof.
intros l l1 l2; unfold list_permut, meq; simpl.
intros H a;
rewrite (multiplicity_app l l1);
rewrite (multiplicity_app l l2);
rewrite (H a);
trivial.
Qed.

Lemma context_list_permut_app2 :
  ∀ l l1 l2, list_permut l1 l2 → list_permut (l1 ++ l) (l2 ++ l).
Proof.
intros l l1 l2; unfold list_permut, meq; simpl; intros H a;
rewrite (multiplicity_app l1 l);
rewrite (multiplicity_app l2 l);
rewrite (H a);
trivial.
Save.

Add Morphism (List.app (A:=elt)) : app_morph.
Proof.
intros x y H1 x' y' H2.
apply list_permut_trans with (x ++ y').
apply context_list_permut_app1; trivial.
apply context_list_permut_app2; trivial.
Qed.

Lemma list_permut_app_app :
 ∀ l1 l2, list_permut (l1 ++ l2) (l2 ++ l1).
Proof.
intros l1 l2;
unfold list_permut, meq;
intro a; rewrite multiplicity_app; rewrite multiplicity_app;
apply plus_comm.
Qed.

Lemma remove_context_list_permut_cons :
  ∀ e l1 l2, list_permut (e :: l1) (e :: l2) → list_permut l1 l2.
Proof.
intros e l1 l2; unfold list_permut, meq; simpl; intros H a;
generalize (H a); apply plus_reg_l.
Qed.

Lemma remove_context_list_permut_app2 :
  ∀ l l1 l2, list_permut (l1 ++ l) (l2 ++ l) → list_permut l1 l2.
Proof.
intros l l1 l2; unfold list_permut, meq; simpl;
intros H a; generalize (H a);
rewrite (multiplicity_app l1 l);
rewrite (multiplicity_app l2 l);
intros; apply plus_reg_l with (multiplicity (list_to_multiset l) a).
rewrite plus_comm; rewrite H0; rewrite plus_comm.
trivial.
Qed.

Lemma list_permut_remove_hd :
  ∀ l l1 l2 a,
  list_permut (a :: l) (l1 ++ a :: l2) → list_permut l (l1 ++ l2).
Proof.
intros l l1 l2 a; unfold list_permut, meq; simpl; intros H a0; generalize (H a0);
rewrite multiplicity_app; rewrite multiplicity_app;
simpl; intro H1;
apply plus_reg_l with (match eq_elt_dec a a0 with left _ ⇒ 1 | right _ ⇒ 0 end);
rewrite H1; repeat rewrite plus_assoc;
apply (f_equal (fun n ⇒ n + multiplicity (list_to_multiset l2) a0));
apply plus_comm.
Qed.

Lemma list_permut_length :
 ∀ l1 l2, list_permut l1 l2 → length l1 = length l2.
Proof.
induction l1; intros l2 H.
rewrite (list_permut_nil (list_permut_sym H)); auto.
elim (In_dec eq_elt_dec a l2).
intro Inal2; generalize (split_list_app_cons eq_elt_dec a l2 Inal2);
destruct (split_list eq_elt_dec l2 a); intro; subst l2.
rewrite list_app_length; simpl;
rewrite (IHl1 _ (list_permut_remove_hd l l0 H));
rewrite list_app_length; auto with arith.
intro notInal2; absurd (In a l2); trivial;
apply in_permut_in with (a :: l1); trivial;
left; trivial.
Qed.

Add Morphism (length (A:=elt)) : length_morph.
Proof.
apply list_permut_length.
Qed.

Lemma list_permut_size :
  ∀ size l1 l2, list_permut l1 l2 → list_size size l1 = list_size size l2.
Proof.
intro size; induction l1.
intros l2 P;
rewrite (list_permut_nil (list_permut_sym P));
trivial.
intros l2 P;
generalize (split_list_app_cons eq_elt_dec _ _ (cons_permut_in P));
destruct (split_list eq_elt_dec l2 a); intro; subst l2;
rewrite list_size_app; simpl;
rewrite (IHl1 _ (list_permut_remove_hd _ _ P));
rewrite list_size_app;
rewrite plus_comm; rewrite <- plus_assoc;
apply (f_equal (fun n ⇒ list_size size l + n));
apply plus_comm.
Qed.

Add Parametric Morphism size : (@list_size elt size) with signature (list_permut ==> @eq nat) as list_size_morph.
Proof.
apply list_permut_size.
Qed.

Lemma list_permut_map :
  ∀ f l1 l2, list_permut l1 l2 → list_permut (map f l1) (map f l2).
Proof.
intros f l1; induction l1.
intros l2 P; rewrite (list_permut_nil (list_permut_sym P)); apply list_permut_refl.
intros l2 P;
generalize (split_list_app_cons eq_elt_dec _ _ (cons_permut_in P));
destruct (split_list eq_elt_dec l2 a); intro; subst l2.
rewrite map_app; simpl;
apply list_permut_add_cons_inside; rewrite <- map_app;
apply (IHl1 _ (list_permut_remove_hd l l0 P)).
Qed.

Add Parametric Morphism f : (map f) with signature list_permut ==> list_permut as map_morph.
Proof.
intros; apply list_permut_map; trivial.
Qed.

Lemma list_permut_length_1:
 ∀ a b, list_permut (a :: nil) (b :: nil) → a = b.
Proof.
intros a b; unfold list_permut, meq; intro P;
generalize (P a); clear P; simpl.
elim (eq_elt_dec a a).
intros _; elim (eq_elt_dec b a).
intros b_eq_a _; apply sym_eq; trivial.
intros _ Abs; simpl in Abs; absurd (1=0); trivial; discriminate.
intro; absurd (a=a); trivial.
Qed.

Lemma list_permut_length_2 :
 ∀ a1 b1 a2 b2, list_permut (a1 :: b1 :: nil) (a2 :: b2 :: nil) →
 (a1=a2 ∧ b1=b2) ∨ (a1=b2 ∧ a2=b1).
Proof.
intros a1 b1 a2 b2 P; elim (cons_permut_in P).
intro; subst a2; left; split; trivial.
apply list_permut_length_1; apply remove_context_list_permut_cons with a1; trivial.
intro H; elim H; clear H.
intro; subst b2; right; split; trivial.
apply sym_eq; apply list_permut_length_1;
apply (list_permut_remove_hd (a2 :: nil) nil P).
intro; contradiction.
Qed.

Lemma ac_syntactic_aux :
 ∀ (l1 l2 l3 l4 : list elt),
 list_permut (l1 ++ l2) (l3 ++ l4) →
 (∃ u1, ∃ u2, ∃ u3, ∃ u4,
 list_permut l1 (u1 ++ u2) ∧
 list_permut l2 (u3 ++ u4) ∧
 list_permut l3 (u1 ++ u3) ∧
 list_permut l4 (u2 ++ u4)).
Proof.
induction l1.
intros l2 l3 l4 P;
∃ (nil : list elt); ∃ (nil : list elt); ∃ l3; ∃ l4;
simpl; intuition.

intros l2 l3 l4 P; rewrite <- app_comm_cons in P;
elim (in_app_or l3 l4 a (cons_permut_in P)); intro In_a;
generalize (split_list_app_cons eq_elt_dec a _ In_a).
destruct (split_list eq_elt_dec l3 a); intro; subst l3;
rewrite app_ass in P; rewrite <- app_comm_cons in P;
generalize (list_permut_remove_hd _ _ P); clear P;
intro P; rewrite <- app_ass in P;
elim (IHl1 l2 (l ++ l0) l4 P); clear IHl1 P;
intros u1 H; elim H; clear H;
intros u2 H; elim H; clear H;
intros u3 H; elim H; clear H;
intros u4 P; elim P; clear P;
intros P1 P; elim P; clear P;
intros P2 P; elim P; clear P;
intros P3 P4;
∃ (a :: u1); ∃ u2; ∃ u3; ∃ u4; intuition; simpl; trivial.
apply context_list_permut_cons; trivial.
apply list_permut_sym; apply list_permut_add_cons_inside;
apply list_permut_sym; trivial.

destruct (split_list eq_elt_dec l4 a); intro; subst l4;
rewrite <- app_ass in P;
generalize (list_permut_remove_hd _ _ P); clear P;
intro P; rewrite app_ass in P;
elim (IHl1 l2 l3 (l ++ l0) P); clear IHl1 P;
intros u1 H; elim H; clear H;
intros u2 H; elim H; clear H;
intros u3 H; elim H; clear H;
intros u4 P; elim P; clear P;
intros P1 P; elim P; clear P;
intros P2 P; elim P; clear P;
intros P3 P4;
∃ u1; ∃ (a :: u2); ∃ u3; ∃ u4; intuition; simpl; trivial.
apply list_permut_add_cons_inside; trivial.
apply list_permut_sym; apply list_permut_add_cons_inside;
apply list_permut_sym; trivial.
Qed.

Lemma ac_syntactic :
 ∀ (l1 l2 l3 l4 : list elt),
 list_permut (l2 ++ l1) (l4 ++ l3) →
 (∃ u1, ∃ u2, ∃ u3, ∃ u4,
 list_permut l1 (u1 ++ u2) ∧
 list_permut l2 (u3 ++ u4) ∧
 list_permut l3 (u1 ++ u3) ∧
 list_permut l4 (u2 ++ u4)).
Proof.
intros l1 l2 l3 l4 P; apply ac_syntactic_aux.
apply list_permut_trans with (l2 ++ l1).
apply list_permut_app_app.
apply list_permut_trans with (l4 ++ l3); trivial.
apply list_permut_app_app.
Qed.

Lemma list_permut_dec : ∀ l1 l2, {list_permut l1 l2}+{¬list_permut l1 l2}.
Proof.
intro l1; induction l1 as [ | e1 l1].
destruct l2 as [ | e2 l2].
left; apply list_permut_refl.
right; intro P; assert (H := list_permut_length P); discriminate.
intro l2; destruct (In_dec eq_elt_dec e1 l2) as [e1_in_l2 | e1_not_in_l2].
generalize (split_list_app_cons eq_elt_dec _ _ e1_in_l2); clear e1_in_l2;
destruct (split_list eq_elt_dec l2 e1) as [l2' l2'']; intro; subst.
destruct (IHl1 (l2' ++ l2'')) as [P | nP].
left; apply list_permut_add_cons_inside; trivial.
right; intro P; apply nP; apply list_permut_remove_hd with e1; trivial.
right; intro P; apply e1_not_in_l2; apply in_permut_in with (e1 :: l1); trivial;
left; trivial.
Qed.

End Make.