proposition: Lemma takeUntil_length_ForAllIf {A1 A2} (P1 : Stream A1 → bool) `(ex1 : LazyExists (fun x => Is_true (P1 x)) s1) {P2 : Stream A2 → bool} `(ex2 : LazyExists (fun x => Is_true (P2 x)) s2) (F : ForAllIf (fun x => Is_true (P2 x)) (fun x => Is_true (P1 x)) s2 s1) : takeUntil_length P1 ex1 ≤ takeUntil_length P2 ex2.
proof: Proof. Proof with auto using Is_true_eq_left, Is_true_neq_left. revert s2 ex2 F. assert (ex1':=ex1). unfold takeUntil_length. induction ex1' as [s1|s1 ? IH]; intros. rewrite takeUntil_end... apply Nat.le_0_l. case_eq (P1 s1); intros EP1. rewrite takeUntil_end... apply Nat.le_0_l. destruct (takeUntil_step _ ex1 (λ _, S) O) as [ex1' E1']... rewrite E1'. assert (ex2':=ex2). induction ex2' as [s2|s2 ? IH2]. destruct F. rewrite takeUntil_end in E1'... discriminate. case_eq (P2 s2); intros EP2. destruct F. rewrite takeUntil_end in E1'... discriminate. destruct (takeUntil_step _ ex2 (λ _, S) O) as [ex2' E2']... rewrite E2'. apply le_n_S, (IH tt). destruct F... 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