(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(***********************************************************************
      UList.v                                                                                       
                                                                                                         
      Definition of list with distinct elements                                 
                                                                                                         
      Definition: ulist                                                                         
                                                                                                         
                                     Laurent.Thery@inria.fr (2006)                
************************************************************************)
(* Modified a little bit by Sunil Kothari for usage with mgu_axioms.v *)

Require Import List.
Require Import Arith.
Require Import Permutation.

 
Section UniqueList.
Variable D : Set.
Variable eqD_dec : forall (a b : D),  ({ a = b }) + ({ a <> b }).
(* A list is unique if there is not twice the same element in the list *)
 
(*
Inductive ulist : list D ->  Prop :=
  ulist_nil: ulist nil
 | ulist_cons: forall a l, ~ In a l -> ulist l ->  ulist (a :: l) .
Hint Constructors ulist .
*)
(* Inversion theorem *)
 Set Implicit Arguments.

Theorem ulist_inv: forall a:D, forall l:list D, NoDup (a :: l) ->  NoDup l.
intros a l H; inversion H; auto.
Qed.
(* The append of two unique list is unique if the list are distinct *)
 
Theorem ulist_app:
 forall l1 l2,
 NoDup l1 ->
 NoDup l2 -> (forall (a : D), In a l1 -> In a l2 ->  False) ->  NoDup (l1 ++ l2).
intros L1; elim L1; simpl; auto.
intros a l H l2 H0 H1 H2; apply NoDup_cons; simpl; auto.
red; intros H3; case in_app_or with ( 1 := H3 ); auto; intros H4.
inversion H0; auto.
apply H2 with a; auto.
apply H; auto.
apply ulist_inv with ( 1 := H0 ); auto.
intros a0 H3 H4; apply (H2 a0); auto.
Qed.
(* Iinversion theorem the appended list *)
 
Theorem ulist_app_inv:
 forall l1 l2 (a : D), NoDup (l1 ++ l2) -> In a l1 -> In a l2 ->  False.
intros l1; elim l1; simpl; auto.
intros a l H l2 a0 H0 [H1|H1] H2.
inversion H0 as [|a1 l0 H3 H4 H5]; auto.
case H4; rewrite H1; auto with datatypes.
apply (H l2 a0); auto.
apply ulist_inv with ( 1 := H0 ); auto.
Qed.
(* Iinversion theorem the appended list *)
 
Theorem ulist_app_inv_l: forall (l1 l2 : list D), NoDup (l1 ++ l2) ->  NoDup l1.
Proof.
intros l1; elim l1; simpl; auto.
intros.
apply NoDup_nil.
intros a l H l2 H0.
inversion H0 as [|il1 iH1 iH2 il2 [iH4 iH5]]; apply NoDup_cons; auto.
intros H5; case iH2; auto with datatypes.
apply H with l2; auto.
Qed.


 
Theorem ulist_app_inv_r: forall (l1 l2 : list D), NoDup (l1 ++ l2) ->  NoDup l2.
intros l1; elim l1; simpl; auto.
intros a l H l2 H0; inversion H0; auto.
Qed.
(* Uniqueness is decidable *)
 Hint Constructors NoDup.

Definition ulist_dec: forall l:list D,  ({ NoDup l }) + ({ ~ NoDup l }).
Proof.
intros l; elim l; auto.
intros a l1 [H|H]; auto.
case (In_dec eqD_dec a l1); intros H2; auto.
right; red; intros H1; inversion H1; auto.
right; intros H1; case H; apply ulist_inv with ( 1 := H1 ).
Defined.
(* Uniqueness is compatible with permutation *)
 
Theorem ulist_perm:
 forall (l1 l2 : list D), Permutation l1 l2 -> NoDup l1 ->  NoDup l2.
intros l1 l2 H; elim H; clear H l1 l2; simpl; auto.
intros a l1 l2 H0 H1 H2; apply NoDup_cons; auto.
inversion_clear H2 as [|ia il iH1 iH2 [iH3 iH4]]; auto.
intros H3. case iH1.
apply Permutation_in with (l:= l2)(l':= l1)(x:=a).
apply Permutation_sym.
auto.
auto.
(*
apply Permutation_in with ( 1 := Permutation_sym _ _ _ H0 ); auto. *)
inversion H2; auto.
intros a b L H0; apply NoDup_cons; auto.
inversion_clear H0 as [|ia il iH1 iH2]; auto.
inversion_clear iH2 as [|ia il iH3 iH4]; auto.
intros H; case H; auto.
intros H1; case iH1; rewrite H1; simpl; auto.
apply NoDup_cons; auto.
inversion_clear H0 as [|ia il iH1 iH2]; auto.
intros H; case iH1; simpl; auto.
inversion_clear H0 as [|ia il iH1 iH2]; auto.
inversion iH2; auto.
Qed.
 
Theorem ulist_def:
 forall l:list D, forall a:D,
 In a l -> NoDup l ->  ~ (exists l1 , Permutation l (a :: (a :: l1)) ).
intros l a H H0 [l1 H1].
absurd (NoDup (a :: (a :: l1))); auto.
intros H2; inversion_clear H2; simpl; auto with datatypes.
apply ulist_perm with ( 1 := H1 ); auto.
Qed.

Theorem in_permutation_ex: forall a l, In a l -> exists l1: list D, Permutation (a::l1) l.
Proof.

intros a l; elim l; simpl in |- *; auto.
intros H; case H; auto.
intros a0 l0 H [H0|H0].
exists l0; rewrite H0; auto.
subst.
apply Permutation_refl.
assert (In a l0).
auto.
apply  H in H0.
elim H0.
intros.
exists (a0::x).
apply perm_skip with (x:=a0) in H2.
apply Permutation_sym in H2.
apply Permutation_sym.
apply perm_trans with (l' := a0::a::x).
auto.
apply perm_swap.
Qed.


Theorem ulist_incl_permutation:
 forall (l1 l2 : list D),
 NoDup l1 -> incl l1 l2 ->  (exists l3 , Permutation l2 (l1 ++ l3) ).
intros l1; elim l1; simpl; auto.
intros l2 H H0; exists l2; simpl; auto.
apply Permutation_refl.
intros a l H l2 H0 H1; auto.
case (in_permutation_ex a l2). auto with datatypes.
intros l3 Hl3.
case (H l3); auto.
apply ulist_inv with ( 1 := H0 ); auto.
intros b Hb.
assert (H2: In b (a :: l3)).
apply Permutation_in with ( 1 := Permutation_sym   Hl3 );
 auto with datatypes.
simpl in H2 |-; case H2; intros H3; simpl; auto.
inversion_clear H0 as [|c lc Hk1]; auto.
case Hk1; subst a; auto.
intros l4 H4; exists l4.
apply Permutation_trans with (a :: l3); auto.
apply Permutation_sym; auto.
apply perm_skip.
auto.
Qed.
 

Theorem ulist_eq_permutation:
 forall (l1 l2 : list D),
 NoDup l1 -> incl l1 l2 -> length l1 = length l2 ->  Permutation l1 l2.
Proof.
intros l1 l2 H1 H2 H3.
apply ulist_incl_permutation with (l2:= l2) in H1.
elim H1.
intros.
assert (H5: x = @nil D).
apply Permutation_length in H.
rewrite app_length in H.
rewrite H3 in H.
pattern (length l2) at 1 in H.
rewrite plus_n_O   with (n:= length l2)  in H.

SearchAbout plus.
apply plus_reg_l in H.
symmetry in H.
generalize H.
case x.
intros;reflexivity.
intros.
inversion H0.
subst.
rewrite <- app_nil_end in H.
apply Permutation_sym in H.
auto.
auto.
Qed.
 

Theorem ulist_incl_length:
 forall (l1 l2 : list D), NoDup l1 -> incl l1 l2 ->  le (length l1) (length l2).
intros l1 l2 H1 Hi; case ulist_incl_permutation with ( 2 := Hi ); auto.
intros l3 Hl3; rewrite Permutation_length with ( 1 := Hl3 ); auto.
rewrite app_length; simpl; auto with arith.
Qed.

Theorem ulist_incl2_permutation:
 forall (l1 l2 : list D),
 NoDup l1 -> NoDup l2 -> incl l1 l2 -> incl l2 l1  ->  Permutation l1 l2.
intros l1 l2 H1 H2 H3 H4.
apply ulist_eq_permutation; auto.
apply le_antisym; apply ulist_incl_length; auto.
Qed.
 
 
Theorem ulist_incl_length_strict:
 forall (l1 l2 : list D),
 NoDup l1 -> incl l1 l2 -> ~ incl l2 l1 ->  lt (length l1) (length l2).
intros l1 l2 H1 Hi Hi0; case ulist_incl_permutation with ( 2 := Hi ); auto.
intros l3 Hl3; rewrite Permutation_length with ( 1 := Hl3 ); auto.
rewrite app_length; simpl; auto with arith.
generalize Hl3; case l3; simpl; auto with arith.
rewrite <- app_nil_end; auto.
intros H2; case Hi0; auto.
intros a HH; apply Permutation_in with ( 1 := H2 ); auto.
intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith).
Qed.
 
Theorem in_inv_dec:
 forall (a b : D) l, In a (cons b l) ->  a = b \/ ~ a = b /\ In a l.
intros a b l H; case (eqD_dec a b); auto; intros H1.
right; split; auto; inversion H; auto.
case H1; auto.
Qed.
 
Theorem in_ex_app_first:
 forall (a : D) (l : list D),
 In a l ->
  (exists l1 : list D , exists l2 : list D , l = l1 ++ (a :: l2) /\ ~ In a l1  ).
intros a l; elim l; clear l; auto.
intros H; case H.
intros a1 l H H1; auto.
generalize (in_inv_dec   H1); intros [H2|[H2 H3]].
exists (nil (A:=D)); exists l; simpl; split; auto.
f_equal; auto.
case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl;
 split; auto.
f_equal; auto.
intros H4; case H4; auto.
Qed.
 (*
Theorem ulist_inv_ulist:
 forall (l : list B),
 ~ ulist l ->
  (exists a ,
   exists l1 ,
   exists l2 ,
   exists l3 , l = l1 ++ ((a :: l2) ++ (a :: l3)) /\ ulist (l1 ++ (a :: l2))    ).
intros l; elim l  using list_length_ind; clear l.
intros l; case l; simpl; auto; clear l.
intros Rec H0; case H0; auto.
intros a l H H0.
case (In_dec eqA_dec a l); intros H1; auto.
case in_ex_app_first with ( 1 := H1 ); intros l1 [l2 [Hl1 Hl2]]; subst l.
case (ulist_dec l1); intros H2.
exists a; exists (@nil B); exists l1; exists l2; split; auto.
simpl; apply ulist_cons; auto.
case (H l1); auto.
rewrite length_app; auto with arith.
intros b [l3 [l4 [l5 [Hl3 Hl4]]]]; subst l1.
exists b; exists (a :: l3); exists l4; exists (l5 ++ (a :: l2)); split; simpl;
 auto.
(repeat (rewrite <- ass_app; simpl)); auto.
apply ulist_cons; auto.
contradict Hl2; auto.
replace (l3 ++ (b :: (l4 ++ (b :: l5)))) with ((l3 ++ (b :: l4)) ++ (b :: l5));
 auto with datatypes.
(repeat (rewrite <- ass_app; simpl)); auto.
case (H l); auto; intros a1 [l1 [l2 [l3 [Hl3 Hl4]]]]; subst l.
exists a1; exists (a :: l1); exists l2; exists l3; split; auto.
simpl; apply ulist_cons; auto.
contradict H1.
replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3))))
     with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes.
(repeat (rewrite <- ass_app; simpl)); auto.
Qed.
 
Theorem incl_length_repetition:
 forall (l1 l2 : list B),
 incl l1 l2 ->
 lt (length l2) (length l1) ->
  (exists a ,
   exists ll1 ,
   exists ll2 ,
   exists ll3 ,
   l1 = ll1 ++ ((a :: ll2) ++ (a :: ll3)) /\ ulist (ll1 ++ (a :: ll2))    ).
intros l1 l2 H H0; apply ulist_inv_ulist.
intros H1; absurd (le (length l1) (length l2)); auto with arith.
apply ulist_incl_length; auto.
Qed.
 
Theorem nth_ulist: forall a i j (l: list B), i < length l -> j < length l ->
    ulist l -> nth i l a = nth j l a -> i = j.
intros a i j l; generalize i j; elim l; simpl; clear l i j.
intros i j H; contradict H; auto with arith.
intros b l1 Rec i j; case i; case j; auto with arith; clear i j.
intros j _ H1 H2 H3; absurd (In b l1); auto.
inversion H2; auto.
subst; apply nth_In; auto with arith.
intros i H1 _ H2 H3; absurd (In b l1); auto.
inversion H2; auto.
subst; apply nth_In; auto with arith.
intros j i H1 H2 H3 H4; inversion H3; auto with arith.
Qed.
*)

End UniqueList.

(*
Implicit Arguments ulist [A].
Hint Constructors ulist .
 

Theorem ulist_map:
 forall (A B : Set) (f : A ->  B) l,
 (forall x y, (In x l) -> (In y l) ->  f x = f y ->  x = y) -> ulist l ->  ulist (map f l).
intros a b f l Hf Hl; generalize Hf; elim Hl; clear Hf;  auto.
simpl; auto.
intros a1 l1 H1 H2 H3 Hf; simpl.
apply ulist_cons; auto with datatypes.
contradiction H1.
case in_map_inv with ( 1 := H1 ); auto.
intros b1 [Hb1 Hb2].
replace a1 with b1; auto with datatypes.
Qed.
 
Theorem ulist_list_prod:
 forall (A : Set) (l1 l2 : list A),
 ulist l1 -> ulist l2 ->  ulist (list_prod l1 l2).
intros A l1 l2 Hl1 Hl2; elim Hl1; simpl; auto.
intros a l H1 H2 H3; apply ulist_app; auto.
apply ulist_map; auto.
intros x y _ _ H; inversion H; auto.
intros p Hp1 Hp2; case H1.
case in_map_inv with ( 1 := Hp1 ); intros a1 [Ha1 Ha2]; auto.
case in_list_prod_inv with ( 1 := Hp2 ); intros b1 [c1 [Hb1 [Hb2 Hb3]]]; auto.
replace a with b1; auto.
rewrite Ha2 in Hb1; injection Hb1; auto.
Qed.
*)