some more properties of fold and elements in FSetProperties

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

3 files changed, 178 insertions, 12 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 3b8d0d708a..76448357a2 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -977,5 +977,94 @@ Module Properties (M: S).
   rewrite (cardinal_1 (min_elt_3 H)) in Heqn; inversion Heqn.
   Qed.  
 
+  Lemma elements_eqlistA_max : forall s s' x, 
+   Above x s -> Add x s s' -> 
+     eqlistA E.eq (elements s') (elements s ++ x::nil).
+  Proof.
+  intros.
+  eapply SortA_equivlistA_eqlistA; eauto.
+   apply E.lt_trans.
+   apply lt_eq.
+   apply eq_lt.
+  apply (@SortA_app E.t E.eq); auto.
+  intros.
+  inversion_clear H2.
+  rewrite <- elements_iff in H1.
+  apply lt_eq with x; auto.
+  inversion H3.
+  red; intros.
+  red in H0.
+  generalize (H0 x0); clear H0; intros.
+  do 2 rewrite elements_iff in H0.
+  rewrite H0; clear H0.
+  intuition.
+  rewrite InA_alt.
+  exists x; split; auto.
+  apply in_or_app; simpl; auto.
+  rewrite InA_alt in H1; destruct H1; intuition.
+  rewrite InA_alt; exists x1; split; auto; apply in_or_app; auto.
+  destruct (InA_app H0); auto.
+  inversion_clear H1; auto.
+  inversion H2.
+  Qed.
+
+  Lemma elements_eqlistA_min : forall s s' x, 
+   Below x s -> Add x s s' -> 
+     eqlistA E.eq (elements s') (x::elements s).
+  Proof.
+  intros.
+  eapply SortA_equivlistA_eqlistA; eauto.
+   apply E.lt_trans.
+   apply lt_eq.
+   apply eq_lt.
+  change (sort E.lt ((x::nil) ++ elements s)).
+  apply (@SortA_app E.t E.eq); auto.
+  intros.
+  inversion_clear H1.
+  rewrite <- elements_iff in H2.
+  apply eq_lt with x; auto.
+  inversion H3.
+  red; intros.
+  red in H0.
+  generalize (H0 x0); clear H0; intros.
+  do 2 rewrite elements_iff in H0.
+  rewrite H0; clear H0.
+  intuition.
+  inversion_clear H0; auto.
+  Qed.
+
+  Lemma fold_3 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
+  Proof.
+  intros.
+  do 2 rewrite M.fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  change (f x (fold_right f i (rev (elements s)))) with 
+    (fold_right f i (rev (x::nil)++rev (elements s))).
+  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
+  rewrite <- distr_rev.
+  apply eqlistA_rev.
+  apply elements_eqlistA_max; auto.
+  Qed.
+
+  Lemma fold_4 :
+   forall s s' x (A : Set) (eqA : A -> A -> Prop)
+     (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A),
+   compat_op E.eq eqA f ->
+   Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
+  Proof.
+  intros.
+  do 2 rewrite M.fold_1.
+  set (g:=fun (a : A) (e : elt) => f e a).
+  change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).
+  unfold g.
+  do 2 rewrite <- fold_left_rev_right.
+  apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
+  apply eqlistA_rev.
+  apply elements_eqlistA_min; auto.
+  Qed.
 
 End Properties.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 76d6ff1125..684d4ca731 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -53,7 +53,15 @@ Hint Constructors NoDupA.
 
 (** lists with same elements modulo [eqA] *)
 
-Definition eqlistA l l' := forall x, InA x l <-> InA x l'.
+Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
+
+(** lists with same elements modulo [eqA] at the same place *)
+
+Inductive eqlistA : list A -> list A -> Prop := 
+    | eqlistA_nil : eqlistA nil nil
+    | eqlistA_cons : forall x x' l l', 
+         eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
+Hint Constructors eqlistA.
 
 (** Results concerning lists modulo [eqA] *)
 
@@ -298,10 +306,10 @@ rewrite removeA_InA.
 intuition.
 Qed. 
 
-Lemma removeA_eqlistA : forall l l' x, 
-  ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l').
+Lemma removeA_equivlistA : forall l l' x, 
+  ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
 Proof.  
-unfold eqlistA; intros. 
+unfold equivlistA; intros. 
 rewrite removeA_InA.
 split; intros.
 rewrite <- H0; split; auto.
@@ -339,6 +347,66 @@ inversion_clear H7; auto.
 elim H6; auto.
 Qed.
 
+(** Some results about [eqlistA] *)
+
+Lemma eqlistA_app : forall l1 l1' l2 l2', 
+   eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
+Proof.
+intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto.
+Qed.
+
+Lemma eqlistA_rev_app : forall l1 l1', 
+   eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> 
+   eqlistA ((rev l1)++l2) ((rev l1')++l2').
+Proof.
+induction 1; auto.
+simpl; intros.
+do 2 rewrite app_ass; simpl; auto.
+Qed.
+
+Lemma eqlistA_rev : forall l1 l1', 
+   eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
+Proof.
+intros.
+rewrite (app_nil_end (rev l1)).
+rewrite (app_nil_end (rev l1')).
+apply eqlistA_rev_app; auto.
+Qed.
+
+Lemma SortA_equivlistA_eqlistA : forall l l', 
+   SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
+Proof.
+induction l; destruct l'; simpl; intros; auto.
+destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
+destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4.  
+inversion_clear H; inversion_clear H0.
+assert (forall y, InA y l -> ltA a y).
+intros; eapply SortA_InfA_InA with (l:=l); eauto.
+assert (forall y, InA y l' -> ltA a0 y).
+intros; eapply SortA_InfA_InA with (l:=l'); eauto.
+clear H3 H4.
+assert (eqA a a0).
+ destruct (H1 a).
+ destruct (H1 a0).
+ assert (InA a (a0::l')) by auto.
+ inversion_clear H8; auto.
+ assert (InA a0 (a::l)) by auto.
+ inversion_clear H8; auto.
+ elim (@ltA_not_eqA a a); auto.
+ apply ltA_trans with a0; auto.
+constructor; auto.
+apply IHl; auto.
+split; intros.
+destruct (H1 x).
+assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto. 
+elim (@ltA_not_eqA a x); eauto.
+destruct (H1 x).
+assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto. 
+elim (@ltA_not_eqA a0 x); eauto.
+Qed.
+
+
+
 Section Fold.
 
 Variable B:Set.
@@ -390,14 +458,14 @@ Proof.
  trans_st (f a (f x (fold_right f i (removeA x l)))).
 Qed.   
 
-Lemma fold_right_equal :
+Lemma fold_right_equivlistA :
   forall s s', NoDupA s -> NoDupA s' ->
-  eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
+  equivlistA 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.
+ unfold equivlistA; intros.
  destruct (H1 a).
  assert (X : InA a nil); auto; inversion X.
  intros x l Hrec s' N N' E; simpl in *.
@@ -406,14 +474,23 @@ Proof.
  apply Hrec; auto.
  inversion N; auto.
  apply removeA_NoDupA; auto; apply eqA_trans.
- apply removeA_eqlistA; auto.
+ apply removeA_equivlistA; auto.
  inversion_clear N; auto.
  sym_st.
  apply removeA_fold_right; auto.
- unfold eqlistA in E.
+ unfold equivlistA in E.
  rewrite <- E; auto.
 Qed.
 
+(* for this one, the transpose hyp is not required *)
+Lemma fold_right_eqlistA : 
+   forall s s', eqlistA s s' -> 
+   eqB (fold_right f i s) (fold_right f i s').
+Proof.
+induction 1; simpl; auto.
+refl_st.
+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)).
@@ -426,9 +503,9 @@ Proof.
  (* if x=x' *)
  destruct (eqA_dec x x').
  apply Comp; auto.
- apply fold_right_equal; auto.
+ apply fold_right_equivlistA; auto.
  inversion_clear N'; trivial.
- unfold eqlistA; unfold addlistA in EQ; intros.
+ unfold equivlistA; unfold addlistA in EQ; intros.
  destruct (EQ x0); clear EQ.
  split; intros.
  destruct H; auto.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 23ff22f92f..e973db4ad3 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -187,7 +187,7 @@ Qed.
 
 Lemma NoDupA_eqlistA_permut : 
   forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
-    eqlistA eqA l l' -> permutation l l'.
+    equivlistA eqA l l' -> permutation l l'.
 Proof.
   intros.
   red; unfold meq; intros.