proposition: Lemma semForAllShrinkMonotonic : forall {A C} `{Checkable C} `{Show A} (gen : G A) (f : A -> C) shrinker `{@SizeMonotonic _ _ ProducerGen gen}, (forall a, SizeMonotonicChecker (checker (f a))) -> (semChecker (forAllShrink gen shrinker f) <-> forall a : A, semProd gen a -> semCheckable (f a)).
proof: Proof. move => A C H1 H2 gen f sh Hmon1 Hmon2. split; move => Hcheck a. - move => [s [_ H']] s'. case_eq (s <= s') => [/leP Hleq | /leP/Compare_dec.not_le/ltP/ltnW Hleq]. + specialize (Hcheck s'). rewrite -> semForAllShrinkSize in Hcheck. apply Hcheck. by eapply Hmon1; eauto. + specialize (Hcheck s). eapply semForAllShrinkSize in Hcheck; eauto. by eapply monotonicChecker_alt_def; eauto. - by eapply semForAllShrinkSize; intros; apply Hcheck; eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes