proposition: Lemma unsized_printTestCase {A C} `{Checkable C} `{Show A} (c : A -> C) : (forall a, Unsized (checker (c a))) -> (forall a, Unsized (printTestCase (String.append (Show.show a) newline) (c a))).
proof: Proof. Abort. Lemma semForAllShrinkSize: forall {A C} `{Checkable C} `{Show A} (gen : G A) (f : A -> C) shrinker (size: nat), semCheckerSize (forAllShrink gen shrinker f) size <-> forall a : A, semProdSize gen size a -> semCheckableSize (f a) size. Proof. move => A C H show gen pf shrink. split. - rewrite /forAllShrink semBindGenSize. move=> H' a /H' Hgen. setoid_rewrite semShrinking_idSize in Hgen. setoid_rewrite semPredQPropSize in Hgen. by apply semPrintTestCase_idSize in Hgen. - move=> H'. rewrite /forAllShrink semBindGenSize. move => a g. rewrite semShrinking_idSize. apply semPredQPropSize. rewrite semPrintTestCase_idSize. by auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes