proposition: Lemma semBindGenSizeMonotonic {A} (gen : G A) (f : A -> Checker) `{@SizeMonotonic _ _ ProducerGen gen} `{forall a, SizeMonotonicChecker (f a)} : (semChecker (bindGen gen f) <-> forall a, semProd gen a -> semChecker (f a)).
proof: Proof. split; move => Hgen a. - move => [s [_ H']] s'. case_eq (s <= s') => [/leP Hleq | /leP/Compare_dec.not_le/ltP/ltnW Hleq]. + specialize (Hgen s'). eapply semBindGenSize in Hgen; eauto. eapply monotonic; eauto. + specialize (Hgen s). eapply semBindGenSize in Hgen; eauto. eapply monotonicChecker_alt_def; eauto. - by eapply semBindGenSize; intros; apply Hgen; eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes