proposition: Lemma Partition_fold : forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), Proper (E.eq==>eq==>eqA==>eqA) f -> transpose_neqkey eqA f -> forall m m1 m2 i, Partition m m1 m2 -> eqA (fold f m i) (fold f m1 (fold f m2 i)).
proof: Proof. intros A eqA st f Comp Tra. induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction. - intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto. rewrite (Partition_Empty Hp) in Hm. destruct Hm. rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity. - intros m1 m2 i Hp. destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]). + assert (~In k m3). { contradict Hn. destruct Hn as (e',He'). destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } transitivity (f k e (fold f m i)). * apply fold_Add with (eqA:=eqA); auto. * symmetry. transitivity (f k e (fold f m3 (fold f m2 i))). -- apply fold_Add with (eqA:=eqA); auto. -- apply Comp; auto. symmetry; apply IH; auto. + assert (~In k m3). { contradict Hn. destruct Hn as (e',He'). destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } assert (~In k m1). { contradict Hn. destruct Hn as (e',He'). destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. } transitivity (f k e (fold f m i)). * apply fold_Add with (eqA:=eqA); auto. * transitivity (f k e (fold f m1 (fold f m3 i))). -- apply Comp; auto using IH. -- transitivity (fold f m1 (f k e (fold f m3 i))). ++ symmetry. apply fold_commutes with (eqA:=eqA); auto. ++ apply fold_init with (eqA:=eqA); auto. symmetry. apply fold_Add with (eqA:=eqA); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface