proposition: Lemma enumeratingOpt_complete A P (e : E (option A)) {Hc : CorrectST P e} ch x : P x -> ch x = Some true -> exists s, enumeratingOpt e ch s = Some true.
proof: Proof. unfold enumeratingOpt. intros Hp Heq. assert (Hs : semProdOpt e x). { eapply Hc. eassumption. } destruct Hs as [s [_ Hs]]. simpl in *. unfold semEnumSize in Hs. exists s. revert Hs Heq. generalize (Enumerators.run e s), false. clear. induction l; intros b Hin Heq; simpl in *. - exfalso; eauto. - inv Hin. + rewrite Heq. reflexivity. + destruct a; eauto. destruct (ch a) as [ [| ] | ] eqn:Heq'; eauto. Qed.
imports: String List mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Producer Generators Enumerators Tactics Sets Classes