proposition: Lemma enumerating_complete' A (e : E A) ch {Hm : SizeMonotonic e} {Hc : Correct A e} : (forall x s1 s2, (s1 <= s2) -> ch s1 x = Some true -> ch s2 x = Some true) -> (exists x s, ch s x = Some true) -> (exists (s : nat), enumerating e (ch s) s = Some true).
proof: Proof. intros Hmon [x [s Hch]]. unfold enumerating. assert (Hin : semProd e x). { eapply Hc. reflexivity. } destruct Hin as [s' [_ Hsem]]. simpl in *. unfold semEnumSize in *. assert (Hsem' : LazyList.In_ll x (Enumerators.run e (max s s'))). { eapply Hm > [| simpl; eassumption ]. lia. } clear Hsem. exists (max s s'). revert Hsem'. generalize (Enumerators.run e (max s s')), false. induction l; intros b Hin; inv Hin; simpl. - erewrite Hmon > [ reflexivity | | eassumption ]. lia. - destruct (ch (Nat.max s s') a); eauto. destruct b0; eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)