From stdpp Require Import prelude.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
From Coq Require Import Streams Sorted.
From VLSM.Lib Require Import Preamble StreamExtras SortedLists.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Lib Require Import ListExtras StdppExtras NeList.

Utility: Stream Filters

Given a predicate P and a stream s, a stream of naturals ns determines a filtering_subsequence for P on s if it corresponds to the list of positions in ss where P holds, increasingly ordered.

Definition filtering_subsequence
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ns : Stream nat)
  : Prop
  := (forall i, i < hd ns -> ~ P (Str_nth i s)) /\
     ForAll2 (fun m n => P (Str_nth m s) /\ m < n /\ forall i, m < i < n -> ~ P (Str_nth i s)) ns.

A more intuitive statement of the filtering_subsequence property. See FilteringSubsequence_iff for the equivalence result.

Record FilteringSubsequence
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ns : Stream nat)
  : Prop :=
{
  fs_monotone : monotone_nat_stream_prop ns;
  fs_is_filter : forall n, P (Str_nth n s) <-> exists k, n = Str_nth k ns;
}.

Lemma filtering_subsequence_sorted
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ns : Stream nat)
  (Hfs : filtering_subsequence P s ns)
  : ForAll2 lt ns.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
ForAll2 lt ns
Proof.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
ForAll2 lt ns
  destruct Hfs as [_ Hfs].A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: ForAll2
(λ m n : nat,
P (Str_nth m s) ∧ m < n ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s))) ns
ForAll2 lt ns
  revert Hfs; apply ForAll2_subsumption.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
∀ a b : nat,
  P (Str_nth a s)
  ∧ a < b ∧ (∀ i : nat, a < i < b → ¬ P (Str_nth i s))
  → a < b
  by intros a b H; apply H.
Qed.

Lemma filtering_subsequence_prefix_sorted
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ns : Stream nat)
  (Hfs : filtering_subsequence P s ns)
  : forall n, LocallySorted lt (stream_prefix ns n).A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
∀ n : nat, LocallySorted lt (stream_prefix ns n)
Proof.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
∀ n : nat, LocallySorted lt (stream_prefix ns n)
  intro n.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
n: nat
LocallySorted lt (stream_prefix ns n) apply LocallySorted_ForAll2.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
n: nat
ForAllSuffix2 lt (stream_prefix ns n)
  apply stream_prefix_ForAll2.A: Type
P: A → Prop
s: Stream A
ns: Stream nat
Hfs: filtering_subsequence P s ns
n: nat
ForAll2 lt ns
  by apply filtering_subsequence_sorted in Hfs.
Qed.

Lemma filtering_subsequence_iff
  {A : Type}
  (P Q : A -> Prop)
  (HPQ : forall a, P a <-> Q a)
  (s : Stream A)
  (ss : Stream nat)
  : filtering_subsequence P s ss <-> filtering_subsequence Q s ss.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a ↔ Q a
s: Stream A
ss: Stream nat
filtering_subsequence P s ss
↔ filtering_subsequence Q s ss
Proof.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a ↔ Q a
s: Stream A
ss: Stream nat
filtering_subsequence P s ss
↔ filtering_subsequence Q s ss
  unfold filtering_subsequence.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a ↔ Q a
s: Stream A
ss: Stream nat
(∀ i : nat, i < hd ss → ¬ P (Str_nth i s))
∧ ForAll2
    (λ m n : nat,
       P (Str_nth m s)
       ∧ m < n
         ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s)))
    ss
↔ (∀ i : nat, i < hd ss → ¬ Q (Str_nth i s))
  ∧ ForAll2
      (λ m n : nat,
         Q (Str_nth m s)
         ∧ m < n
           ∧ (∀ i : nat, m < i < n → ¬ Q (Str_nth i s)))
      ss
  rewrite !ForAll2_forall.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a ↔ Q a
s: Stream A
ss: Stream nat
(∀ i : nat, i < hd ss → ¬ P (Str_nth i s))
∧ (∀ n : nat,
     P (Str_nth (Str_nth n ss) s)
     ∧ Str_nth n ss < Str_nth (S n) ss
       ∧ (∀ i : nat,
            Str_nth n ss < i < Str_nth (S n) ss
            → ¬ P (Str_nth i s)))
↔ (∀ i : nat, i < hd ss → ¬ Q (Str_nth i s))
  ∧ (∀ n : nat,
       Q (Str_nth (Str_nth n ss) s)
       ∧ Str_nth n ss < Str_nth (S n) ss
         ∧ (∀ i : nat,
              Str_nth n ss < i < Str_nth (S n) ss
              → ¬ Q (Str_nth i s)))
  by setoid_rewrite <- HPQ.
Qed.

Each element in a filtering_subsequence is a position in the base stream for which the predicate holds.

Lemma filtering_subsequence_witness
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (k : nat)
  : P (Str_nth (Str_nth k ss) s).A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
P (Str_nth (Str_nth k ss) s)
Proof.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
P (Str_nth (Str_nth k ss) s)
  destruct Hfs as [_ Hfs].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: ForAll2
(λ m n : nat,
P (Str_nth m s) ∧ m < n ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s))) ss
k: nat
P (Str_nth (Str_nth k ss) s)
  by rewrite ForAll2_forall in Hfs; apply Hfs.
Qed.

For each position in the base stream for which the predicate holds is present in the filtering_subsequence.

Lemma filtering_subsequence_witness_rev
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (n : nat)
  (Hn : P (Str_nth n s))
  : exists k, n = Str_nth k ss.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
∃ k : nat, n = Str_nth k ss
Proof.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
∃ k : nat, n = Str_nth k ss
  apply filtering_subsequence_sorted in Hfs as Hss_sorted.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Hss_sorted: ForAll2 lt ss
∃ k : nat, n = Str_nth k ss
  apply monotone_nat_stream_prop_from_successor in Hss_sorted.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Hss_sorted: monotone_nat_stream_prop ss
∃ k : nat, n = Str_nth k ss
  apply monotone_nat_stream_find with (n := n) in Hss_sorted.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Hss_sorted: n < hd ss
∨ (∃ k : nat,
     Str_nth k ss = n
     ∨ Str_nth k ss < n <
       Str_nth (S k) ss)
∃ k : nat, n = Str_nth k ss
  destruct Hss_sorted  as [Hlt | [k Hk]].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Hlt: n < hd ss
∃ k : nat, n = Str_nth k ss
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss = n
∨ Str_nth k ss < n < Str_nth (S k) ss
∃ k : nat, n = Str_nth k ss
  -A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Hlt: n < hd ss
∃ k : nat, n = Str_nth k ss by destruct Hfs as [Hfs _]; elim (Hfs n).
  -A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss = n
∨ Str_nth k ss < n < Str_nth (S k) ss
∃ k : nat, n = Str_nth k ss destruct Hk as [Heq | Hk]; subst; [by exists k |].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss < n < Str_nth (S k) ss
∃ k : nat, n = Str_nth k ss
    exfalso.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss < n < Str_nth (S k) ss
False apply proj2 in Hfs.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: ForAll2
(λ m n : nat,
P (Str_nth m s) ∧ m < n ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s))) ss
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss < n < Str_nth (S k) ss
False
    rewrite ForAll2_forall in Hfs.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
Hfs: ∀ n : nat,
P (Str_nth (Str_nth n ss) s)
∧ Str_nth n ss < Str_nth (S n) ss
∧ (∀ i : nat, Str_nth n ss < i < Str_nth (S n) ss → ¬ P (Str_nth i s))
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss < n < Str_nth (S k) ss
False
    specialize (Hfs k) as [_ [_ Hfs]].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
n: nat
Hn: P (Str_nth n s)
k: nat
Hk: Str_nth k ss < n < Str_nth (S k) ss
Hfs: ∀ i : nat, Str_nth k ss < i < Str_nth (S k) ss → ¬ P (Str_nth i s)
False
    by elim (Hfs n).
Qed.

Lemma FilteringSubsequence_iff
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ss : Stream nat)
  : FilteringSubsequence P s ss <-> filtering_subsequence P s ss.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
FilteringSubsequence P s ss
↔ filtering_subsequence P s ss
Proof.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
FilteringSubsequence P s ss
↔ filtering_subsequence P s ss
  split.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
FilteringSubsequence P s ss
→ filtering_subsequence P s ss
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
filtering_subsequence P s ss
→ FilteringSubsequence P s ss
  -A: Type
P: A → Prop
s: Stream A
ss: Stream nat
FilteringSubsequence P s ss
→ filtering_subsequence P s ss intros []; split.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
∀ i : nat, i < hd ss → ¬ P (Str_nth i s)
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
ForAll2
  (λ m n : nat,
     P (Str_nth m s)
     ∧ m < n
       ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s)))
  ss
    +A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
∀ i : nat, i < hd ss → ¬ P (Str_nth i s) setoid_rewrite fs_is_filter0.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
∀ i : nat, i < hd ss → ¬ (∃ k : nat, i = Str_nth k ss)
      intros i Hi [? ->].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
x: nat
Hi: Str_nth x ss < hd ss
False
      apply (fs_monotone0 x 0) in Hi.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
x: nat
Hi: x < 0
False
      by lia.
    +A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
ForAll2
  (λ m n : nat,
     P (Str_nth m s)
     ∧ m < n
       ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s)))
  ss apply ForAll2_forall; intros n; split_and!.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
P (Str_nth (Str_nth n ss) s)
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
Str_nth n ss < Str_nth (S n) ss
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
∀ i : nat,
  Str_nth n ss < i < Str_nth (S n) ss
  → ¬ P (Str_nth i s)
      *A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
P (Str_nth (Str_nth n ss) s) by apply fs_is_filter0; eexists.
      *A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
Str_nth n ss < Str_nth (S n) ss by apply (fs_monotone0 n (S n)); lia.
      *A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
∀ i : nat,
  Str_nth n ss < i < Str_nth (S n) ss
  → ¬ P (Str_nth i s) setoid_rewrite fs_is_filter0.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n: nat
∀ i : nat,
  Str_nth n ss < i < Str_nth (S n) ss
  → ¬ (∃ k : nat, i = Str_nth k ss)
        intros i [Hni Hni'] [? ->].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
fs_monotone0: monotone_nat_stream_prop ss
fs_is_filter0: ∀ n : nat,
  P (Str_nth n s)
  ↔ (∃ k : nat, n = Str_nth k ss)
n, x: nat
Hni': Str_nth x ss < Str_nth (S n) ss
Hni: Str_nth n ss < Str_nth x ss
False
        by apply fs_monotone0 in Hni, Hni'; lia.
  -A: Type
P: A → Prop
s: Stream A
ss: Stream nat
filtering_subsequence P s ss
→ FilteringSubsequence P s ss constructor.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
H: filtering_subsequence P s ss
monotone_nat_stream_prop ss
A: Type
P: A → Prop
s: Stream A
ss: Stream nat
H: filtering_subsequence P s ss
∀ n : nat,
  P (Str_nth n s) ↔ (∃ k : nat, n = Str_nth k ss)
    +A: Type
P: A → Prop
s: Stream A
ss: Stream nat
H: filtering_subsequence P s ss
monotone_nat_stream_prop ss by eapply monotone_nat_stream_prop_from_successor, filtering_subsequence_sorted.
    +A: Type
P: A → Prop
s: Stream A
ss: Stream nat
H: filtering_subsequence P s ss
∀ n : nat,
  P (Str_nth n s) ↔ (∃ k : nat, n = Str_nth k ss) split; [by apply filtering_subsequence_witness_rev |].A: Type
P: A → Prop
s: Stream A
ss: Stream nat
H: filtering_subsequence P s ss
n: nat
(∃ k : nat, n = Str_nth k ss) → P (Str_nth n s)
      by intros [? ->]; apply filtering_subsequence_witness.
Qed.

Prefixes of the filtering subsequence expressed as filters.

Lemma filtering_subsequence_prefix_is_filter
  {A : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  : forall (k : nat),
    stream_prefix ss (S k) =
    filter (fun i => P (Str_nth i s)) (stream_prefix nat_sequence (S (Str_nth k ss))).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
∀ k : nat,
  stream_prefix ss (S k) =
  filter (λ i : nat, P (Str_nth i s))
    (stream_prefix nat_sequence (S (Str_nth k ss)))
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
∀ k : nat,
  stream_prefix ss (S k) =
  filter (λ i : nat, P (Str_nth i s))
    (stream_prefix nat_sequence (S (Str_nth k ss)))
  intro k.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
stream_prefix ss (S k) =
filter (λ i : nat, P (Str_nth i s))
  (stream_prefix nat_sequence (S (Str_nth k ss)))
  apply (@set_equality_predicate _ lt _).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt (stream_prefix ss (S k))
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (S (Str_nth k ss))))
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
ListSetExtras.set_eq (stream_prefix ss (S k))
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (S (Str_nth k ss))))
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt (stream_prefix ss (S k)) by apply filtering_subsequence_prefix_sorted with P s.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (S (Str_nth k ss)))) apply LocallySorted_filter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
Transitive lt
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt
  (stream_prefix nat_sequence (S (Str_nth k ss)))
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
Transitive lt by typeclasses eauto.
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
LocallySorted lt
  (stream_prefix nat_sequence (S (Str_nth k ss))) by apply nat_sequence_prefix_sorted.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
ListSetExtras.set_eq (stream_prefix ss (S k))
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (S (Str_nth k ss)))) unfold ListSetExtras.set_eq, subseteq, list_subseteq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
(∀ x : nat,
   x ∈ stream_prefix ss (S k)
   → x
     ∈ filter (λ i : nat, P (Str_nth i s))
         (stream_prefix nat_sequence
            (S (Str_nth k ss))))
∧ (∀ x : nat,
     x
     ∈ filter (λ i : nat, P (Str_nth i s))
         (stream_prefix nat_sequence
            (S (Str_nth k ss)))
     → x ∈ stream_prefix ss (S k))
    setoid_rewrite elem_of_list_filter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
(∀ x : nat,
   x ∈ stream_prefix ss (S k)
   → P (Str_nth x s)
     ∧ x
       ∈ stream_prefix nat_sequence (S (Str_nth k ss)))
∧ (∀ x : nat,
     P (Str_nth x s)
     ∧ x
       ∈ stream_prefix nat_sequence (S (Str_nth k ss))
     → x ∈ stream_prefix ss (S k))
    setoid_rewrite elem_of_stream_prefix.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
(∀ x : nat,
   (∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x)
   → P (Str_nth x s)
     ∧ (∃ k0 : nat,
          k0 < S (Str_nth k ss)
          ∧ Str_nth k0 nat_sequence = x))
∧ (∀ x : nat,
     P (Str_nth x s)
     ∧ (∃ k0 : nat,
          k0 < S (Str_nth k ss)
          ∧ Str_nth k0 nat_sequence = x)
     → ∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x)
    setoid_rewrite nat_sequence_nth.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k: nat
(∀ x : nat,
   (∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x)
   → P (Str_nth x s)
     ∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x))
∧ (∀ x : nat,
     P (Str_nth x s)
     ∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x)
     → ∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x)
    split; intros.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
H: ∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x
P (Str_nth x s)
∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x)
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
H: P (Str_nth x s)
∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x)
∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
H: ∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x
P (Str_nth x s)
∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x) destruct H as [i [Hi Ha]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x, i: nat
Hi: i < S k
Ha: Str_nth i ss = x
P (Str_nth x s)
∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x)
      subst.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
P (Str_nth (Str_nth i ss) s)
∧ (∃ k0 : nat,
     k0 < S (Str_nth k ss) ∧ k0 = Str_nth i ss)
      split; [by apply filtering_subsequence_witness |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = Str_nth i ss
      eexists; split; [| done].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
Str_nth i ss < S (Str_nth k ss)
      destruct (decide (i = k)); [subst; lia |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
n: i ≠ k
Str_nth i ss < S (Str_nth k ss)
      cut (Str_nth i ss < Str_nth k ss); [lia |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
n: i ≠ k
Str_nth i ss < Str_nth k ss
      apply ForAll2_transitive_lookup; [by typeclasses eauto | | lia].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, i: nat
Hi: i < S k
n: i ≠ k
ForAll2 lt ss
      by apply filtering_subsequence_sorted in Hfs.
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
H: P (Str_nth x s)
∧ (∃ k0 : nat, k0 < S (Str_nth k ss) ∧ k0 = x)
∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x destruct H as [Hpa [_a [Hlt H_a]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
Hpa: P (Str_nth x s)
_a: nat
Hlt: _a < S (Str_nth k ss)
H_a: _a = x
∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x
      subst _a.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, x: nat
Hpa: P (Str_nth x s)
Hlt: x < S (Str_nth k ss)
∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = x
      destruct (filtering_subsequence_witness_rev _ _ _ Hfs _ Hpa) as [k' ->].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
∃ k0 : nat, k0 < S k ∧ Str_nth k0 ss = Str_nth k' ss
      exists k'.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
k' < S k ∧ Str_nth k' ss = Str_nth k' ss
      split; [| done].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
k' < S k
      apply filtering_subsequence_sorted in Hfs.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: ForAll2 lt ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
k' < S k
      apply monotone_nat_stream_prop_from_successor in Hfs.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: monotone_nat_stream_prop ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
k' < S k
      specialize (monotone_nat_stream_rev _ Hfs k' k) as Hle.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: monotone_nat_stream_prop ss
k, k': nat
Hlt: Str_nth k' ss < S (Str_nth k ss)
Hpa: P (Str_nth (Str_nth k' ss) s)
Hle: Str_nth k' ss ≤ Str_nth k ss → k' ≤ k
k' < S k
      by lia.
Qed.

Lemma filtering_subsequence_prefix_length
  {A : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (m : nat)
  : length (filter P (stream_prefix s (S (Str_nth m ss)))) = S m.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  specialize (filtering_subsequence_prefix_is_filter _ _ _ Hfs m) as Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: stream_prefix ss (S m) =
filter (λ i : nat, P (Str_nth i s))
  (stream_prefix nat_sequence
     (S (Str_nth m ss)))
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  apply f_equal with (f := length) in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: length (stream_prefix ss (S m)) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (S (Str_nth m ss))))
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  rewrite stream_prefix_length in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (S (Str_nth m ss))))
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  rewrite! stream_prefix_S, filter_app in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   filter (λ i : nat, P (Str_nth i s))
     [Str_nth (Str_nth m ss) nat_sequence])
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  unfold filter at 2 in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   list_filter (λ i : nat, P (Str_nth i s))
     (λ x : nat, Pdec (Str_nth x s))
     [Str_nth (Str_nth m ss) nat_sequence])
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m simpl in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if
     decide
       (P
          (Str_nth
             (Str_nth (Str_nth m ss)
                nat_sequence) s))
    then
     Str_nth (Str_nth m ss) nat_sequence
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  rewrite nat_sequence_nth in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then
     Str_nth m ss
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
length (filter P (stream_prefix s (S (Str_nth m ss)))) =
S m
  rewrite stream_prefix_S, filter_app.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then
     Str_nth m ss
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   filter P [Str_nth (Str_nth m ss) s]) = S m
  unfold filter at 2.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then
     Str_nth m ss
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   list_filter P Pdec [Str_nth (Str_nth m ss) s]) =
S m simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then
     Str_nth m ss
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then Str_nth (Str_nth m ss) s :: filter P []
    else filter P [])) = S m
  specialize (filtering_subsequence_witness _ _ _ Hfs m) as Hm.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then
     Str_nth m ss
     :: filter (λ i : nat, P (Str_nth i s))
          []
    else
     filter (λ i : nat, P (Str_nth i s)) []))
Hm: P (Str_nth (Str_nth m ss) s)
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then Str_nth (Str_nth m ss) s :: filter P []
    else filter P [])) = S m
  rewrite decide_True in Hfilter by done.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   Str_nth m ss
   :: filter (λ i : nat, P (Str_nth i s)) [])
Hm: P (Str_nth (Str_nth m ss) s)
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   (if decide (P (Str_nth (Str_nth m ss) s))
    then Str_nth (Str_nth m ss) s :: filter P []
    else filter P [])) = S m
  rewrite decide_True by done.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)) ++
   Str_nth m ss
   :: filter (λ i : nat, P (Str_nth i s)) [])
Hm: P (Str_nth (Str_nth m ss) s)
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   Str_nth (Str_nth m ss) s :: filter P []) = S m
  rewrite app_length, Nat.add_comm in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
length
  (Str_nth m ss
   :: filter (λ i : nat, P (Str_nth i s)) []) +
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence
        (Str_nth m ss)))
Hm: P (Str_nth (Str_nth m ss) s)
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   Str_nth (Str_nth m ss) s :: filter P []) = S m simpl in Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence
           (Str_nth m ss))))
Hm: P (Str_nth (Str_nth m ss) s)
length
  (filter P (stream_prefix s (Str_nth m ss)) ++
   Str_nth (Str_nth m ss) s :: filter P []) = S m
  rewrite app_length, Nat.add_comm.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence
           (Str_nth m ss))))
Hm: P (Str_nth (Str_nth m ss) s)
length (Str_nth (Str_nth m ss) s :: filter P []) +
length (filter P (stream_prefix s (Str_nth m ss))) =
S m simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence
           (Str_nth m ss))))
Hm: P (Str_nth (Str_nth m ss) s)
S (length (filter P (stream_prefix s (Str_nth m ss)))) =
S m
  rewrite Hfilter.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence
           (Str_nth m ss))))
Hm: P (Str_nth (Str_nth m ss) s)
S (length (filter P (stream_prefix s (Str_nth m ss)))) =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence (Str_nth m ss))))
  f_equal.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Hfilter: S m =
S
  (length
     (filter (λ i : nat, P (Str_nth i s))
        (stream_prefix nat_sequence
           (Str_nth m ss))))
Hm: P (Str_nth (Str_nth m ss) s)
length (filter P (stream_prefix s (Str_nth m ss))) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (Str_nth m ss)))
  clear -Hfs.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
length (filter P (stream_prefix s (Str_nth m ss))) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (Str_nth m ss)))
  generalize (Str_nth m ss).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
∀ n : nat,
  length (filter P (stream_prefix s n)) =
  length
    (filter (λ i : nat, P (Str_nth i s))
       (stream_prefix nat_sequence n))
  induction n; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m, n: nat
IHn: length (filter P (stream_prefix s n)) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n))
length (filter P (stream_prefix s (S n))) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence (S n)))
  rewrite !stream_prefix_S, !filter_app, !app_length, IHn.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m, n: nat
IHn: length (filter P (stream_prefix s n)) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n))
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n)) +
length (filter P [Str_nth n s]) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n)) +
length
  (filter (λ i : nat, P (Str_nth i s))
     [Str_nth n nat_sequence])
  f_equal.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m, n: nat
IHn: length (filter P (stream_prefix s n)) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n))
length (filter P [Str_nth n s]) =
length
  (filter (λ i : nat, P (Str_nth i s))
     [Str_nth n nat_sequence]) rewrite nat_sequence_nth.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m, n: nat
IHn: length (filter P (stream_prefix s n)) =
length
  (filter (λ i : nat, P (Str_nth i s))
     (stream_prefix nat_sequence n))
length (filter P [Str_nth n s]) =
length (filter (λ i : nat, P (Str_nth i s)) [n])
  by cbn; case_decide.
Qed.

Lemma filtering_subsequence_prefix_is_filter_last
  {A : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (n : nat)
  (Hn : P (Str_nth n s))
  : Str_nth (length (filter P (stream_prefix s n))) ss = n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Str_nth (length (filter P (stream_prefix s n))) ss = n
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
Str_nth (length (filter P (stream_prefix s n))) ss = n
  specialize (filtering_subsequence_witness_rev _ _ _ Hfs _ Hn) as [k Heqn].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Str_nth (length (filter P (stream_prefix s n))) ss = n
  replace (length _) with k; [by subst |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
k = length (filter P (stream_prefix s n))
  specialize (filtering_subsequence_prefix_length _ _ _ Hfs k) as Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (filter P
     (stream_prefix s (S (Str_nth k ss)))) =
S k
k = length (filter P (stream_prefix s n))
  rewrite! stream_prefix_S, filter_app in Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (filter P (stream_prefix s (Str_nth k ss)) ++
   filter P [Str_nth (Str_nth k ss) s]) =
S k
k = length (filter P (stream_prefix s n))
  unfold filter at 2 in Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (filter P (stream_prefix s (Str_nth k ss)) ++
   list_filter P Pdec
     [Str_nth (Str_nth k ss) s]) = 
S k
k = length (filter P (stream_prefix s n)) simpl in Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (filter P (stream_prefix s (Str_nth k ss)) ++
   (if decide (P (Str_nth (Str_nth k ss) s))
    then
     Str_nth (Str_nth k ss) s :: filter P []
    else filter P [])) = 
S k
k = length (filter P (stream_prefix s n))
  rewrite decide_True in Hlength by (subst; done).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (filter P (stream_prefix s (Str_nth k ss)) ++
   Str_nth (Str_nth k ss) s :: filter P []) =
S k
k = length (filter P (stream_prefix s n))
  rewrite app_length, Nat.add_comm in Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: length
  (Str_nth (Str_nth k ss) s :: filter P []) +
length
  (filter P (stream_prefix s (Str_nth k ss))) =
S k
k = length (filter P (stream_prefix s n)) simpl in Hlength.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
Hn: P (Str_nth n s)
k: nat
Heqn: n = Str_nth k ss
Hlength: S
  (length
     (filter P
        (stream_prefix s (Str_nth k ss)))) =
S k
k = length (filter P (stream_prefix s n))
  by inversion Hlength; subst.
Qed.

Given a filtering_subsequence for property P over a stream s and a function f transforming elements with property P, we can define the filtering of s by P mapped through the function f.

Definition filtering_subsequence_stream_filter_map
  {A B : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (f : dsig P -> B)
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  : Stream B
  := map (fun k => f (dexist _ (filtering_subsequence_witness P s ss Hfs k))) nat_sequence.

Connecting prefixes of filtering_subsequence_stream_filter_map with list_filter_maps on prefixes.

Lemma fitering_subsequence_stream_filter_map_prefix
  {A B : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (f : dsig P -> B)
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (n : nat)
  (pre_filter_map := list_filter_map P f (stream_prefix s n))
  (m := length pre_filter_map)
  : stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m = pre_filter_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
pre_filter_map:= list_filter_map P f
  (stream_prefix s n): list B
m:= length pre_filter_map: nat
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs) m = pre_filter_map
Proof.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
pre_filter_map:= list_filter_map P f
  (stream_prefix s n): list B
m:= length pre_filter_map: nat
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs) m = pre_filter_map
  subst m pre_filter_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
  induction n; [done |].A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length
     (list_filter_map P f (stream_prefix s (S n)))) =
list_filter_map P f (stream_prefix s (S n))
  rewrite stream_prefix_S, list_filter_map_app, app_length.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   length (list_filter_map P f [Str_nth n s])) =
list_filter_map P f (stream_prefix s n) ++
list_filter_map P f [Str_nth n s]
  remember (list_filter_map P f [Str_nth n s]) as lst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
lst: list B
Heqlst: lst = list_filter_map P f [Str_nth n s]
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   length lst) =
list_filter_map P f (stream_prefix s n) ++ lst
  unfold list_filter_map in Heqlst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
lst: list B
Heqlst: lst =
List.map f (filter_annotate P [Str_nth n s])
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   length lst) =
list_filter_map P f (stream_prefix s n) ++ lst
  rewrite filter_annotate_unroll in Heqlst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
lst: list B
Heqlst: lst =
List.map f
  (let fa := filter_annotate P [] in
   match decide (P (Str_nth n s)) with
   | left pa => dexist (Str_nth n s) pa :: fa
   | right _ => fa
   end)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   length lst) =
list_filter_map P f (stream_prefix s n) ++ lst simpl in Heqlst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
lst: list B
Heqlst: lst =
List.map f
  match decide (P (Str_nth n s)) with
  | left pa => [dexist (Str_nth n s) pa]
  | right _ => []
  end
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   length lst) =
list_filter_map P f (stream_prefix s n) ++ lst
  case_decide; subst lst; simpl; [| by rewrite Nat.add_comm, app_nil_r].A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n)) +
   1) =
list_filter_map P f (stream_prefix s n) ++
[f (dexist (Str_nth n s) H)]
  replace (length (list_filter_map P f (stream_prefix s n)) + 1)
    with (S (length (list_filter_map P f (stream_prefix s n))))
    by lia.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (S
     (length (list_filter_map P f (stream_prefix s n)))) =
list_filter_map P f (stream_prefix s n) ++
[f (dexist (Str_nth n s) H)]
  rewrite stream_prefix_S.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length (list_filter_map P f (stream_prefix s n))) ++
[Str_nth
   (length (list_filter_map P f (stream_prefix s n)))
   (filtering_subsequence_stream_filter_map P f s ss
      Hfs)] =
list_filter_map P f (stream_prefix s n) ++
[f (dexist (Str_nth n s) H)]
  rewrite IHn.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
list_filter_map P f (stream_prefix s n) ++
[Str_nth
   (length (list_filter_map P f (stream_prefix s n)))
   (filtering_subsequence_stream_filter_map P f s ss
      Hfs)] =
list_filter_map P f (stream_prefix s n) ++
[f (dexist (Str_nth n s) H)]
  f_equal.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
[Str_nth
   (length (list_filter_map P f (stream_prefix s n)))
   (filtering_subsequence_stream_filter_map P f s ss
      Hfs)] = [f (dexist (Str_nth n s) H)] f_equal.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (length (list_filter_map P f (stream_prefix s n)))
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs) = f (dexist (Str_nth n s) H)
  unfold filtering_subsequence_stream_filter_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (length (list_filter_map P f (stream_prefix s n)))
  (map
     (λ k : nat,
        f
          (dexist (Str_nth (Str_nth k ss) s)
             (filtering_subsequence_witness P s ss Hfs
                k))) nat_sequence) =
f (dexist (Str_nth n s) H)
  rewrite Str_nth_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
f
  (dexist
     (Str_nth
        (Str_nth
           (Str_nth
              (length
                 (list_filter_map P f
                    (stream_prefix s n))) nat_sequence)
           ss) s)
     (filtering_subsequence_witness P s ss Hfs
        (Str_nth
           (length
              (list_filter_map P f (stream_prefix s n)))
           nat_sequence))) =
f (dexist (Str_nth n s) H)
  f_equal.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
dexist
  (Str_nth
     (Str_nth
        (Str_nth
           (length
              (list_filter_map P f (stream_prefix s n)))
           nat_sequence) ss) s)
  (filtering_subsequence_witness P s ss Hfs
     (Str_nth
        (length
           (list_filter_map P f (stream_prefix s n)))
        nat_sequence)) = dexist (Str_nth n s) H apply dsig_eq.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
`(dexist
    (Str_nth
       (Str_nth
          (Str_nth
             (length
                (list_filter_map P f
                   (stream_prefix s n))) nat_sequence)
          ss) s)
    (filtering_subsequence_witness P s ss Hfs
       (Str_nth
          (length
             (list_filter_map P f (stream_prefix s n)))
          nat_sequence))) = `(dexist (Str_nth n s) H)
  simpl.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (Str_nth
     (Str_nth
        (length
           (list_filter_map P f (stream_prefix s n)))
        nat_sequence) ss) s = Str_nth n s rewrite nat_sequence_nth.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (Str_nth
     (length (list_filter_map P f (stream_prefix s n)))
     ss) s = Str_nth n s
  f_equal.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (length (list_filter_map P f (stream_prefix s n)))
  ss = n
  unfold list_filter_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (length
     (List.map f
        (filter_annotate P (stream_prefix s n)))) ss =
n
  rewrite map_length.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth
  (length (filter_annotate P (stream_prefix s n))) ss =
n rewrite filter_annotate_length.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
n: nat
IHn: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f (stream_prefix s n))) =
list_filter_map P f (stream_prefix s n)
H: P (Str_nth n s)
Str_nth (length (filter P (stream_prefix s n))) ss = n
  by apply filtering_subsequence_prefix_is_filter_last.
Qed.

Program Definition fitering_subsequence_stream_filter_map_prefix_ex
  {A B : Type}
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  (f : dsig P -> B)
  (s : Stream A)
  (ss : Stream nat)
  (Hfs : filtering_subsequence P s ss)
  (m : nat)
  : {n : nat |
      stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m =
      list_filter_map P f (stream_prefix s n)}
  :=
  match m with
  | 0 => exist _ 0 _
  | S m => exist _ (S (Str_nth m ss)) _
  end.
Next Obligation.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (s : Stream A) (ss : Stream nat) 
  (Hfs : filtering_subsequence P s ss) (m : nat),
  0 = m
  → (λ n : nat,
       stream_prefix
         (filtering_subsequence_stream_filter_map P f
            s ss Hfs) 0 =
       list_filter_map P f (stream_prefix s n)) 0
Proof.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (s : Stream A) (ss : Stream nat) 
  (Hfs : filtering_subsequence P s ss) (m : nat),
  0 = m
  → (λ n : nat,
       stream_prefix
         (filtering_subsequence_stream_filter_map P f
            s ss Hfs) 0 =
       list_filter_map P f (stream_prefix s n)) 0 done. Qed.
Next Obligation.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (s : Stream A) (ss : Stream nat) 
  (Hfs : filtering_subsequence P s ss) (m0 m : nat),
  S m = m0
  → (λ n : nat,
       stream_prefix
         (filtering_subsequence_stream_filter_map P f
            s ss Hfs) (S m) =
       list_filter_map P f (stream_prefix s n))
      (S (Str_nth m ss))
Proof.∀ (A B : Type) (P : A → Prop) (Pdec : ∀ a : A,
                                        Decision (P a)) 
  (f : dsig P → B) (s : Stream A) (ss : Stream nat) 
  (Hfs : filtering_subsequence P s ss) (m0 m : nat),
  S m = m0
  → (λ n : nat,
       stream_prefix
         (filtering_subsequence_stream_filter_map P f
            s ss Hfs) (S m) =
       list_filter_map P f (stream_prefix s n))
      (S (Str_nth m ss))
  intros.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m0, m: nat
Heq_m: S m = m0
(λ n : nat,
   stream_prefix
     (filtering_subsequence_stream_filter_map P f s ss
        Hfs) (S m) =
   list_filter_map P f (stream_prefix s n))
  (S (Str_nth m ss)) subst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
(λ n : nat,
   stream_prefix
     (filtering_subsequence_stream_filter_map P f s ss
        Hfs) (S m) =
   list_filter_map P f (stream_prefix s n))
  (S (Str_nth m ss))
  specialize (fitering_subsequence_stream_filter_map_prefix P f _ _ Hfs (S (Str_nth m ss))) as Heq.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: let pre_filter_map :=
  list_filter_map P f
    (stream_prefix s (S (Str_nth m ss))) in
let m := length pre_filter_map in
stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs) m = pre_filter_map
(λ n : nat,
   stream_prefix
     (filtering_subsequence_stream_filter_map P f s ss
        Hfs) (S m) =
   list_filter_map P f (stream_prefix s n))
  (S (Str_nth m ss))
  remember (S m) as Sm.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: let pre_filter_map :=
  list_filter_map P f
    (stream_prefix s (S (Str_nth m ss))) in
let m := length pre_filter_map in
stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs) m = pre_filter_map
Sm: nat
HeqSm: Sm = S m
(λ n : nat,
   stream_prefix
     (filtering_subsequence_stream_filter_map P f s ss
        Hfs) Sm =
   list_filter_map P f (stream_prefix s n))
  (S (Str_nth m ss))
  simpl in *.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs) Sm =
list_filter_map P f
  match s with
  | Cons a l => a :: stream_prefix l (Str_nth m ss)
  end
  rewrite <- Heq.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs) Sm =
stream_prefix
  (filtering_subsequence_stream_filter_map P f s ss
     Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end))
  f_equal.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
Sm =
length
  (list_filter_map P f
     match s with
     | Cons a l => a :: stream_prefix l (Str_nth m ss)
     end)
  unfold list_filter_map.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
Sm =
length
  (List.map f
     (filter_annotate P
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end))
  rewrite map_length.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
Sm =
length
  (filter_annotate P
     match s with
     | Cons a l => a :: stream_prefix l (Str_nth m ss)
     end) rewrite filter_annotate_length.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
Sm =
length
  (filter P
     match s with
     | Cons a l => a :: stream_prefix l (Str_nth m ss)
     end)
  symmetry.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
Sm: nat
HeqSm: Sm = S m
length
  (filter P
     match s with
     | Cons a l => a :: stream_prefix l (Str_nth m ss)
     end) = Sm subst.A, B: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
f: dsig P → B
s: Stream A
ss: Stream nat
Hfs: filtering_subsequence P s ss
m: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map P f s
     ss Hfs)
  (length
     (list_filter_map P f
        match s with
        | Cons a l =>
            a :: stream_prefix l (Str_nth m ss)
        end)) =
list_filter_map P f
  match s with
  | Cons a l =>
      a :: stream_prefix l (Str_nth m ss)
  end
length
  (filter P
     match s with
     | Cons a l => a :: stream_prefix l (Str_nth m ss)
     end) = S m
  by apply filtering_subsequence_prefix_length.
Qed.

Lemma stream_filter_Forall
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  (ss : Stream nat)
  (s' := stream_subsequence s ss)
  (Hfs : filtering_subsequence P s ss)
  : ForAll1 P s'.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
ForAll1 P s'
Proof.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
ForAll1 P s'
  apply ForAll1_forall.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
∀ n : nat, P (Str_nth n s')
  intro n.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
n: nat
P (Str_nth n s')
  unfold s'.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
n: nat
P (Str_nth n (stream_subsequence s ss))
  unfold stream_subsequence.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
n: nat
P (Str_nth n (map (λ k : nat, Str_nth k s) ss))
  rewrite Str_nth_map.A: Type
P: A → Prop
s: Stream A
ss: Stream nat
s':= stream_subsequence s ss: Stream A
Hfs: filtering_subsequence P s ss
n: nat
P (Str_nth (Str_nth n ss) s)
  by apply filtering_subsequence_witness.
Qed.

Obtaining filtering_sequences for streams

Given a stream, a decidable predicate on its elements, and a guarantee that the predicates holds InfinitelyOften on the elements of the stream, we can (coinductively) obtain a filtering_sequence.

The approach below follows closely the one proposed by the following paper, except that instead of obtaining the filtered sequence itself we obtain the stream of all positions corresponding to the filtered sequence.

Yves Bertot. Filters on Co-Inductive streams: an application to Eratosthenes’ sieve. RR-5343, INRIA. 2004, pp.21. ffinria-00070658 https://hal.inria.fr/inria-00070658/document

Section sec_stream_filter_positions.

Context
  [A : Type]
  (P : A -> Prop)
  {Pdec : forall a, Decision (P a)}
  .

Given a stream s and a proof that there exists an element of s for which P holds, computes the first position of s in which P holds (shifted by the given argument n) and the remainder of s after that position.

The definition iterates looking for the first position in which P holds, termination being ensured by the fact that Exists1 is inductive.

Fixpoint stream_filter_fst_pos
  (s : Stream A)
  (Hev : Exists1 P s)
  (n : nat)
  {struct Hev}
  : nat * Stream A.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
stream_filter_fst_pos: ∀ s : Stream A,
  Exists1 P s
  → nat → nat * Stream A
s: Stream A
Hev: Exists1 P s
n: nat
(nat * Stream A)%type
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
stream_filter_fst_pos: ∀ s : Stream A,
  Exists1 P s
  → nat → nat * Stream A
s: Stream A
Hev: Exists1 P s
n: nat
(nat * Stream A)%type
  refine
    (match decide (P (hd s)) with
      | left p => (n, tl s)
      | right _ =>
        stream_filter_fst_pos (tl s) _ (S n)
     end).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
stream_filter_fst_pos: ∀ s : Stream A,
  Exists1 P s
  → nat → nat * Stream A
s: Stream A
Hev: Exists1 P s
n: nat
n0: ¬ P (hd s)
Exists1 P (tl s)
  by destruct Hev.
Defined.

Lemma stream_filter_fst_pos_characterization
  (s : Stream A)
  (Hev : Exists1 P s)
  (n : nat)
  : exists k,
    stream_filter_fst_pos s Hev n = (n + k, Str_nth_tl (S k) s) /\
    P (Str_nth k s) /\ (forall i, i < k -> ~ P (Str_nth i s)).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
∃ k : nat,
  stream_filter_fst_pos s Hev n =
  (n + k, Str_nth_tl (S k) s)
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
∃ k : nat,
  stream_filter_fst_pos s Hev n =
  (n + k, Str_nth_tl (S k) s)
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
  revert s Hev n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
  fix H 2.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
  intros.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists1 P s
n: nat
∃ k : nat,
  stream_filter_fst_pos s Hev n =
  (n + k, Str_nth_tl (S k) s)
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
  destruct Hev; simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
p: P (hd s)
n: nat
∃ k : nat,
  match decide (P (hd s)) with
  | left _ => (n, tl s)
  | right n0 =>
      stream_filter_fst_pos (tl s)
        (False_ind (Exists1 P (tl s)) (n0 p)) (S n)
  end = (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
∃ k : nat,
  (if decide (P (hd s))
   then (n, tl s)
   else stream_filter_fst_pos (tl s) Hev (S n)) =
  (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
p: P (hd s)
n: nat
∃ k : nat,
  match decide (P (hd s)) with
  | left _ => (n, tl s)
  | right n0 =>
      stream_filter_fst_pos (tl s)
        (False_ind (Exists1 P (tl s)) (n0 p)) (S n)
  end = (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s)) destruct (decide _); [| done].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
p: P (hd s)
n: nat
p0: P (hd s)
∃ k : nat,
  (n, tl s) = (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
    by exists 0; split_and!; f_equal; [lia | | lia].
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
∃ k : nat,
  (if decide (P (hd s))
   then (n, tl s)
   else stream_filter_fst_pos (tl s) Hev (S n)) =
  (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s)) destruct (decide _); simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
p: P (hd s)
∃ k : nat,
  (n, tl s) = (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
∃ k : nat,
  stream_filter_fst_pos (tl s) Hev (S n) =
  (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
p: P (hd s)
∃ k : nat,
  (n, tl s) = (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s)) by exists 0; split_and!; f_equal; [lia | | lia].
    +A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hev : Exists1 P s) (n : nat),
  ∃ k : nat,
    stream_filter_fst_pos s Hev n =
    (n + k, Str_nth_tl (S k) s)
    ∧ P (Str_nth k s)
      ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
∃ k : nat,
  stream_filter_fst_pos (tl s) Hev (S n) =
  (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s)) specialize (H (tl s) Hev (S n)) as (k & Heq & Hp & Hnp).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
∃ k : nat,
  stream_filter_fst_pos (tl s) Hev (S n) =
  (n + k, Str_nth_tl k (tl s))
  ∧ P (Str_nth k s)
    ∧ (∀ i : nat, i < k → ¬ P (Str_nth i s))
      exists (S k).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
stream_filter_fst_pos (tl s) Hev (S n) =
(n + S k, Str_nth_tl (S k) (tl s))
∧ P (Str_nth (S k) s)
  ∧ (∀ i : nat, i < S k → ¬ P (Str_nth i s)) rewrite Heq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
(S n + k, Str_nth_tl (S k) (tl s)) =
(n + S k, Str_nth_tl (S k) (tl s))
∧ P (Str_nth (S k) s)
  ∧ (∀ i : nat, i < S k → ¬ P (Str_nth i s))
      split; [f_equal; lia |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
P (Str_nth (S k) s)
∧ (∀ i : nat, i < S k → ¬ P (Str_nth i s))
      split; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
∀ i : nat, i < S k → ¬ P (Str_nth i s)
      intros.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
i: nat
H: i < S k
¬ P (Str_nth i s) destruct i; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists (λ s : Stream A, P (hd s)) (tl s)
n: nat
n0: ¬ P (hd s)
k: nat
Heq: stream_filter_fst_pos (tl s) Hev (S n) =
(S n + k, Str_nth_tl (S k) (tl s))
Hp: P (Str_nth k (tl s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (tl s))
i: nat
H: S i < S k
¬ P (Str_nth (S i) s)
      by apply Hnp; lia.
Qed.

Lemma stream_filter_fst_pos_infinitely_often
  (s : Stream A)
  (Hev : Exists1 P s)
  (n : nat)
  : InfinitelyOften P s -> InfinitelyOften P (stream_filter_fst_pos s Hev n).2.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
InfinitelyOften P s
→ InfinitelyOften P (stream_filter_fst_pos s Hev n).2
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
InfinitelyOften P s
→ InfinitelyOften P (stream_filter_fst_pos s Hev n).2
  destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n, k: nat
InfinitelyOften P s
→ InfinitelyOften P (n + k, Str_nth_tl (S k) s).2
  by apply InfinitelyOften_nth_tl.
Qed.

Lemma stream_filter_fst_pos_le
  (s : Stream A)
  (Hev : Exists1 P s)
  (n : nat)
  : n <= (stream_filter_fst_pos s Hev n).1.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
n ≤ (stream_filter_fst_pos s Hev n).1
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n: nat
n ≤ (stream_filter_fst_pos s Hev n).1
  destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hev: Exists1 P s
n, k: nat
n ≤ (n + k, Str_nth_tl (S k) s).1
  by cbn; lia.
Qed.

Lemma stream_filter_fst_pos_nth_tl_has_property
  (s : Stream A)
  (n : nat)
  (sn := Str_nth_tl n s)
  (Hev : Exists1 P sn)
  (fpair := stream_filter_fst_pos (Str_nth_tl n s) Hev n)
  : P (Str_nth fpair.1 s) /\
    forall i, n <= i < fpair.1 -> ~ P (Str_nth i s).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
sn:= Str_nth_tl n s: Stream A
Hev: Exists1 P sn
fpair:= stream_filter_fst_pos (Str_nth_tl n s) Hev n: (nat * Stream A)%type
P (Str_nth fpair.1 s)
∧ (∀ i : nat, n <= i < fpair.1 → ¬ P (Str_nth i s))
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
sn:= Str_nth_tl n s: Stream A
Hev: Exists1 P sn
fpair:= stream_filter_fst_pos (Str_nth_tl n s) Hev n: (nat * Stream A)%type
P (Str_nth fpair.1 s)
∧ (∀ i : nat, n <= i < fpair.1 → ¬ P (Str_nth i s))
  specialize (stream_filter_fst_pos_characterization sn Hev n)
    as [k [Heq [Hp Hnp]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
sn:= Str_nth_tl n s: Stream A
Hev: Exists1 P sn
fpair:= stream_filter_fst_pos (Str_nth_tl n s) Hev n: (nat * Stream A)%type
k: nat
Heq: stream_filter_fst_pos sn Hev n =
(n + k, Str_nth_tl (S k) sn)
Hp: P (Str_nth k sn)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i sn)
P (Str_nth fpair.1 s)
∧ (∀ i : nat, n <= i < fpair.1 → ¬ P (Str_nth i s))
  subst sn fpair.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
Hev: Exists1 P (Str_nth_tl n s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl n s) Hev n =
(n + k, Str_nth_tl (S k) (Str_nth_tl n s))
Hp: P (Str_nth k (Str_nth_tl n s))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl n s))
P
  (Str_nth
     (stream_filter_fst_pos (Str_nth_tl n s) Hev n).1
     s)
∧ (∀ i : nat,
     n <= i <
     (stream_filter_fst_pos (Str_nth_tl n s) Hev n).1
     → ¬ P (Str_nth i s))
  rewrite Heq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
Hev: Exists1 P (Str_nth_tl n s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl n s) Hev n =
(n + k, Str_nth_tl (S k) (Str_nth_tl n s))
Hp: P (Str_nth k (Str_nth_tl n s))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl n s))
P
  (Str_nth
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1 s)
∧ (∀ i : nat,
     n <= i <
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
     → ¬ P (Str_nth i s))
  clear -Hp Hnp.A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth k (Str_nth_tl n s))
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
P
  (Str_nth
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1 s)
∧ (∀ i : nat,
     n <= i <
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
     → ¬ P (Str_nth i s)) rewrite Str_nth_plus, Nat.add_comm in Hp.A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth (n + k) s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
P
  (Str_nth
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1 s)
∧ (∀ i : nat,
     n <= i <
     (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
     → ¬ P (Str_nth i s))
  split; [done |].A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth (n + k) s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
∀ i : nat,
  n <= i <
  (n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
  → ¬ P (Str_nth i s)
  intros i [Hlt_i Hilt].A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth (n + k) s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
i: nat
Hlt_i: n ≤ i
Hilt: i <
(n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
¬ P (Str_nth i s)
  apply stdpp_nat_le_sum in Hlt_i as [i' ->].A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth (n + k) s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
i': nat
Hilt: n + i' <
(n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
¬ P (Str_nth (n + i') s)
  rewrite Nat.add_comm, <- Str_nth_plus.A: Type
P: A → Prop
s: Stream A
n, k: nat
Hp: P (Str_nth (n + k) s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i (Str_nth_tl n s))
i': nat
Hilt: n + i' <
(n + k, Str_nth_tl (S k) (Str_nth_tl n s)).1
¬ P (Str_nth i' (Str_nth_tl n s))
  by apply Hnp; cbn in *; lia.
Qed.

Given as stream s for which predicate P holds InfinitelyOften produces the streams of all its position at which P holds in a strictly increasing order (shifted by the given argument n).

CoFixpoint stream_filter_positions
  (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat) : Stream nat :=
  let fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n in
  Cons fpair.1 (stream_filter_positions fpair.2
    (stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf)  (S fpair.1)).

Lemma stream_filter_positions_unroll (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
  (fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n)
  : stream_filter_positions s Hinf n =
    Cons fpair.1 (stream_filter_positions fpair.2
      (stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf)  (S fpair.1)).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
fpair:= stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n: (nat * Stream A)%type
stream_filter_positions s Hinf n =
Cons fpair.1
  (stream_filter_positions fpair.2
     (stream_filter_fst_pos_infinitely_often s
        (fHere (Exists1 P) s Hinf) n Hinf) (S fpair.1))
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
fpair:= stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n: (nat * Stream A)%type
stream_filter_positions s Hinf n =
Cons fpair.1
  (stream_filter_positions fpair.2
     (stream_filter_fst_pos_infinitely_often s
        (fHere (Exists1 P) s Hinf) n Hinf) (S fpair.1))
  by rewrite <- recons at 1.
Qed.

Lemma stream_filter_positions_Str_nth_tl
  (s : Stream A) (Hinf : InfinitelyOften P s) (n0 : nat) (n : nat)
  : exists kn (Hinf' : InfinitelyOften P (Str_nth_tl (S kn) s)),
    Str_nth_tl n (stream_filter_positions s Hinf n0) =
    Cons (n0 + kn) (stream_filter_positions (Str_nth_tl (S kn) s) Hinf' (S (n0 + kn))) /\
    P (Str_nth kn s).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
  induction n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl 0 (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n: nat
IHn: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n
    (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions
       (Str_nth_tl (S kn) s) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl (S n) (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions 
       (Str_nth_tl (S kn) s) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl 0 (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s) simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  stream_filter_positions s Hinf n0 =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl kn (tl s))
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s) rewrite (stream_filter_positions_unroll s Hinf n0).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0: nat
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl kn (tl s))
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    specialize
      (stream_filter_fst_pos_characterization s (fHere _ s Hinf) n0)
        as [k [Heq [Hp _]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl kn (tl s))
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    assert (Hk : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).1 = n0 + k).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
(stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).1 =
n0 + k
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions 
       (Str_nth_tl kn (tl s)) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
    {A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
(stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).1 =
n0 + k by rewrite Heq. }A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl kn (tl s))
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    assert (Htl : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).2 = Str_nth_tl (S k) s).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
(stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).2 =
Str_nth_tl (S k) s
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
Htl: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).2 =
Str_nth_tl (S k) s
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions 
       (Str_nth_tl kn (tl s)) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
    {A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
(stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).2 =
Str_nth_tl (S k) s by rewrite Heq. }A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
Htl: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).2 =
Str_nth_tl (S k) s
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn (tl s))),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl kn (tl s))
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    exists k.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) n0 =
(n0 + k, Str_nth_tl (S k) s)
Hp: P (Str_nth k s)
Hk: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).1 = 
n0 + k
Htl: (stream_filter_fst_pos s
   (fHere (Exists1 P) s Hinf) n0).2 =
Str_nth_tl (S k) s
∃ Hinf' : InfinitelyOften P (Str_nth_tl k (tl s)),
  Cons
    (stream_filter_fst_pos s
       (fHere (Exists1 P) s Hinf) n0).1
    (stream_filter_positions
       (stream_filter_fst_pos s
          (fHere (Exists1 P) s Hinf) n0).2
       (stream_filter_fst_pos_infinitely_often s
          (fHere (Exists1 P) s Hinf) n0 Hinf)
       (S
          (stream_filter_fst_pos s
             (fHere (Exists1 P) s Hinf) n0).1)) =
  Cons (n0 + k)
    (stream_filter_positions (Str_nth_tl k (tl s))
       Hinf' (S (n0 + k))) ∧ P (Str_nth k s)
    by rewrite Hk; cbn in *; rewrite <- Htl; eauto.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n: nat
IHn: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n
    (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions
       (Str_nth_tl (S kn) s) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl (S n) (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s) replace
      (Str_nth_tl (S n) (stream_filter_positions s Hinf n0))
      with (tl (Str_nth_tl n (stream_filter_positions s Hinf n0)))
      by apply tl_nth_tl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n: nat
IHn: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n
    (stream_filter_positions s Hinf n0) =
  Cons (n0 + kn)
    (stream_filter_positions
       (Str_nth_tl (S kn) s) Hinf' 
       (S (n0 + kn))) ∧ P (Str_nth kn s)
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  tl
    (Str_nth_tl n (stream_filter_positions s Hinf n0)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    destruct IHn as [kn [Hinfn [Hsn Hpn]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  tl
    (Str_nth_tl n (stream_filter_positions s Hinf n0)) =
  Cons (n0 + kn)
    (stream_filter_positions (Str_nth_tl (S kn) s)
       Hinf' (S (n0 + kn))) ∧ P (Str_nth kn s)
    rewrite Hsn.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
∃ (kn0 : nat) (Hinf' : InfinitelyOften P
                         (Str_nth_tl (S kn0) s)),
  tl
    (Cons (n0 + kn)
       (stream_filter_positions (Str_nth_tl (S kn) s)
          Hinfn (S (n0 + kn)))) =
  Cons (n0 + kn0)
    (stream_filter_positions (Str_nth_tl (S kn0) s)
       Hinf' (S (n0 + kn0))) ∧ P (Str_nth kn0 s)
    simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
∃ (kn0 : nat) (Hinf' : InfinitelyOften P
                         (Str_nth_tl kn0 (tl s))),
  stream_filter_positions (Str_nth_tl kn (tl s)) Hinfn
    (S (n0 + kn)) =
  Cons (n0 + kn0)
    (stream_filter_positions (Str_nth_tl kn0 (tl s))
       Hinf' (S (n0 + kn0))) ∧ P (Str_nth kn0 s) rewrite (stream_filter_positions_unroll (Str_nth_tl kn (tl s)) Hinfn (S (n0 + kn))).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
∃ (kn0 : nat) (Hinf' : InfinitelyOften P
                         (Str_nth_tl kn0 (tl s))),
  Cons
    (stream_filter_fst_pos (Str_nth_tl kn (tl s))
       (fHere (Exists1 P) (Str_nth_tl kn (tl s)) Hinfn)
       (S (n0 + kn))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (stream_filter_fst_pos
             (Str_nth_tl kn (tl s))
             (fHere (Exists1 P) (Str_nth_tl kn (tl s))
                Hinfn) (S (n0 + kn))).1)) =
  Cons (n0 + kn0)
    (stream_filter_positions (Str_nth_tl kn0 (tl s))
       Hinf' (S (n0 + kn0))) ∧ P (Str_nth kn0 s)
    specialize
      (stream_filter_fst_pos_characterization (Str_nth_tl kn (tl s)) (fHere _ _ Hinfn) (S (n0 + kn)))
        as [k [Heq [Hp _]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl (S kn) s) Hinfn)
  (S (n0 + kn)) =
(S (n0 + kn) + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
∃ (kn0 : nat) (Hinf' : InfinitelyOften P
                         (Str_nth_tl kn0 (tl s))),
  Cons
    (stream_filter_fst_pos (Str_nth_tl kn (tl s))
       (fHere (Exists1 P) (Str_nth_tl kn (tl s)) Hinfn)
       (S (n0 + kn))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (stream_filter_fst_pos
             (Str_nth_tl kn (tl s))
             (fHere (Exists1 P) (Str_nth_tl kn (tl s))
                Hinfn) (S (n0 + kn))).1)) =
  Cons (n0 + kn0)
    (stream_filter_positions (Str_nth_tl kn0 (tl s))
       Hinf' (S (n0 + kn0))) ∧ P (Str_nth kn0 s)
    exists (S (k + kn)).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl (S kn) s) Hinfn)
  (S (n0 + kn)) =
(S (n0 + kn) + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (S (k + kn)) (tl s)),
  Cons
    (stream_filter_fst_pos (Str_nth_tl kn (tl s))
       (fHere (Exists1 P) (Str_nth_tl kn (tl s)) Hinfn)
       (S (n0 + kn))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (stream_filter_fst_pos
             (Str_nth_tl kn (tl s))
             (fHere (Exists1 P) (Str_nth_tl kn (tl s))
                Hinfn) (S (n0 + kn))).1)) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (S (k + kn)) (tl s)) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    cbn in Heq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (S (k + kn)) (tl s)),
  Cons
    (stream_filter_fst_pos (Str_nth_tl kn (tl s))
       (fHere (Exists1 P) (Str_nth_tl kn (tl s)) Hinfn)
       (S (n0 + kn))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (stream_filter_fst_pos
             (Str_nth_tl kn (tl s))
             (fHere (Exists1 P) (Str_nth_tl kn (tl s))
                Hinfn) (S (n0 + kn))).1)) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (S (k + kn)) (tl s)) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    apply (f_equal fst) in Heq as Hk; rewrite Hk.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (S (k + kn)) (tl s)),
  Cons
    (S (n0 + kn + k),
     Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (S (n0 + kn + k),
           Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1)) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (S (k + kn)) (tl s)) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    apply (f_equal snd) in Heq as Htl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
Htl: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).2 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).2
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (S (k + kn)) (tl s)),
  Cons
    (S (n0 + kn + k),
     Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S
          (S (n0 + kn + k),
           Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1)) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (S (k + kn)) (tl s)) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    simpl in Htl |- *.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
Htl: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).2 =
Str_nth_tl k (tl (Str_nth_tl kn (tl s)))
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (k + kn) (tl (tl s))),
  Cons (S (n0 + kn + k))
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S (S (n0 + kn + k)))) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (k + kn) (tl (tl s))) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    rewrite tl_nth_tl, Str_nth_tl_plus in Htl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth k (Str_nth_tl kn (tl s)))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
Htl: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).2 =
Str_nth_tl (k + kn) (tl (tl s))
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (k + kn) (tl (tl s))),
  Cons (S (n0 + kn + k))
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S (S (n0 + kn + k)))) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (k + kn) (tl (tl s))) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    rewrite Str_nth_plus in Hp.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth (k + kn) (tl s))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
Htl: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).2 =
Str_nth_tl (k + kn) (tl (tl s))
∃ Hinf' : InfinitelyOften P
            (Str_nth_tl (k + kn) (tl (tl s))),
  Cons (S (n0 + kn + k))
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S (S (n0 + kn + k)))) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (Str_nth_tl (k + kn) (tl (tl s))) Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    rewrite <- Htl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n0, n, kn: nat
Hinfn: InfinitelyOften P (Str_nth_tl (S kn) s)
Hsn: Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn)
  (stream_filter_positions 
     (Str_nth_tl (S kn) s) Hinfn 
     (S (n0 + kn)))
Hpn: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hinfn) (S (n0 + kn)) =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s))))
Hp: P (Str_nth (k + kn) (tl s))
Hk: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).1 =
(S (n0 + kn + k),
 Str_nth_tl k (tl (Str_nth_tl kn (tl s)))).1
Htl: (stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s))
      Hinfn) (S (n0 + kn))).2 =
Str_nth_tl (k + kn) (tl (tl s))
∃ Hinf' : InfinitelyOften P
            (stream_filter_fst_pos
               (Str_nth_tl kn (tl s))
               (fHere (Exists1 P)
                  (Str_nth_tl kn (tl s)) Hinfn)
               (S (n0 + kn))).2,
  Cons (S (n0 + kn + k))
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2
       (stream_filter_fst_pos_infinitely_often
          (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn)) Hinfn)
       (S (S (n0 + kn + k)))) =
  Cons (n0 + S (k + kn))
    (stream_filter_positions
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hinfn) (S (n0 + kn))).2 Hinf'
       (S (n0 + S (k + kn))))
  ∧ P (Str_nth (S (k + kn)) s)
    by replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia; eauto.
Qed.

Lemma stream_filter_positions_monotone
  (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
  : monotone_nat_stream_prop (stream_filter_positions s Hinf n).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
monotone_nat_stream_prop
  (stream_filter_positions s Hinf n)
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
monotone_nat_stream_prop
  (stream_filter_positions s Hinf n)
  apply monotone_nat_stream_prop_from_successor.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
ForAll2 lt (stream_filter_positions s Hinf n)
  revert s Hinf n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat),
  ForAll2 lt (stream_filter_positions s Hinf n)
  cofix H.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hinf : InfinitelyOften P s) 
  (n : nat),
  ForAll2 lt (stream_filter_positions s Hinf n)
∀ (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat),
  ForAll2 lt (stream_filter_positions s Hinf n)
  intros.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hinf : InfinitelyOften P s) 
  (n : nat),
  ForAll2 lt (stream_filter_positions s Hinf n)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
ForAll2 lt (stream_filter_positions s Hinf n)
  constructor; simpl; [| by apply H].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
H: ∀ (s : Stream A) (Hinf : InfinitelyOften P s) 
  (n : nat),
  ForAll2 lt (stream_filter_positions s Hinf n)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
(stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n).1 <
(stream_filter_fst_pos
   (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf)
      n).2
   (fHere (Exists1 P)
      (stream_filter_fst_pos s
         (fHere (Exists1 P) s Hinf) n).2
      (stream_filter_fst_pos_infinitely_often s
         (fHere (Exists1 P) s Hinf) n Hinf))
   (S
      (stream_filter_fst_pos s
         (fHere (Exists1 P) s Hinf) n).1)).1
  by apply stream_filter_fst_pos_le.
Qed.

stream_filter_positions produces a filtering_sequence.

Lemma stream_filter_positions_filtering_subsequence
  (s : Stream A) (Hinf : InfinitelyOften P s)
  : filtering_subsequence P s (stream_filter_positions s Hinf 0).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
filtering_subsequence P s
  (stream_filter_positions s Hinf 0)
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
filtering_subsequence P s
  (stream_filter_positions s Hinf 0)
  split.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
∀ i : nat,
  i < hd (stream_filter_positions s Hinf 0)
  → ¬ P (Str_nth i s)
A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
ForAll2
  (λ m n : nat,
     P (Str_nth m s)
     ∧ m < n
       ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s)))
  (stream_filter_positions s Hinf 0)
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
∀ i : nat,
  i < hd (stream_filter_positions s Hinf 0)
  → ¬ P (Str_nth i s) specialize (stream_filter_fst_pos_characterization s (fHere (Exists1 P) s Hinf) 0)
      as [k [Heq [Hpk Hnp]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) 0 =
(0 + k, Str_nth_tl (S k) s)
Hpk: P (Str_nth k s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i s)
∀ i : nat,
  i < hd (stream_filter_positions s Hinf 0)
  → ¬ P (Str_nth i s)
    simpl in Heq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
k: nat
Heq: stream_filter_fst_pos s
  (fHere (Exists1 P) s Hinf) 0 =
(k, Str_nth_tl k (tl s))
Hpk: P (Str_nth k s)
Hnp: ∀ i : nat, i < k → ¬ P (Str_nth i s)
∀ i : nat,
  i < hd (stream_filter_positions s Hinf 0)
  → ¬ P (Str_nth i s)
    by rewrite stream_filter_positions_unroll; cbn; rewrite Heq.
  -A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
ForAll2
  (λ m n : nat,
     P (Str_nth m s)
     ∧ m < n
       ∧ (∀ i : nat, m < i < n → ¬ P (Str_nth i s)))
  (stream_filter_positions s Hinf 0) apply ForAll2_forall.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
∀ n : nat,
  P
    (Str_nth
       (Str_nth n (stream_filter_positions s Hinf 0))
       s)
  ∧ Str_nth n (stream_filter_positions s Hinf 0) <
    Str_nth (S n) (stream_filter_positions s Hinf 0)
    ∧ (∀ i : nat,
         Str_nth n (stream_filter_positions s Hinf 0) <
         i <
         Str_nth (S n)
           (stream_filter_positions s Hinf 0)
         → ¬ P (Str_nth i s))
    intro n.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
P
  (Str_nth
     (Str_nth n (stream_filter_positions s Hinf 0)) s)
∧ Str_nth n (stream_filter_positions s Hinf 0) <
  Str_nth (S n) (stream_filter_positions s Hinf 0)
  ∧ (∀ i : nat,
       Str_nth n (stream_filter_positions s Hinf 0) <
       i <
       Str_nth (S n)
         (stream_filter_positions s Hinf 0)
       → ¬ P (Str_nth i s))
    specialize (stream_filter_positions_Str_nth_tl s Hinf 0 n) as Hnth_tl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
Hnth_tl: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl (S kn) s)),
  Str_nth_tl n
    (stream_filter_positions s Hinf 0) =
  Cons (0 + kn)
    (stream_filter_positions
       (Str_nth_tl (S kn) s) Hinf'
       (S (0 + kn))) ∧ P (Str_nth kn s)
P
  (Str_nth
     (Str_nth n (stream_filter_positions s Hinf 0)) s)
∧ Str_nth n (stream_filter_positions s Hinf 0) <
  Str_nth (S n) (stream_filter_positions s Hinf 0)
  ∧ (∀ i : nat,
       Str_nth n (stream_filter_positions s Hinf 0) <
       i <
       Str_nth (S n)
         (stream_filter_positions s Hinf 0)
       → ¬ P (Str_nth i s))
    simpl in Hnth_tl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
Hnth_tl: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn
                        (tl s))),
  Str_nth_tl n
    (stream_filter_positions s Hinf 0) =
  Cons kn
    (stream_filter_positions
       (Str_nth_tl kn (tl s)) Hinf' 
       (S kn)) ∧ P (Str_nth kn s)
P
  (Str_nth
     (Str_nth n (stream_filter_positions s Hinf 0)) s)
∧ Str_nth n (stream_filter_positions s Hinf 0) <
  Str_nth (S n) (stream_filter_positions s Hinf 0)
  ∧ (∀ i : nat,
       Str_nth n (stream_filter_positions s Hinf 0) <
       i <
       Str_nth (S n)
         (stream_filter_positions s Hinf 0)
       → ¬ P (Str_nth i s))
    remember (stream_filter_positions s Hinf 0).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
Hnth_tl: ∃ (kn : nat) (Hinf' : InfinitelyOften P
                        (Str_nth_tl kn
                        (tl s))),
  Str_nth_tl n s0 =
  Cons kn
    (stream_filter_positions
       (Str_nth_tl kn (tl s)) Hinf' 
       (S kn)) ∧ P (Str_nth kn s)
P (Str_nth (Str_nth n s0) s)
∧ Str_nth n s0 < Str_nth (S n) s0
  ∧ (∀ i : nat,
       Str_nth n s0 < i < Str_nth (S n) s0
       → ¬ P (Str_nth i s))
    destruct Hnth_tl as [kn [Hnth_inf [Hnth Hnth_p]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (stream_filter_positions
     (Str_nth_tl kn (tl s)) Hnth_inf 
     (S kn))
Hnth_p: P (Str_nth kn s)
P (Str_nth (Str_nth n s0) s)
∧ Str_nth n s0 < Str_nth (S n) s0
  ∧ (∀ i : nat,
       Str_nth n s0 < i < Str_nth (S n) s0
       → ¬ P (Str_nth i s))
    unfold Str_nth.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (stream_filter_positions
     (Str_nth_tl kn (tl s)) Hnth_inf 
     (S kn))
Hnth_p: P (Str_nth kn s)
P (hd (Str_nth_tl (hd (Str_nth_tl n s0)) s))
∧ hd (Str_nth_tl n s0) < hd (Str_nth_tl (S n) s0)
  ∧ (∀ i : nat,
       hd (Str_nth_tl n s0) < i <
       hd (Str_nth_tl (S n) s0)
       → ¬ P (hd (Str_nth_tl i s))) simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (stream_filter_positions
     (Str_nth_tl kn (tl s)) Hnth_inf 
     (S kn))
Hnth_p: P (Str_nth kn s)
P (hd (Str_nth_tl (hd (Str_nth_tl n s0)) s))
∧ hd (Str_nth_tl n s0) < hd (Str_nth_tl n (tl s0))
  ∧ (∀ i : nat,
       hd (Str_nth_tl n s0) < i <
       hd (Str_nth_tl n (tl s0))
       → ¬ P (hd (Str_nth_tl i s))) rewrite <- tl_nth_tl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (stream_filter_positions
     (Str_nth_tl kn (tl s)) Hnth_inf 
     (S kn))
Hnth_p: P (Str_nth kn s)
P (hd (Str_nth_tl (hd (Str_nth_tl n s0)) s))
∧ hd (Str_nth_tl n s0) < hd (tl (Str_nth_tl n s0))
  ∧ (∀ i : nat,
       hd (Str_nth_tl n s0) < i <
       hd (tl (Str_nth_tl n s0))
       → ¬ P (hd (Str_nth_tl i s)))
    rewrite stream_filter_positions_unroll in Hnth.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
P (hd (Str_nth_tl (hd (Str_nth_tl n s0)) s))
∧ hd (Str_nth_tl n s0) < hd (tl (Str_nth_tl n s0))
  ∧ (∀ i : nat,
       hd (Str_nth_tl n s0) < i <
       hd (tl (Str_nth_tl n s0))
       → ¬ P (hd (Str_nth_tl i s)))
    specialize (stream_filter_fst_pos_characterization
      (Str_nth_tl kn (tl s)) (fHere _ _ Hnth_inf) (S kn))
      as [k [Heq [Hpk Hnp]]].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
P (hd (Str_nth_tl (hd (Str_nth_tl n s0)) s))
∧ hd (Str_nth_tl n s0) < hd (tl (Str_nth_tl n s0))
  ∧ (∀ i : nat,
       hd (Str_nth_tl n s0) < i <
       hd (tl (Str_nth_tl n s0))
       → ¬ P (hd (Str_nth_tl i s)))
    rewrite Hnth; simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
P (hd (Str_nth_tl kn s))
∧ kn <
  (stream_filter_fst_pos (Str_nth_tl kn (tl s))
     (fHere (Exists1 P) (Str_nth_tl kn (tl s))
        Hnth_inf) (S kn)).1
  ∧ (∀ i : nat,
       kn < i <
       (stream_filter_fst_pos (Str_nth_tl kn (tl s))
          (fHere (Exists1 P) (Str_nth_tl kn (tl s))
             Hnth_inf) (S kn)).1
       → ¬ P (hd (Str_nth_tl i s)))
    split; [done |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
kn <
(stream_filter_fst_pos (Str_nth_tl kn (tl s))
   (fHere (Exists1 P) (Str_nth_tl kn (tl s)) Hnth_inf)
   (S kn)).1
∧ (∀ i : nat,
     kn < i <
     (stream_filter_fst_pos (Str_nth_tl kn (tl s))
        (fHere (Exists1 P) (Str_nth_tl kn (tl s))
           Hnth_inf) (S kn)).1
     → ¬ P (hd (Str_nth_tl i s)))
    rewrite Heq.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
kn <
(S kn + k, Str_nth_tl (S k) (Str_nth_tl kn (tl s))).1
∧ (∀ i : nat,
     kn < i <
     (S kn + k,
      Str_nth_tl (S k) (Str_nth_tl kn (tl s))).1
     → ¬ P (hd (Str_nth_tl i s))) simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
kn < S (kn + k)
∧ (∀ i : nat,
     kn < i < S (kn + k) → ¬ P (hd (Str_nth_tl i s)))
    split; [lia |].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
∀ i : nat,
  kn < i < S (kn + k) → ¬ P (hd (Str_nth_tl i s))
    intros i [Hle Hlt].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
i: nat
Hle: kn < i
Hlt: i < S (kn + k)
¬ P (hd (Str_nth_tl i s))
    apply stdpp_nat_le_sum in Hle as [k' ->].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
k': nat
Hlt: S kn + k' < S (kn + k)
¬ P (hd (Str_nth_tl (S kn + k') s))
    rewrite Nat.add_comm, <- Str_nth_tl_plus.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
k': nat
Hlt: S kn + k' < S (kn + k)
¬ P (hd (Str_nth_tl k' (Str_nth_tl (S kn) s))) simpl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
Hinf: InfinitelyOften P s
n: nat
s0: Stream nat
Heqs0: s0 = stream_filter_positions s Hinf 0
kn: nat
Hnth_inf: InfinitelyOften P (Str_nth_tl kn (tl s))
Hnth: Str_nth_tl n s0 =
Cons kn
  (Cons
     (stream_filter_fst_pos
        (Str_nth_tl kn (tl s))
        (fHere (Exists1 P)
           (Str_nth_tl kn (tl s)) Hnth_inf)
        (S kn)).1
     (stream_filter_positions
        (stream_filter_fst_pos
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn)).2
        (stream_filter_fst_pos_infinitely_often
           (Str_nth_tl kn (tl s))
           (fHere (Exists1 P)
              (Str_nth_tl kn (tl s)) Hnth_inf)
           (S kn) Hnth_inf)
        (S
           (stream_filter_fst_pos
              (Str_nth_tl kn (tl s))
              (fHere (Exists1 P)
                 (Str_nth_tl kn (tl s))
                 Hnth_inf) 
              (S kn)).1)))
Hnth_p: P (Str_nth kn s)
k: nat
Heq: stream_filter_fst_pos (Str_nth_tl kn (tl s))
  (fHere (Exists1 P) (Str_nth_tl kn (tl s))
     Hnth_inf) (S kn) =
(S kn + k,
 Str_nth_tl (S k) (Str_nth_tl kn (tl s)))
Hpk: P (Str_nth k (Str_nth_tl kn (tl s)))
Hnp: ∀ i : nat,
  i < k → ¬ P (Str_nth i (Str_nth_tl kn (tl s)))
k': nat
Hlt: S kn + k' < S (kn + k)
¬ P (hd (Str_nth_tl k' (Str_nth_tl kn (tl s))))
    by apply Hnp; lia.
Qed.

A restatement of filtering_subsequence_stream_filter_map based on the InfinitelyOften predicate, using the stream_filter_positions_filtering_subsequence.

Definition stream_filter_map
  [B : Type]
  (f : dsig P -> B)
  (s : Stream A)
  (Hinf : InfinitelyOften P s)
  : Stream B :=
  filtering_subsequence_stream_filter_map P f _ _
    (stream_filter_positions_filtering_subsequence s Hinf).

Stream filtering is obtained as a specialization of stream_filter_map.

Definition stream_filter
  (s : Stream A)
  (Hinf : InfinitelyOften P s)
  : Stream A :=
  stream_filter_map proj1_sig s Hinf.

End sec_stream_filter_positions.

Section sec_stream_map_option.

Mapping a partial function on a stream

Given a partial function f which is InfinitelyOften defined on the elements of a stream s, we can define the stream of the defined mapped values of s through f as a particular stream_filter_map.

Context
  [A B : Type]
  (f : A -> option B)
  (P : A -> Prop := is_Some ∘ f)
  (s : Stream A)
  .

Definition stream_map_option
  (Hinf : InfinitelyOften P s)
  : Stream B :=
  stream_filter_map P (fun k : dsig P => is_Some_proj (proj2_dsig k)) s Hinf.

Lemma stream_map_option_prefix
  (Hinf : InfinitelyOften P s)
  (n : nat)
  (map_opt_pre := omap f (stream_prefix s n))
  (m := length map_opt_pre)
  : stream_prefix (stream_map_option Hinf) m = map_opt_pre.A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
Hinf: InfinitelyOften P s
n: nat
map_opt_pre:= omap f (stream_prefix s n): list B
m:= length map_opt_pre: nat
stream_prefix (stream_map_option Hinf) m = map_opt_pre
Proof.A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
Hinf: InfinitelyOften P s
n: nat
map_opt_pre:= omap f (stream_prefix s n): list B
m:= length map_opt_pre: nat
stream_prefix (stream_map_option Hinf) m = map_opt_pre
  subst map_opt_pre m.A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
Hinf: InfinitelyOften P s
n: nat
stream_prefix (stream_map_option Hinf)
  (length (omap f (stream_prefix s n))) =
omap f (stream_prefix s n)
  rewrite !(omap_as_filter f (stream_prefix s n)).A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
Hinf: InfinitelyOften P s
n: nat
stream_prefix (stream_map_option Hinf)
  (length
     (list_filter_map (is_Some ∘ f)
        (λ x : dsig (is_Some ∘ f),
           is_Some_proj (proj2_dsig x))
        (stream_prefix s n))) =
list_filter_map (is_Some ∘ f)
  (λ x : dsig (is_Some ∘ f),
     is_Some_proj (proj2_dsig x)) (stream_prefix s n)
  by apply fitering_subsequence_stream_filter_map_prefix.
Qed.

Program Definition stream_map_option_prefix_ex
  (Hinf : InfinitelyOften P s)
  (Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf)
  (k : nat)
  : { n | stream_prefix (stream_map_option Hinf) k = omap f (stream_prefix s n)} :=
  let (n, Heq) := (fitering_subsequence_stream_filter_map_prefix_ex P
                    (fun k => is_Some_proj (proj2_dsig k)) _ _ Hfs k)
  in exist _ n _.
Next Obligation.A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
∀ (Hinf : InfinitelyOften P s) (Hfs :
                                filtering_subsequence
                                  P s
                                  (stream_filter_positions
                                     P s Hinf 0) :=
                                stream_filter_positions_filtering_subsequence
                                  P s Hinf) (k
                                             n : nat),
  stream_prefix
    (filtering_subsequence_stream_filter_map P
       (λ k0 : dsig P, is_Some_proj (proj2_dsig k0)) s
       (stream_filter_positions P s Hinf 0) Hfs) k =
  list_filter_map P
    (λ k0 : dsig P, is_Some_proj (proj2_dsig k0))
    (stream_prefix s n)
  → (λ n0 : nat,
       stream_prefix (stream_map_option Hinf) k =
       omap f (stream_prefix s n0)) n
Proof.A, B: Type
f: A → option B
P:= is_Some ∘ f: A → Prop
s: Stream A
∀ (Hinf : InfinitelyOften P s) (Hfs :
                                filtering_subsequence
                                  P s
                                  (stream_filter_positions
                                     P s Hinf 0) :=
                                stream_filter_positions_filtering_subsequence
                                  P s Hinf) (k
                                             n : nat),
  stream_prefix
    (filtering_subsequence_stream_filter_map P
       (λ k0 : dsig P, is_Some_proj (proj2_dsig k0)) s
       (stream_filter_positions P s Hinf 0) Hfs) k =
  list_filter_map P
    (λ k0 : dsig P, is_Some_proj (proj2_dsig k0))
    (stream_prefix s n)
  → (λ n0 : nat,
       stream_prefix (stream_map_option Hinf) k =
       omap f (stream_prefix s n0)) n
  by intros; cbn; rewrite !omap_as_filter.
Qed.

Definition bounded_stream_map_option
  (Hfin : FinitelyManyBound P s)
  : list B :=
  omap f (stream_prefix s (` Hfin)).

End sec_stream_map_option.

Section sec_stream_concat_map.

Mapping a function expanding elements to lists of elements on a stream

Given a function f which InfinitelyOften produces non-empty lists from the elements of a stream s, we can define the stream obtained by concatenating the values of s through f.

Context
  [A B : Type]
  (f : A -> list B)
  (FNonEmpty : A -> Prop := fun a => f a <> [])
  (s : Stream A)
  .

Definition stream_concat_map
  (Hinf : InfinitelyOften FNonEmpty s)
  : Stream B :=
  stream_concat (stream_filter_map FNonEmpty (list_function_restriction f) s Hinf).

Lemma stream_concat_map_prefix
  (Hinf : InfinitelyOften FNonEmpty s)
  (n : nat)
  (mbind_prefix := mbind f (stream_prefix s n))
  (m := length mbind_prefix)
  : stream_prefix (stream_concat_map Hinf) m = mbind_prefix.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mbind_prefix:= stream_prefix s n ≫= f: list B
m:= length mbind_prefix: nat
stream_prefix (stream_concat_map Hinf) m =
mbind_prefix
Proof.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mbind_prefix:= stream_prefix s n ≫= f: list B
m:= length mbind_prefix: nat
stream_prefix (stream_concat_map Hinf) m =
mbind_prefix
  subst mbind_prefix m; unfold stream_concat_map.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
stream_prefix
  (stream_concat
     (stream_filter_map FNonEmpty
        (list_function_restriction f) s Hinf))
  (length (stream_prefix s n ≫= f)) =
stream_prefix s n ≫= f
  cut (mjoin
    (List.map ne_list_to_list
      (list_filter_map (fun a : A => f a <> []) (list_function_restriction f)
          (stream_prefix s n))) = mbind f (stream_prefix s n)).A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mjoin
  (List.map ne_list_to_list
     (list_filter_map (λ a : A, f a ≠ [])
        (list_function_restriction f)
        (stream_prefix s n))) = stream_prefix s n ≫= f
→ stream_prefix
    (stream_concat
       (stream_filter_map FNonEmpty
          (list_function_restriction f) s Hinf))
    (length (stream_prefix s n ≫= f)) =
  stream_prefix s n ≫= f
A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mjoin
  (List.map ne_list_to_list
     (list_filter_map (λ a : A, f a ≠ [])
        (list_function_restriction f)
        (stream_prefix s n))) = 
stream_prefix s n ≫= f
  {A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mjoin
  (List.map ne_list_to_list
     (list_filter_map (λ a : A, f a ≠ [])
        (list_function_restriction f)
        (stream_prefix s n))) = stream_prefix s n ≫= f
→ stream_prefix
    (stream_concat
       (stream_filter_map FNonEmpty
          (list_function_restriction f) s Hinf))
    (length (stream_prefix s n ≫= f)) =
  stream_prefix s n ≫= f
    intros <-.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
stream_prefix
  (stream_concat
     (stream_filter_map FNonEmpty
        (list_function_restriction f) s Hinf))
  (length
     (mjoin
        (List.map ne_list_to_list
           (list_filter_map (λ a : A, f a ≠ [])
              (list_function_restriction f)
              (stream_prefix s n))))) =
mjoin
  (List.map ne_list_to_list
     (list_filter_map (λ a : A, f a ≠ [])
        (list_function_restriction f)
        (stream_prefix s n)))
    by erewrite stream_concat_prefix;
      unfold stream_filter_map;
      rewrite fitering_subsequence_stream_filter_map_prefix.
  }A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
n: nat
mjoin
  (List.map ne_list_to_list
     (list_filter_map (λ a : A, f a ≠ [])
        (list_function_restriction f)
        (stream_prefix s n))) = stream_prefix s n ≫= f
  by apply list_filter_map_mbind.
Qed.

Program Definition stream_concat_map_ex_prefix
  (Hinf : InfinitelyOften FNonEmpty s)
  (Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf)
  (k : nat)
  : {n : nat |
      stream_prefix (stream_concat_map Hinf) k
        `prefix_of`
      mbind f (stream_prefix s n)}
  :=
  let (n, Heq) :=
    (fitering_subsequence_stream_filter_map_prefix_ex
      FNonEmpty (list_function_restriction f) _ _ Hfs k)
  in exist _ n _.
Next Obligation.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
∀ (Hinf : InfinitelyOften FNonEmpty s) (Hfs :
                                        filtering_subsequence
                                          FNonEmpty s
                                          (stream_filter_positions
                                             FNonEmpty
                                             s Hinf 0) :=
                                        stream_filter_positions_filtering_subsequence
                                          FNonEmpty s
                                          Hinf) (k
                                                 n : nat),
  stream_prefix
    (filtering_subsequence_stream_filter_map FNonEmpty
       (list_function_restriction f) s
       (stream_filter_positions FNonEmpty s Hinf 0)
       Hfs) k =
  list_filter_map FNonEmpty
    (list_function_restriction f) (stream_prefix s n)
  → (λ n0 : nat,
       stream_prefix (stream_concat_map Hinf) k
       `prefix_of` stream_prefix s n0 ≫= f) n
Proof.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
∀ (Hinf : InfinitelyOften FNonEmpty s) (Hfs :
                                        filtering_subsequence
                                          FNonEmpty s
                                          (stream_filter_positions
                                             FNonEmpty
                                             s Hinf 0) :=
                                        stream_filter_positions_filtering_subsequence
                                          FNonEmpty s
                                          Hinf) (k
                                                 n : nat),
  stream_prefix
    (filtering_subsequence_stream_filter_map FNonEmpty
       (list_function_restriction f) s
       (stream_filter_positions FNonEmpty s Hinf 0)
       Hfs) k =
  list_filter_map FNonEmpty
    (list_function_restriction f) (stream_prefix s n)
  → (λ n0 : nat,
       stream_prefix (stream_concat_map Hinf) k
       `prefix_of` stream_prefix s n0 ≫= f) n
  cbn; intros Hinf k n Heq.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
k, n: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map
     FNonEmpty (list_function_restriction f) s
     (stream_filter_positions FNonEmpty s Hinf 0)
     (stream_filter_positions_filtering_subsequence
        FNonEmpty s Hinf)) k =
list_filter_map FNonEmpty
  (list_function_restriction f)
  (stream_prefix s n)
stream_prefix (stream_concat_map Hinf) k
`prefix_of` stream_prefix s n ≫= f
  rewrite <- (stream_concat_map_prefix Hinf).A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
k, n: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map
     FNonEmpty (list_function_restriction f) s
     (stream_filter_positions FNonEmpty s Hinf 0)
     (stream_filter_positions_filtering_subsequence
        FNonEmpty s Hinf)) k =
list_filter_map FNonEmpty
  (list_function_restriction f)
  (stream_prefix s n)
stream_prefix (stream_concat_map Hinf) k
`prefix_of` stream_prefix (stream_concat_map Hinf)
              (length (stream_prefix s n ≫= f))
  apply stream_prefix_of.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
k, n: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map
     FNonEmpty (list_function_restriction f) s
     (stream_filter_positions FNonEmpty s Hinf 0)
     (stream_filter_positions_filtering_subsequence
        FNonEmpty s Hinf)) k =
list_filter_map FNonEmpty
  (list_function_restriction f)
  (stream_prefix s n)
k ≤ length (stream_prefix s n ≫= f)
  rewrite <- list_filter_map_mbind.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
k, n: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map
     FNonEmpty (list_function_restriction f) s
     (stream_filter_positions FNonEmpty s Hinf 0)
     (stream_filter_positions_filtering_subsequence
        FNonEmpty s Hinf)) k =
list_filter_map FNonEmpty
  (list_function_restriction f)
  (stream_prefix s n)
k
≤ length
    (mjoin
       (List.map ne_list_to_list
          (list_filter_map (λ a : A, f a ≠ [])
             (list_function_restriction f)
             (stream_prefix s n))))
  replace k
    with (length (list_filter_map FNonEmpty (list_function_restriction f) (stream_prefix s n)))
    by (rewrite <- Heq; apply stream_prefix_length).A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
Hinf: InfinitelyOften FNonEmpty s
k, n: nat
Heq: stream_prefix
  (filtering_subsequence_stream_filter_map
     FNonEmpty (list_function_restriction f) s
     (stream_filter_positions FNonEmpty s Hinf 0)
     (stream_filter_positions_filtering_subsequence
        FNonEmpty s Hinf)) k =
list_filter_map FNonEmpty
  (list_function_restriction f)
  (stream_prefix s n)
length
  (list_filter_map FNonEmpty
     (list_function_restriction f) (stream_prefix s n))
≤ length
    (mjoin
       (List.map ne_list_to_list
          (list_filter_map (λ a : A, f a ≠ [])
             (list_function_restriction f)
             (stream_prefix s n))))
  by apply ne_list_concat_min_length.
Qed.

Program Definition stream_concat_map_ex_min_prefix
  `{EqDecision B}
  (Hinf : InfinitelyOften FNonEmpty s)
  (k : nat)
  (Ppre := fun m =>
    stream_prefix (stream_concat_map Hinf) k
      `prefix_of`
    mbind f (stream_prefix s m))
  : {n : nat | minimal_among le Ppre n}
  :=
  let (n, Hpre) :=  stream_concat_map_ex_prefix Hinf k in
  exist _ (find_least_among Ppre n) _.
Next Obligation.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
∀ (EqDecision0 : EqDecision B) (Hinf : InfinitelyOften
                                         FNonEmpty s) 
  (k : nat) (Ppre :=
             λ m : nat,
               stream_prefix (stream_concat_map Hinf)
                 k `prefix_of` stream_prefix s m ≫= f) 
  (n : nat),
  stream_prefix (stream_concat_map Hinf) k
  `prefix_of` stream_prefix s n ≫= f
  → (λ n0 : nat, minimal_among le Ppre n0)
      (find_least_among Ppre n)
Proof.A, B: Type
f: A → list B
FNonEmpty:= λ a : A, f a ≠ []: A → Prop
s: Stream A
∀ (EqDecision0 : EqDecision B) (Hinf : InfinitelyOften
                                         FNonEmpty s) 
  (k : nat) (Ppre :=
             λ m : nat,
               stream_prefix (stream_concat_map Hinf)
                 k `prefix_of` stream_prefix s m ≫= f) 
  (n : nat),
  stream_prefix (stream_concat_map Hinf) k
  `prefix_of` stream_prefix s n ≫= f
  → (λ n0 : nat, minimal_among le Ppre n0)
      (find_least_among Ppre n)
  by intros; apply find_least_among_is_minimal.
Qed.

Definition bounded_stream_concat_map
  (Hfin : FinitelyManyBound FNonEmpty s)
  : list B :=
  mbind f (stream_prefix s (` Hfin)).

End sec_stream_concat_map.

For a totally defined function, stream_map_option corresponds to the regular map on streams.

Lemma stream_map_option_EqSt [A B : Type] (f : A -> B)
  : forall s (Hinf : InfinitelyOften (is_Some ∘ (Some ∘ f)) s),
  EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf).A, B: Type
f: A → B
∀ (s : Stream A) (Hinf : InfinitelyOften
                           (is_Some ∘ (Some ∘ f)) s),
  EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf)
Proof.A, B: Type
f: A → B
∀ (s : Stream A) (Hinf : InfinitelyOften
                           (is_Some ∘ (Some ∘ f)) s),
  EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf)
  intros.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf) apply EqSt_stream_prefix.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
∀ n : nat,
  stream_prefix (map f s) n =
  stream_prefix (stream_map_option (Some ∘ f) s Hinf)
    n intro n.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
stream_prefix (map f s) n =
stream_prefix (stream_map_option (Some ∘ f) s Hinf) n
  destruct n; [done |].A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
stream_prefix (map f s) (S n) =
stream_prefix (stream_map_option (Some ∘ f) s Hinf)
  (S n)
  rewrite <- stream_prefix_map.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
List.map f (stream_prefix s (S n)) =
stream_prefix (stream_map_option (Some ∘ f) s Hinf)
  (S n)

  pose (stream_map_option_prefix_ex (Some ∘ f) s Hinf (S n)) as Hrew.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hrew:= stream_map_option_prefix_ex 
  (Some ∘ f) s Hinf (S n): {n0 : nat
| stream_prefix
    (stream_map_option (Some ∘ f) s Hinf) 
    (S n) =
  omap (Some ∘ f) (stream_prefix s n0)}
List.map f (stream_prefix s (S n)) =
stream_prefix (stream_map_option (Some ∘ f) s Hinf)
  (S n)
  rewrite (proj2_sig Hrew).A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hrew:= stream_map_option_prefix_ex 
  (Some ∘ f) s Hinf (S n): {n0 : nat
| stream_prefix
    (stream_map_option (Some ∘ f) s Hinf) 
    (S n) =
  omap (Some ∘ f) (stream_prefix s n0)}
List.map f (stream_prefix s (S n)) =
omap (Some ∘ f) (stream_prefix s (`Hrew))
  replace (` Hrew) with (S n); [done |].A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hrew:= stream_map_option_prefix_ex 
  (Some ∘ f) s Hinf (S n): {n0 : nat
| stream_prefix
    (stream_map_option (Some ∘ f) s Hinf) 
    (S n) =
  omap (Some ∘ f) (stream_prefix s n0)}
S n = `Hrew
  simpl.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hrew:= stream_map_option_prefix_ex 
  (Some ∘ f) s Hinf (S n): {n0 : nat
| stream_prefix
    (stream_map_option (Some ∘ f) s Hinf) 
    (S n) =
  omap (Some ∘ f) (stream_prefix s n0)}
S n =
S
  (Str_nth n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f)) s Hinf 0)) f_equal.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hrew:= stream_map_option_prefix_ex 
  (Some ∘ f) s Hinf (S n): {n0 : nat
| stream_prefix
    (stream_map_option (Some ∘ f) s Hinf) 
    (S n) =
  omap (Some ∘ f) (stream_prefix s n0)}
n =
Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) clear.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
n =
Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0)
  cut
    (forall k, Streams.Str_nth n
      (stream_filter_positions (is_Some ∘ (Some ∘ f)) s Hinf k) = k + n).A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
(∀ k : nat,
   Str_nth n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f)) s Hinf k) = 
   k + n)
→ n =
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf 0)
A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
∀ k : nat,
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
  {A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
(∀ k : nat,
   Str_nth n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f)) s Hinf k) = 
   k + n)
→ n =
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf 0) intros Hk.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hk: ∀ k : nat,
  Str_nth n
    (stream_filter_positions
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
n =
Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) specialize (Hk 0).A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hk: Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) = 
0 + n
n =
Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) simpl in Hk.A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
Hk: Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) = n
n =
Str_nth n
  (stream_filter_positions 
     (is_Some ∘ (Some ∘ f)) s Hinf 0) congruence.  }A, B: Type
f: A → B
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
n: nat
∀ k : nat,
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
  revert s Hinf.A, B: Type
f: A → B
n: nat
∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
  assert (Hfirst : forall s Hinf k,
    (stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s (fHere _ _ Hinf) k).1 = k).A, B: Type
f: A → B
n: nat
∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1 (is_Some ∘ (Some ∘ f))) s) 
  (k : nat),
  (stream_filter_fst_pos 
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s Hinf) k).1 =
  k
A, B: Type
f: A → B
n: nat
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
  {A, B: Type
f: A → B
n: nat
∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1 (is_Some ∘ (Some ∘ f))) s) 
  (k : nat),
  (stream_filter_fst_pos 
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s Hinf) k).1 =
  k
    intros.A, B: Type
f: A → B
n: nat
s: Stream A
Hinf: ForAll (Exists1 (is_Some ∘ (Some ∘ f))) s
k: nat
(stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s
   (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s Hinf) k).1 =
k
    edestruct stream_filter_fst_pos_characterization as (_k & -> & _ & H_k); cbn.A, B: Type
f: A → B
n: nat
s: Stream A
Hinf: ForAll (Exists1 (is_Some ∘ (Some ∘ f))) s
k, _k: nat
H_k: ∀ i : nat,
  i < _k
  → ¬ (is_Some ∘ (Some ∘ f)) (Str_nth i s)
k + _k = k
    destruct _k; [lia |].A, B: Type
f: A → B
n: nat
s: Stream A
Hinf: ForAll (Exists1 (is_Some ∘ (Some ∘ f))) s
k, _k: nat
H_k: ∀ i : nat,
  i < S _k
  → ¬ (is_Some ∘ (Some ∘ f)) (Str_nth i s)
k + S _k = k
    by exfalso; apply (H_k 0); [lia | eexists].
  }A, B: Type
f: A → B
n: nat
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  Str_nth n
    (stream_filter_positions 
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
  induction n; intros; rewrite stream_filter_positions_unroll; unfold Streams.Str_nth; simpl.A, B: Type
f: A → B
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
k: nat
(stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s
   (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s Hinf) k).1 =
k + 0
A, B: Type
f: A → B
n: nat
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
IHn: ∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  Str_nth n
    (stream_filter_positions
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
k: nat
hd
  (Str_nth_tl n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f))
        (stream_filter_fst_pos 
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k).2
        (stream_filter_fst_pos_infinitely_often
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k Hinf)
        (S
           (stream_filter_fst_pos
              (is_Some ∘ (Some ∘ f)) s
              (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
                 s Hinf) k).1))) = 
k + S n
  -A, B: Type
f: A → B
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
k: nat
(stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s
   (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s Hinf) k).1 =
k + 0 by rewrite Hfirst; lia.
  -A, B: Type
f: A → B
n: nat
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
IHn: ∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  Str_nth n
    (stream_filter_positions
       (is_Some ∘ (Some ∘ f)) s Hinf k) = 
  k + n
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
k: nat
hd
  (Str_nth_tl n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f))
        (stream_filter_fst_pos 
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k).2
        (stream_filter_fst_pos_infinitely_often
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k Hinf)
        (S
           (stream_filter_fst_pos
              (is_Some ∘ (Some ∘ f)) s
              (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
                 s Hinf) k).1))) = 
k + S n unfold Streams.Str_nth in IHn.A, B: Type
f: A → B
n: nat
Hfirst: ∀ (s : Stream A) (Hinf : 
                  ForAll
                    (Exists1
                       (is_Some ∘ (Some ∘ f)))
                    s) (k : nat),
  (stream_filter_fst_pos
     (is_Some ∘ (Some ∘ f)) s
     (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
        s Hinf) k).1 = k
IHn: ∀ (s : Stream A) (Hinf : 
                  InfinitelyOften
                    (is_Some ∘ (Some ∘ f)) s) 
  (k : nat),
  hd
    (Str_nth_tl n
       (stream_filter_positions
          (is_Some ∘ (Some ∘ f)) s Hinf k)) =
  k + n
s: Stream A
Hinf: InfinitelyOften (is_Some ∘ (Some ∘ f)) s
k: nat
hd
  (Str_nth_tl n
     (stream_filter_positions 
        (is_Some ∘ (Some ∘ f))
        (stream_filter_fst_pos 
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k).2
        (stream_filter_fst_pos_infinitely_often
           (is_Some ∘ (Some ∘ f)) s
           (fHere (Exists1 (is_Some ∘ (Some ∘ f))) s
              Hinf) k Hinf)
        (S
           (stream_filter_fst_pos
              (is_Some ∘ (Some ∘ f)) s
              (fHere (Exists1 (is_Some ∘ (Some ∘ f)))
                 s Hinf) k).1))) = 
k + S n
    by rewrite IHn, Hfirst; lia.
Qed.