proposition: Lemma semBindOptSize_subset_compat (A B : Type) (g g' : E (option A)) (f f' : A -> E (option B)) s : semProdSize g s \subset semProdSize g' s -> (forall (x : A), semProdSize g s (Some x) -> semProdSize (f x) s \subset semProdSize (f' x) s) -> semProdSize (bindOpt g f) s \subset semProdSize (bindOpt g' f') s.
proof: Proof. intros Hyp0 Hyp1 x H. simpl in *. unfold semEnumSize in *. unfold LazyList.bindLazyList in *. simpl in *. eapply (@lazy_concat_in' (option B)) in H. destruct H as [l1 [Hinl1 Hinl2]]. assert (Hinl2' := Hinl2). eapply LazyList.lazy_in_map_iff in Hinl2'. destruct Hinl2' as [z [Hrun Hin]]. destruct z. - subst. assert (Hin' := Hin). eapply Hyp0 in Hin. eapply Hyp1 in Hinl1. eapply (@LazyList.lazy_concat_in (option B)). eassumption. eapply LazyList.lazy_in_map with (f := fun x : option A => Enumerators.run match x with | Some a0 => f' a0 | None => returnEnum None end s) (x := Some a). eassumption. eassumption. - subst. eapply Hyp0 in Hin. eapply (@LazyList.lazy_concat_in (option B)). eassumption. eapply LazyList.lazy_in_map with (f := fun x : option A => Enumerators.run match x with | Some a0 => f' a0 | None => returnEnum None end s) (x := None). eassumption. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)