proposition: Lemma takeUntil_wd_alt `{Setoid A} `{Setoid B} `{!Proper ((=) ==> eq) (P : Stream A → bool)} `(ex1 : LazyExists (fun x => Is_true (P x)) s1) `(ex2 : LazyExists (fun x => Is_true (P x)) s2) (cons: A → B → B) `{!Proper ((=) ==> (=) ==> (=)) cons} (nil : B) : s1 = s2 → takeUntil P ex1 cons nil = takeUntil P ex2 cons nil.
proof: Proof. Proof with try easy. revert s2 ex2. assert (ex1':=ex1). induction ex1' as [s1 P1 | s1 P1 IH]; intros ? ? E; case ex1; clear ex1; case ex2; clear ex2; simpl; case_eq (P s1); case_eq (P s2); intros P2 P3 ? ?... destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. now destruct (Is_true_neq_left _ P3). destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. destruct (eq_true_false_abs (P s1))... now rewrite E. rewrite (IH tt); now rewrite E. 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