proposition: Lemma semShrinking_idSize {C A} {HCheck : Checkable C} (sh : A -> list A) (x : A) (pf : A -> C) (s : nat) : semCheckerSize (shrinking sh x pf) s <-> semCheckableSize (pf x) s.
proof: Proof. unfold semCheckableSize, shrinking, semCheckerSize, semProdSize, props. have [n <-] : exists n, S n = 1000 by eexists; reflexivity. split. - move => H b [[[res [l]]] [/= [seed Hgen] H']]; subst. + destruct (RandomQC.randomSplitAssumption seed seed) as [seed' Hseed']. suff : successful (run (@fmap _ (@Functor_Monad G (@super _ (ProducerGen))) _ _ (fun x0 => {| unProp := joinRose (fmapRose unProp x0) |}) (promote (@props' _ _ HCheck (S n) pf sh x))) s seed'). setoid_rewrite runFmap. rewrite runPromote. simpl. rewrite Hseed'. simpl. rewrite Hgen -H' /=. move => -> //. rewrite <- H => //. eexists. split; try by reflexivity. eexists. reflexivity. - move => H b [[[r [l]]] /= [[seed H1] <-]]. apply H. simpl in *. destruct (RandomQC.randomSplit seed) as [s1 s2]. destruct ((run (checker (pf x)) s s1)) as [[res [l']]] eqn:Heq=> //=. simpl in *. move : H1 => [H1 H2]; subst. eexists. eexists. exists s1. reflexivity. rewrite Heq. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes