proposition: Lemma arbOpt_correct: forall {A} `{H : Arbitrary A} (P : nat -> A -> Prop) s, (semProdSize arbitrary s <--> P s) -> (semProdSize arbitrary s <--> (fun (m : option A) => match m with | None => true | Some x => P s x end)).
proof: Proof. move => A G S Arb P s Hgen m. rewrite !/arbitrary /genOption; split. - move => /semFrequencySize [[w g] H2]. move: H2 => [[H2 | [H2 | H2]] H3]; destruct m => //=; apply Hgen => //=; inversion H2; subst; auto; simpl in *. + apply (@semReturnSize Generators.G ProducerGen ProducerSemanticsGen (option A) None s (Some a)) in H3; inversion H3. + apply (@semLiftProdSize _ ProducerGen _ _ _ Some (@arbitrary _ G) s (Some a)) in H3; eauto with typeclass_instances. inversion H3 as [x [H0 H1]]. inversion H1; subst; auto. - destruct m eqn:Hm; simpl in *; move => HP; subst. + apply semFrequencySize; simpl. exists (7, liftM Some arbitrary); split; auto. * right; left; auto. * simpl. apply (@semLiftProdSize _ ProducerGen _ _ _ Some (@arbitrary _ G) s (Some a)); simpl; eauto with typeclass_instances. apply imset_in; apply Hgen; auto. + apply semFrequencySize; simpl. exists (1, ret None); split; auto. * left; auto. * simpl. apply (@semReturnSize Generators.G ProducerGen ProducerSemanticsGen (option A) None s None). constructor. Qed.
imports: Coq(Arith Basics List Recdef ZArith Lia) mathcomp(ssrbool ssreflect ssrnat) QuickChick(Classes Sets Producer Enumerators Generators Tactics)