1 files changed, 170 insertions, 19 deletions

diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 0fd1693e..b57c3f04 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -11,7 +11,7 @@ Require Export Sorted.
 Require Export Setoid Basics Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
-
+(* Set Universe Polymorphism. *)
 (** * Logical relations over lists with respect to a setoid equality
       or ordering. *)
 
@@ -34,7 +34,7 @@ Hint Constructors InA.
     of the previous one. Having [InA = Exists eqA] raises too
     many compatibility issues. For now, we only state the equivalence: *)
 
-Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l.
+Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. 
 Proof. split; induction 1; auto. Qed.
 
 Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
@@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed.
 (** Results concerning lists modulo [eqA] *)
 
 Hypothesis eqA_equiv : Equivalence eqA.
-
-Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
-Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
+Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
+Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
+Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
+ 
+Hint Resolve eqarefl eqatrans.
+Hint Immediate eqasym.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
@@ -123,7 +125,6 @@ Proof.
  intros x y z H; revert z; induction H; auto.
  inversion 1; subst; auto. invlist eqlistA; eauto with *.
 Qed.
-
 (** Moreover, [eqlistA] implies [equivlistA]. A reverse result
     will be proved later for sorted list without duplicates. *)
 
@@ -149,7 +150,7 @@ Qed.
 
 Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
- intros l x y H H'. rewrite <- H; auto.
+ intros l x y H H'. rewrite <- H. auto.
 Qed.
 Hint Immediate InA_eqA.
 
@@ -496,7 +497,7 @@ Proof.
  apply Hrec; auto.
  inv; auto.
  eapply NoDupA_split; eauto.
- invlist ForallOrdPairs; auto.
+ invlist ForallOrdPairs; auto. 
  eapply equivlistA_NoDupA_split; eauto.
  transitivity (f y (fold_right f i (s1++s2))).
  apply Comp; auto. reflexivity.
@@ -545,6 +546,155 @@ Qed.
 
 End Fold.
 
