(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id$ i*)

Require Import Omega Relations Multiset Permutation SetoidList.

Set Implicit Arguments.

(** This file contains additional results about permutations
     with respect to a setoid equality (i.e. an equivalence relation).
*)

Section Perm.

Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.

Notation permutation := (permutation _ eqA_dec).
Notation list_contents := (list_contents _ eqA_dec).

(** we can use [multiplicity] to define [InA] and [NoDupA]. *)

Fact if_eqA_then : forall a a' (B:Type)(b b':B),
 eqA a a' -> (if eqA_dec a a' then b else b') = b.
Proof.
  intros. destruct eqA_dec as [_|NEQ]; auto.
  contradict NEQ; auto.
Qed.

Fact if_eqA_else : forall a a' (B:Type)(b b':B),
 ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
Proof.
  intros. decide (eqA_dec a a') with H; auto.
Qed.

Fact if_eqA_refl : forall a (B:Type)(b b':B),
 (if eqA_dec a a then b else b') = b.
Proof.
  intros; apply (decide_left (eqA_dec a a)); auto with *.
Qed.

(** PL: Inutilisable dans un rewrite sans un change prealable. *)

Global Instance if_eqA (B:Type)(b b':B) :
 Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
Proof.
 intros B b b' x x' Hxx' y y' Hyy'.
 intros; destruct (eqA_dec x y) as [H|H];
  destruct (eqA_dec x' y') as [H'|H']; auto.
 contradict H'; transitivity x; auto with *; transitivity y; auto with *.
 contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
Qed.

Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
 eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1' a2 then b else b').
Proof.
 intros; destruct (eqA_dec a1 a2) as [A1|A1];
  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
 contradict A1'; transitivity a1; eauto with *.
 contradict A1; transitivity a1'; eauto with *.
Qed.

Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
 eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
               (if eqA_dec a1 a2' then b else b').
Proof.
 intros; destruct (eqA_dec a1 a2) as [A2|A2];
  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
 contradict A2'; transitivity a2; eauto with *.
 contradict A2; transitivity a2'; eauto with *.
Qed.


Global Instance multiplicity_eqA (l:list A) :
 Proper (eqA==>@eq _) (multiplicity (list_contents l)).
Proof.
  intros l x x' Hxx'.
  induction l as [|y l Hl]; simpl; auto.
  rewrite (@if_eqA_rewrite_r y x x'); auto.
Qed.

Lemma multiplicity_InA :
  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
Proof.
  induction l.
  simpl.
  split; inversion 1.
  simpl.
  intros a'; split; intros H. inversion_clear H.
  apply (decide_left (eqA_dec a a')); auto with *.
  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
Qed.

Lemma multiplicity_InA_O :
  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
Proof.
  intros l a; rewrite multiplicity_InA;
    destruct (multiplicity (list_contents l) a); auto with arith.
  destruct 1; auto with arith.
Qed.

Lemma multiplicity_InA_S :
  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
Proof.
  intros l a; rewrite multiplicity_InA; auto with arith.
Qed.

Lemma multiplicity_NoDupA : forall l,
  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
Proof.
  induction l.
  simpl.
  split; auto with arith.
  split; simpl.
  inversion_clear 1.
  rewrite IHl in H1.
  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
  rewrite <- EQ.
  rewrite multiplicity_InA_O; auto.
  intros; constructor.
  rewrite multiplicity_InA.
  specialize (H a).
  rewrite if_eqA_refl in H.
  clear IHl; omega.
  rewrite IHl; intros.
  specialize (H a0); auto with *.
  destruct (eqA_dec a a0); simpl; auto with *.
Qed.


(** Permutation is compatible with InA. *)
Lemma permut_InA_InA :
  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
Proof.
  intros l1 l2 e.
  do 2 rewrite multiplicity_InA.
  unfold Permutation.permutation, meq.
  intros H;rewrite H; auto.
Qed.

Lemma permut_cons_InA :
  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
Proof.
  intros; apply (permut_InA_InA (e:=e) H); auto with *.
Qed.

(** Permutation of an empty list. *)
Lemma permut_nil :
  forall l, permutation l nil -> l = nil.
Proof.
  intro l; destruct l as [ | e l ]; trivial.
  assert (InA eqA e (e::l)) by (auto with *).
  intro Abs; generalize (permut_InA_InA Abs H).
  inversion 1.
Qed.

(** Permutation for short lists. *)

Lemma permut_length_1:
  forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
Proof.
  intros a b; unfold Permutation.permutation, meq.
  intro P; specialize (P b); simpl in *.
  rewrite if_eqA_refl in *.
  destruct (eqA_dec a b); simpl; auto; discriminate.
Qed.

Lemma permut_length_2 :
  forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
Proof.
  intros a1 b1 a2 b2 P.
  assert (H:=permut_cons_InA P).
  inversion_clear H.
  left; split; auto.
  apply permut_length_1.
  red; red; intros.
  specialize (P a). simpl in *.
  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto.
  (** Bug omega: le "set" suivant ne devrait pas etre necessaire *)
  set (u:= if eqA_dec a2 a then 1 else 0) in *; omega.
  right.
  inversion_clear H0; [|inversion H].
  split; auto.
  apply permut_length_1.
  red; red; intros.
  specialize (P a); simpl in *.
  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto.
  (** Bug omega: idem *)
  set (u:= if eqA_dec b2 a then 1 else 0) in *; omega.
Qed.

(** Permutation is compatible with length. *)
Lemma permut_length :
  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
Proof.
  induction l1; intros l2 H.
  rewrite (permut_nil (permut_sym H)); auto.
  assert (H0:=permut_cons_InA H).
  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
  subst l2.
  rewrite app_length.
  simpl; rewrite <- plus_n_Sm; f_equal.
  rewrite <- app_length.
  apply IHl1.
  apply permut_remove_hd with b.
  apply permut_tran with (a::l1); auto.
  revert H1; unfold Permutation.permutation, meq; simpl.
  intros; f_equal; auto.
  rewrite (@if_eqA_rewrite_l a b a0); auto.
Qed.

Lemma NoDupA_equivlistA_permut :
  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
    equivlistA eqA l l' -> permutation l l'.
Proof.
  intros.
  red; unfold meq; intros.
  rewrite multiplicity_NoDupA in H, H0.
  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
  do 2 rewrite multiplicity_InA.
  destruct 3; omega.
Qed.


Variable B : Type.
Variable eqB : B->B->Prop.
Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Variable eqB_trans : Transitive eqB.


(** Permutation is compatible with map. *)

Lemma permut_map :
  forall f,
    (Proper (eqA==>eqB) f) ->
    forall l1 l2, permutation l1 l2 ->
      Permutation.permutation _ eqB_dec (map f l1) (map f l2).
Proof.
  intros f; induction l1.
  intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
  intros l2 P.
  simpl.
  assert (H0:=permut_cons_InA P).
  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
  subst l2.
  rewrite map_app.
  simpl.
  apply permut_tran with (f b :: map f l1).
  revert H1; unfold Permutation.permutation, meq; simpl.
  intros; f_equal; auto.
  destruct (eqB_dec (f b) a0) as [H2|H2];
    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
  destruct H3; transitivity (f b); auto with *.
  destruct H2; transitivity (f a); auto with *.
  apply permut_add_cons_inside.
  rewrite <- map_app.
  apply IHl1; auto.
  apply permut_remove_hd with b.
  apply permut_tran with (a::l1); auto.
  revert H1; unfold Permutation.permutation, meq; simpl.
  intros; f_equal; auto.
  rewrite (@if_eqA_rewrite_l a b a0); auto.
Qed.

End Perm.