proposition: Lemma semBindSizeMonotonicIncl_l {A B} (g : G A) (f : A -> G (option B)) (s1 : set A) (fs : A -> set B) `{Hg : @SizeMonotonic _ _ PG g} `{Hf : forall a, SizeMonotonicOpt (f a)} : s1 \subset semProd g -> (forall x, Some @: (fs x) \subset semProd (f x)) -> (Some @: \bigcup_(a in s1) (fs a)) \subset semProd (bind g f).
proof: Proof. move => H1 H2 y [y' [[x [Hs1 Hfs2]] Heq]]; inversion Heq; subst; clear Heq. eapply H1 in Hs1. assert (Hin2 : (Some @: fs x) (Some y')). { eexists; split; eauto. now constructor. } eapply H2 in Hin2. unfold SizeMonotonic in Hg. edestruct Hs1 as [s [_ Hgen]]. edestruct Hin2 as [s' [_ Hfgen]]. assert (Hin2' : ((fun u : option B => u) :&: semProdSize (f x) s') (Some y')). { split; eauto. } apply Hg with (s2 := s + s') in Hgen; [| now ssromega]. rewrite /semProd. exists (s + s'); split; unfold setT; auto. apply semBindSize. exists x; split; auto. apply monotonicOpt with (s1 := s'); eauto; try ssromega. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)