+
+Section Fold2.
+
+Variable B:Type.
+Variable eqB:B->B->Prop.
+Variable st:Equivalence eqB.
+Variable f:A->B->B.
+Variable Comp:Proper (eqA==>eqB==>eqB) f.
+
+
+Lemma fold_right_eqlistA2 :
+  forall s s' (i j:B) (heqij: eqB i j) (heqss': eqlistA s s'),
+  eqB (fold_right f i s) (fold_right f j s').
+Proof.
+  intros s.
+  induction s;intros.
+  - inversion heqss'.
+    subst.
+    simpl.
+    assumption.
+  - inversion heqss'.
+    subst.
+    simpl.
+    apply Comp.
+    + assumption.
+    + apply IHs;assumption.
+Qed.
+
+Section Fold2_With_Restriction.
+
+Variable R : A -> A -> Prop.
+Hypothesis R_sym : Symmetric R.
+Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
+
+(** Two-argument functions that allow to reorder their arguments. *)
+Definition transpose2 (f : A -> B -> B) :=
+  forall (x y : A) (z z': B), eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
+
+(** A version of transpose with restriction on where it should hold *)
+Definition transpose_restr2 (R : A -> A -> Prop)(f : A -> B -> B) :=
+  forall (x y : A) (z z': B), R x y -> eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
+
+Variable TraR :transpose_restr2 R f.
+
+Lemma fold_right_commutes_restr2 :
+  forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) ->
+  eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
+Proof.
+induction s1; simpl; auto; intros.
+- apply Comp.
+  + destruct eqA_equiv. apply Equivalence_Reflexive.
+  + eapply fold_right_eqlistA2.
+    * assumption.
+    * reflexivity.
+- transitivity (f a (f x (fold_right f j (s1++s2)))).
+  apply Comp; auto.
+  eapply IHs1.
+  assumption.
+  invlist ForallOrdPairs; auto.
+  apply TraR.
+  invlist ForallOrdPairs; auto.
+  rewrite Forall_forall in H0; apply H0.
+  apply in_or_app; simpl; auto.
+  reflexivity.
+Qed.
+
+Lemma fold_right_equivlistA_restr2 :
+  forall s s' (i j:B) (heqij: eqB i j),
+    NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
+               eqB i j -> 
+  equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
+Proof.
+ simple induction s.
+ destruct s'; simpl.
+ intros. assumption.
+ unfold equivlistA; intros.
+ destruct (H3 a).
+ assert (InA a nil) by auto; inv.
+ intros x l Hrec s' i j heqij N N' F eqij E; simpl in *.
+ assert (InA x s') by (rewrite <- (E x); auto).
+ destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
+ subst s'.
+ transitivity (f x (fold_right f j (s1++s2))).
+ - apply Comp; auto.
+   apply Hrec; auto.
+   inv; auto.
+   eapply NoDupA_split; eauto.
+   invlist ForallOrdPairs; auto.
+   eapply equivlistA_NoDupA_split; eauto.
+ - transitivity (f y (fold_right f i (s1++s2))).
+   + apply Comp; auto.
+     symmetry.
+     apply fold_right_eqlistA2.
+     * assumption.
+     * reflexivity.
+   + symmetry.
+     apply fold_right_commutes_restr2.
+     symmetry.
+     assumption.
+     apply ForallOrdPairs_inclA with (x::l); auto.
+     red; intros; rewrite E; auto.
+Qed.
+
+
+Lemma fold_right_add_restr2 :
+  forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
+  equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
+Proof.
+ intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto.
+Qed.
+
+End Fold2_With_Restriction.
+
+Variable Tra :transpose2 f.
+
+Lemma fold_right_commutes2 : forall s1 s2 i x x',
+  eqA x x' -> 
+  eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))).
+Proof.
+  induction s1;simpl;intros.
+- apply Comp;auto.
+  reflexivity.
+- transitivity (f a (f x' (fold_right f i (s1++s2)))); auto.
+  + apply Comp;auto.
+  + apply Tra.
+    reflexivity.
+Qed.
+
+Lemma fold_right_equivlistA2 :
+  forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j ->
+  equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
+Proof.
+red in Tra.
+intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True);
+repeat red; auto.
+apply ForallPairs_ForallOrdPairs; try red; auto.
+Qed.
+
+Lemma fold_right_add2 :
+  forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s ->
+  equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
+Proof.
+ intros.
+ replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto.
+ eapply fold_right_equivlistA2;auto. 
+Qed.
+
+End Fold2.
+
 Section Remove.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
@@ -582,14 +732,14 @@ split.
 intro; inv.
 destruct 1; inv.
 intros.
-destruct (eqA_dec x a); simpl; auto.
+destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto.
 rewrite IHl; split; destruct 1; split; auto.
 inv; auto.
 destruct H0; transitivity a; auto.
 split.
 intro; inv.
 split; auto.
-contradict n.
+contradict Hnot.
 transitivity y; auto.
 rewrite (IHl x y) in H0; destruct H0; auto.
 destruct 1; inv; auto.
@@ -633,7 +783,9 @@ Variable ltA : A -> A -> Prop.
 Hypothesis ltA_strorder : StrictOrder ltA.
 Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
-Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Hint Resolve sotrans.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
@@ -647,7 +799,7 @@ Proof.
 Qed.
 
 Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
-Proof.
+Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *)
  intros x x' Hxx' l l' Hll'.
  inversion_clear Hll'.
  intuition.
@@ -658,7 +810,7 @@ Qed.
 
 (** For compatibility, can be deduced from [InfA_compat] *)
 Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
-Proof.
+Proof using eqA_equiv ltA_compat.
  intros H; now rewrite H.
 Qed.
 Hint Immediate InfA_ltA InfA_eqA.
@@ -759,7 +911,7 @@ Qed.
 Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
 Proof.
 repeat red. intros.
-rewrite (app_nil_end (rev x)), (app_nil_end (rev y)).
+rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)).
 apply eqlistA_rev_app; auto.
 Qed.
 
@@ -815,13 +967,12 @@ intros.
 rewrite filter_In in H; destruct H.
 eapply SortA_InfA_InA; eauto.
 Qed.
-
 Arguments eq {A} x _.
 
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
-clear ltA ltA_compat ltA_strorder.
+clear sotrans ltA ltA_strorder ltA_compat.
 intros; do 2 rewrite InA_alt; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
@@ -888,9 +1039,9 @@ split; intros.
 invlist InA.
 compute in H2; destruct H2. subst b'.
 destruct (eqA_dec a a'); intuition.
-destruct (eqA_dec a a'); simpl.
+destruct (eqA_dec a a') as [HeqA|]; simpl.
 contradict H0.
-revert e H2; clear - eqA_equiv.
+revert HeqA H2; clear - eqA_equiv.
 induction l.
 intros; invlist InA.
 intros; invlist InA; auto.