proposition: Lemma semBindOptSize_isNone_subset_compat (A B : Type) (g g' : E (option A)) (f f' : A -> E (option B)) s : (~ semProdSize g' s None -> semProdSize g' s <--> semProdSize g s) -> isNone :&: semProdSize g s \subset isNone :&: semProdSize g' s -> (forall (x : A), isNone :&: semProdSize (f x) s \subset isNone :&: semProdSize (f' x) s) -> (fun u : option _ => isNone u) :&: semProdSize (bindOpt g f) s \subset (fun u : option _ => isNone u) :&: semProdSize (bindOpt g' f') s.
proof: Proof. intros Hyp0 Hyp1 Hyp2 z [Hin1 Hin2]. destruct z. now inv Hin1. simpl in Hin2. split. reflexivity. simpl in *. unfold semEnumSize in *. simpl in *. unfold LazyList.bindLazyList in *. simpl in *. eapply (@lazy_concat_in' (option B)) in Hin2. destruct Hin2 as [l1 [Hinl1 Hinl2]]. assert (Hinl2' := Hinl2). eapply LazyList.lazy_in_map_iff in Hinl2'. destruct Hinl2' as [x [Hrun Hin]]. destruct x. - unfold semProdSizeOpt in *. simpl in *. unfold semEnumSize in *. destruct (In_ll_Dec None (Enumerators.run g' s)). eapply (@LazyList.lazy_concat_in (option B)). 2:{ 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. } simpl. now left. eapply Hyp0 in H. eapply H in Hin. assert (Hina : ((fun u : option B => isNone u) :&: LazyList.In_ll^~ (Enumerators.run (f a) s)) None). { split; eauto. rewrite Hrun; eassumption. } eapply Hyp2 in Hina. inv Hina. eapply (@LazyList.lazy_concat_in (option B)). eapply H1. 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. - assert (Hin' : LazyList.In_ll None (Enumerators.run g' s)). { eapply Hyp1. split; eauto. } eapply (@LazyList.lazy_concat_in (option B)). eassumption. rewrite <- Hrun. 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)