proposition: Lemma fold_compat : forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f g:elt->A->A), Proper (E.eq==>eqA==>eqA) f -> transpose eqA f -> Proper (E.eq==>eqA==>eqA) g -> transpose eqA g -> forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> (eqA (fold f s i) (fold g s i)).
proof: Proof. intros A eqA st f g fc ft gc gt i. intro s; pattern s; apply set_rec; intros. - transitivity (fold f s0 i). + apply fold_equal with (eqA:=eqA); auto. rewrite equal_sym; auto. + transitivity (fold g s0 i). * apply H0; intros; apply H1; auto with set. elim (equal_2 H x); auto with set; intros. * apply fold_equal with (eqA:=eqA); auto with set. - transitivity (f x (fold f s0 i)). + apply fold_add with (eqA:=eqA); auto with set. + transitivity (g x (fold f s0 i)); auto with set relations. transitivity (g x (fold g s0 i)); auto with set relations. * apply gc; auto with set relations. * symmetry; apply fold_add with (eqA:=eqA); auto. - do 2 rewrite fold_empty; reflexivity. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx