proposition: Lemma takeUntil_correct {A B} (P : Stream A → bool) `(ex : !LazyExists (fun x => Is_true (P x)) s) (cons: A → B → B) (nil : B) : takeUntil P ex cons nil ≡ take s (takeUntil_length P ex) cons nil.
proof: Proof. Proof with auto using Is_true_eq_left, Is_true_neq_left. assert (ex':=ex). unfold takeUntil_length. induction ex' as [s|s ? IH]. repeat rewrite takeUntil_end... case_eq (P s); intros E. repeat rewrite takeUntil_end... destruct (takeUntil_step P ex cons nil) as [ex1 E1]... rewrite E1. rewrite (IH tt)... destruct (takeUntil_step P ex (λ _, S) O) as [ex2 E2]... rewrite E2. simpl. rewrite (takeUntil_wd ex1 ex2 (λ _, S) O)... 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