1 files changed, 300 insertions, 0 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
new file mode 100644
index 00000000..811dcab4
--- /dev/null
+++ b/theories/Lists/SetoidList.v
@@ -0,0 +1,300 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id: SetoidList.v 8686 2006-04-06 13:25:10Z letouzey $ *)
+
+Require Export List.
+Require Export Sorting.
+Require Export Setoid.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Logical relations over lists with respect to a setoid equality 
+      or ordering. *) 
+
+(** This can be seen as a complement of predicate [lelistA] and [sort] 
+    found in [Sorting]. *)
+
+Section Type_with_equality.
+Variable A : Set.
+Variable eqA : A -> A -> Prop. 
+
+(** Being in a list modulo an equality relation over type [A]. *)
+
+Inductive InA (x : A) : list A -> Prop :=
+  | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
+  | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
+
+Hint Constructors InA.
+
+(** An alternative definition of [InA]. *)
+
+Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
+Proof. 
+ induction l; intuition.
+ inversion H.
+ firstorder.
+ inversion H1; firstorder.
+ firstorder; subst; auto.
+Qed.
+
+(** A list without redundancy modulo the equality over [A]. *)
+
+Inductive NoDupA : list A -> Prop :=
+  | NoDupA_nil : NoDupA nil
+  | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
+
+Hint Constructors NoDupA.
+
+(** lists with same elements modulo [eqA] *)
+
+Definition eqlistA l l' := forall x, InA x l <-> InA x l'.
+
+(** Results concerning lists modulo [eqA] *)
+
+Hypothesis eqA_refl : forall x, eqA x x.
+Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
+Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+
+Hint Resolve eqA_refl eqA_trans.
+Hint Immediate eqA_sym.
+
+Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
+Proof. 
+ intros s x y.
+ do 2 rewrite InA_alt.
+ intros H (z,(U,V)).  
+ exists z; split; eauto.
+Qed.
+Hint Immediate InA_eqA.
+
+Lemma In_InA : forall l x, In x l -> InA x l.
+Proof.
+ simple induction l; simpl in |- *; intuition.
+ subst; auto.  
+Qed.
+Hint Resolve In_InA.
+
+(** Results concerning lists modulo [eqA] and [ltA] *)
+
+Variable ltA : A -> A -> Prop.
+
+Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z.
+Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y.
+Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
+Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.
+
+Hint Resolve ltA_trans.
+Hint Immediate ltA_eqA eqA_ltA.
+
+Notation InfA:=(lelistA ltA).
+Notation SortA:=(sort ltA).
+
+Lemma InfA_ltA :
+ forall l x y, ltA x y -> InfA y l -> InfA x l.
+Proof.
+ intro s; case s; constructor; inversion_clear H0.
+ eapply ltA_trans; eauto.
+Qed.
+ 
+Lemma InfA_eqA :
+ forall l x y, eqA x y -> InfA y l -> InfA x l.
+Proof.
+ intro s; case s; constructor; inversion_clear H0; eauto.
+Qed.
+Hint Immediate InfA_ltA InfA_eqA. 
+
+Lemma SortA_InfA_InA :
+ forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
+Proof. 
+ simple induction l.
+ intros; inversion H1.
+ intros.
+ inversion_clear H0; inversion_clear H1; inversion_clear H2.
+ eapply ltA_eqA; eauto.
+ eauto.
+Qed.
+  
+Lemma In_InfA :
+ forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl in |- *; intros; constructor; auto.
+Qed.
+ 
+Lemma InA_InfA :
+ forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
+Proof.
+ simple induction l; simpl in |- *; intros; constructor; auto.
+Qed.
+
+(* In fact, this may be used as an alternative definition for InfA: *)
+
+Lemma InfA_alt : 
+ forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
+Proof. 
+split.
+intros; eapply SortA_InfA_InA; eauto.
+apply InA_InfA.
+Qed.
+
+Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
+Proof.
+ simple induction l; auto.
+ intros x l' H H0.
+ inversion_clear H0.
+ constructor; auto.  
+ intro.
+ assert (ltA x x) by eapply SortA_InfA_InA; eauto.
+ elim (ltA_not_eqA H3); auto.
+Qed.
+
+Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> 
+  (forall x, InA x l -> InA x l' -> False) -> 
+  NoDupA (l++l').
+Proof.
+induction l; simpl; auto; intros.
+inversion_clear H.
+constructor.
+rewrite InA_alt; intros (y,(H4,H5)).
+destruct (in_app_or _ _ _ H5).
+elim H2.
+rewrite InA_alt.
+exists y; auto.
+apply (H1 a).
+auto.
+rewrite InA_alt.
+exists y; auto.
+apply IHl; auto.
+intros.
+apply (H1 x); auto.
+Qed.
+
+
+Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
+Proof.
+induction l.
+simpl; auto.
+simpl; intros.
+inversion_clear H.
+apply NoDupA_app; auto.
+constructor; auto.
+intro H2; inversion H2.
+intros x.
+rewrite InA_alt.
+intros (x1,(H2,H3)).
+inversion_clear 1.
+destruct H0.
+apply InA_eqA with x1; eauto.
+apply In_InA.
+rewrite In_rev; auto.
+inversion H4.
+Qed.
+
+
+Lemma InA_app : forall l1 l2 x,
+ InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H; auto.
+ elim (IHl1 l2 x H0); auto.
+Qed.
+
+ Hint Constructors lelistA sort.
+
+Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
+Proof.
+ induction l1; simpl; auto.
+ inversion_clear 1; auto.
+Qed.
+
+Lemma SortA_app :
+ forall l1 l2, SortA l1 -> SortA l2 ->
+ (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
+ SortA (l1 ++ l2).
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H.
+ constructor; auto.
+ apply InfA_app; auto.
+ destruct l2; auto.
+Qed.
+
+Section Remove.
+
+Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
+
+Fixpoint removeA (x : A) (l : list A){struct l} : list A :=
+  match l with
+    | nil => nil
+    | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
+  end.
+
+Lemma removeA_filter : forall x l, 
+  removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
+Proof.
+induction l; simpl; auto.
+destruct (eqA_dec x a); auto.
+rewrite IHl; auto.
+Qed.
+
+Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
+Proof.
+induction l; simpl; auto.
+split.
+inversion_clear 1.
+destruct 1; inversion_clear H.
+intros.
+destruct (eqA_dec x a); simpl; auto.
+rewrite IHl; split; destruct 1; split; auto.
+inversion_clear H; auto.
+destruct H0; apply eqA_trans with a; auto.
+split.
+inversion_clear 1.
+split; auto.
+swap n.
+apply eqA_trans with y; auto.
+rewrite (IHl x y) in H0; destruct H0; auto.
+destruct 1; inversion_clear H; auto.
+constructor 2; rewrite IHl; auto.
+Qed.
+
+Lemma removeA_NoDupA :
+  forall s x, NoDupA s ->  NoDupA (removeA x s).
+Proof.
+simple induction s; simpl; intros.
+auto.
+inversion_clear H0.
+destruct (eqA_dec x a); simpl; auto. 
+constructor; auto.
+rewrite removeA_InA.
+intuition.
+Qed. 
+
+Lemma removeA_eqlistA : forall l l' x, 
+  ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l').
+Proof.  
+unfold eqlistA; intros. 
+rewrite removeA_InA.
+split; intros.
+rewrite <- H0; split; auto.
+swap H.
+apply InA_eqA with x0; auto.
+rewrite <- (H0 x0) in H1.
+destruct H1.
+inversion_clear H1; auto.
+elim H2; auto.
+Qed.
+
+End Remove.
+
+End Type_with_equality.
+
+Hint Constructors InA.
+Hint Constructors NoDupA. 
+Hint Constructors sort.
+Hint Constructors lelistA.