proposition: Lemma takeUntil_elim {A B} (P:Stream A → bool) (cons: A → B → B) (nil: B) (Q: Stream A → B → Prop) : (∀ s, Is_true (P s) → Q s nil) → (∀ s x, Q (tl s) x → ¬Is_true (P s) → Q s (cons (hd s) x)) → ∀ `(ex : LazyExists (fun x => Is_true (P x)) s), Q s (takeUntil P ex cons nil).
proof: Proof. intros c1 c2 s ex. assert (ex':=ex). induction ex'. rewrite takeUntil_end; try assumption. eapply c1. apply H. assert (Z0:=takeUntil_end P ex cons nil). assert (Z1:=takeUntil_step P ex cons nil). assert (Z0':=c1 x). assert (Z1':=c2 x). destruct (P x). clear Z1. rewrite Z0; try constructor. apply Z0'. constructor. clear Z0 Z0'. destruct (Z1 (λ x, x)) as [ex' Z]. rewrite Z. clear Z Z1. eapply Z1'; auto. apply H0. constructor. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals