From 835f581b40183986e76e5e02a26fab05239609c9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 26 Dec 2008 22:26:30 +0000 Subject: FMaps: various updates (mostly suggested by P. Casteran) - New functions: update (a kind of union), restrict (a kind of inter), diff. - New predicat Partition (and Disjoint), many results about Partition. - Equivalence instead of obsolete Setoid_Theory (they are aliases). refl_st, sym_st, trans_st aren't used anymore and marked as obsolete. - Start using Morphism (E.eq==>...) instead of compat_... This change (FMaps only) is incompatible with 8.2betaX, but it's really better now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Lists/SetoidList.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'theories/Lists') diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index ce36ade64..886c95aad 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -449,7 +449,7 @@ Definition transpose (f : A -> B -> B) := Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) := forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)). -Variable st:Setoid_Theory _ eqB. +Variable st:Equivalence eqB. Variable f:A->B->B. Variable i:B. Variable Comp:compat_op f. @@ -459,7 +459,7 @@ Lemma fold_right_eqlistA : eqB (fold_right f i s) (fold_right f i s'). Proof. induction 1; simpl; auto. -refl_st. +reflexivity. Qed. Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> @@ -598,8 +598,8 @@ Lemma fold_right_commutes_restr : eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. induction s1; simpl; auto; intros. -refl_st. -trans_st (f a (f x (fold_right f i (s1++s2)))). +reflexivity. +transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. apply IHs1. inversion_clear H; auto. @@ -615,7 +615,7 @@ Lemma fold_right_equivlistA_restr : Proof. simple induction s. destruct s'; simpl. - intros; refl_st; auto. + intros; reflexivity. unfold equivlistA; intros. destruct (H2 a). assert (X : InA a nil); auto; inversion X. @@ -624,16 +624,16 @@ Proof. rewrite <- (E x); auto. destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. - trans_st (f x (fold_right f i (s1++s2))). + transitivity (f x (fold_right f i (s1++s2))). apply Comp; auto. apply Hrec; auto. inversion_clear N; auto. eapply NoDupA_split; eauto. inversion_clear F; auto. eapply equivlistA_NoDupA_split; eauto. - trans_st (f y (fold_right f i (s1++s2))). - apply Comp; auto; refl_st. - sym_st; apply fold_right_commutes_restr. + transitivity (f y (fold_right f i (s1++s2))). + apply Comp; auto. reflexivity. + symmetry; apply fold_right_commutes_restr. apply ForallList2_equivlistA with (x::l); auto. Qed. @@ -654,8 +654,8 @@ Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. induction s1; simpl; auto; intros. -refl_st. -trans_st (f a (f x (fold_right f i (s1++s2)))). +reflexivity. +transitivity (f a (f x (fold_right f i (s1++s2)))); auto. Qed. Lemma fold_right_equivlistA : -- cgit v1.2.3