proposition: Lemma theorem46A x xs y ys z zs : x = foldl mul b xs -> y = foldl mul b ys -> z = foldl mul b zs -> aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) -> add x (add y z) = add (add x y) z.
proof: Proof. move=> xxs yys zzs H. rewrite {1}(theorem46rid (add := add) idempotent_converse injective_return zzs) //. Abort. End theorem46_contd. Section theorem47. Variable M : nondetCIMonad. Variables (A B : Type) (b : B) (mul : B -> A -> B) (add : B -> B -> B). Hypothesis idempotent_converse : forall C m1 m2 x, m1 [~] m2 = Ret x :> M C -> m1 = ret _ x /\ m2 = ret _ x. Hypothesis injective_return : forall C x1 x2, Ret x1 = Ret x2 :> M C -> x1 = x2. Lemma theorem47 : aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) -> is_hom add (mul b) b (foldl mul b). Proof. move=> H. split; first by []. split; first by []. move=> xs ys. rewrite (_ : xs ++ ys = flatten [:: xs; ys]); last by rewrite /= cats0. transitivity (foldl add b (map (foldl mul b) [:: xs; ys])). case: (@iperm_is_alt_ret M _ [:: xs; ys]) => m Hm. by rewrite (lemma45a idempotent_converse injective_return H). transitivity (add (foldl mul b xs) (add (foldl mul b ys) b)). rewrite /=. rewrite /= -(theorem46lid (zs := xs) (mul := mul) idempotent_converse injective_return _ H) //. by rewrite /= -(theorem46rid (zs := ys) (mul := mul) idempotent_converse injective_return _ H). by rewrite /= -(theorem46rid (zs := ys) (mul := mul) idempotent_converse injective_return _ H). Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib