Duplication du fichier FSetProperties pour les ensembles Weak.

Du coup, factorisation d'une partie dans SetoidList. Ajout de 
lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface 
concernant elements. 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 143 insertions, 0 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index a25b83fc8..726f569d6 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -290,6 +290,149 @@ inversion_clear H1; auto.
 elim H2; auto.
 Qed.
 
+Let addlistA x l l' := forall y, InA y l' <-> eqA x y \/ InA y l.
+
+Lemma removeA_add :
+  forall s s' x x', NoDupA s -> NoDupA (x' :: s') ->
+  ~ eqA x x' -> ~ InA x s -> 
+  addlistA x s (x' :: s') -> addlistA x (removeA x' s) s'.
+Proof.
+unfold addlistA; intros.
+inversion_clear H0.
+rewrite removeA_InA; auto.
+split; intros.
+destruct (eqA_dec x y); auto; intros.
+right; split; auto.
+destruct (H3 y); clear H3.
+destruct H6; intuition.
+swap H4; apply InA_eqA with y; auto.
+destruct H0.
+assert (InA y (x' :: s')) by rewrite H3; auto.
+inversion_clear H6; auto.
+elim H1; apply eqA_trans with y; auto.
+destruct H0.
+assert (InA y (x' :: s')) by rewrite H3; auto.
+inversion_clear H7; auto.
+elim H6; auto.
+Qed.
+
+Section Fold.
+
+Variable B:Set.
+Variable eqB:B->B->Prop.
+
+(** Two-argument functions that allow to reorder its arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
+
+(** Compatibility of a two-argument function with respect to two equalities. *)
+Definition compat_op (f : A -> B -> B) :=
+  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
+
+(** Compatibility of a function upon natural numbers. *)
+Definition compat_nat (f : A -> nat) :=
+  forall x x' : A, eqA x x' -> f x = f x'.
+
+Variable st:Setoid_Theory _ eqB.
+Variable f:A->B->B.
+Variable Comp:compat_op f.
+Variable Ass:transpose f.
+Variable i:B.
+
+Lemma removeA_fold_right_0 :
+  forall s x, ~InA x s ->
+  eqB (fold_right f i s) (fold_right f i (removeA x s)).
+Proof.
+ simple induction s; simpl; intros.
+ refl_st.
+ destruct (eqA_dec x a); simpl; intros.
+ absurd_hyp e; auto.
+ apply Comp; auto. 
+Qed.   
+
+Lemma removeA_fold_right :
+  forall s x, NoDupA s -> InA x s ->
+  eqB (fold_right f i s) (f x (fold_right f i (removeA x s))).
+Proof.
+ simple induction s; simpl.  
+ inversion_clear 2.
+ intros.
+ inversion_clear H0.
+ destruct (eqA_dec x a); simpl; intros.
+ apply Comp; auto. 
+ apply removeA_fold_right_0; auto.
+ swap H2; apply InA_eqA with x; auto.
+ inversion_clear H1. 
+ destruct n; auto.
+ trans_st (f a (f x (fold_right f i (removeA x l)))).
+Qed.   
+
+Lemma fold_right_equal :
+  forall s s', NoDupA s -> NoDupA s' ->
+  eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
+Proof.
+ simple induction s.
+ destruct s'; simpl.
+ intros; refl_st; auto.
+ unfold eqlistA; intros.
+ destruct (H1 a).
+ assert (X : InA a nil); auto; inversion X.
+ intros x l Hrec s' N N' E; simpl in *.
+ trans_st (f x (fold_right f i (removeA x s'))).
+ apply Comp; auto.
+ apply Hrec; auto.
+ inversion N; auto.
+ apply removeA_NoDupA; auto; apply eqA_trans.
+ apply removeA_eqlistA; auto.
+ inversion_clear N; auto.
+ sym_st.
+ apply removeA_fold_right; auto.
+ unfold eqlistA in E.
+ rewrite <- E; auto.
+Qed.
+
+Lemma fold_right_add :
+  forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
+  addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)).
+Proof.   
+ simple induction s'.
+ unfold addlistA; intros.
+ destruct (H2 x); clear H2.
+ assert (X : InA x nil); auto; inversion X.
+ intros x' l' Hrec s x N N' IN EQ; simpl.
+ (* if x=x' *)
+ destruct (eqA_dec x x').
+ apply Comp; auto.
+ apply fold_right_equal; auto.
+ inversion_clear N'; trivial.
+ unfold eqlistA; unfold addlistA in EQ; intros.
+ destruct (EQ x0); clear EQ.
+ split; intros.
+ destruct H; auto.
+ inversion_clear N'.
+ destruct H2; apply InA_eqA with x0; auto.
+ apply eqA_trans with x; auto.
+ assert (X:InA x0 (x' :: l')); auto; inversion_clear X; auto.
+ destruct IN; apply InA_eqA with x0; auto.
+ apply eqA_trans with x'; auto.
+ (* else x<>x' *)   
+ trans_st (f x' (f x (fold_right f i (removeA x' s)))).
+ apply Comp; auto.
+ apply Hrec; auto.
+ apply removeA_NoDupA; auto; apply eqA_trans.
+ inversion_clear N'; auto.
+ rewrite removeA_InA; intuition.
+ apply removeA_add; auto.
+ trans_st (f x (f x' (fold_right f i (removeA x' s)))).
+ apply Comp; auto.
+ sym_st.
+ apply removeA_fold_right; auto.
+ destruct (EQ x'). 
+ destruct H; auto; destruct n; auto.
+Qed.
+
+End Fold.
+
 End Remove.
 
 End Type_with_equality.