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 Classical Sorted.
From VLSM.Lib Require Import Preamble ListExtras StdppExtras SortedLists NeList.[Loading ML file coq-itauto.plugin ... done]

Utility: Stream Definitions and Results

Lemma stream_eq_hd_tl {A} (s s' : Stream A) :
  hd s = hd s' -> tl s = tl s' -> s = s'.A: Type
s, s': Stream A
hd s = hd s' → tl s = tl s' → s = s'
Proof.A: Type
s, s': Stream A
hd s = hd s' → tl s = tl s' → s = s' by destruct s, s'; cbn; intros -> ->. Qed.

Lemma fHere [A : Type] (P : Stream A -> Prop) : forall s, ForAll P s -> P s.A: Type
P: Stream A → Prop
∀ s : Stream A, ForAll P s → P s
Proof.A: Type
P: Stream A → Prop
∀ s : Stream A, ForAll P s → P s by intros s []. Qed.

Lemma fFurther [A : Type] (P : Stream A -> Prop) : forall s, ForAll P s -> ForAll P (tl s).A: Type
P: Stream A → Prop
∀ s : Stream A, ForAll P s → ForAll P (tl s)
Proof.A: Type
P: Stream A → Prop
∀ s : Stream A, ForAll P s → ForAll P (tl s) by intros s []. Qed.

Lemma ForAll_subsumption [A : Type] (P Q : Stream A -> Prop)
  (HPQ : forall s, P s -> Q s)
  : forall s, ForAll P s -> ForAll Q s.A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ s : Stream A, ForAll P s → ForAll Q s
Proof.A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ s : Stream A, ForAll P s → ForAll Q s
  apply ForAll_coind.A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ x : Stream A, ForAll P x → Q x
A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ x : Stream A, ForAll P x → ForAll P (tl x)
  -A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ x : Stream A, ForAll P x → Q x by intros s Hp; apply fHere in Hp; apply HPQ.
  -A: Type
P, Q: Stream A → Prop
HPQ: ∀ s : Stream A, P s → Q s
∀ x : Stream A, ForAll P x → ForAll P (tl x) by apply fFurther.
Qed.

Lemma Exists_map_conv :
  forall [A B : Type] (f : A -> B) (P : Stream B -> Prop) (s : Stream A),
    Exists P (Streams.map f s) -> Exists (fun s => P (Streams.map f s)) s.∀ (A B : Type) (f : A → B) (P : Stream B → Prop) (s : 
                                                 Stream
                                                 A),
  Exists P (map f s)
  → Exists (λ s0 : Stream A, P (map f s0)) s
Proof.∀ (A B : Type) (f : A → B) (P : Stream B → Prop) (s : 
                                                 Stream
                                                 A),
  Exists P (map f s)
  → Exists (λ s0 : Stream A, P (map f s0)) s
  intros A B f P s HEx.A, B: Type
f: A → B
P: Stream B → Prop
s: Stream A
HEx: Exists P (map f s)
Exists (λ s : Stream A, P (map f s)) s
  remember (map f s) as fs; revert s Heqfs.A, B: Type
f: A → B
P: Stream B → Prop
fs: Stream B
HEx: Exists P fs
∀ s : Stream A,
  fs = map f s
  → Exists (λ s0 : Stream A, P (map f s0)) s
  induction HEx; [by intros s ->; constructor |].A, B: Type
f: A → B
P: Stream B → Prop
x: Stream B
HEx: Exists P (tl x)
IHHEx: ∀ s : Stream A,
  tl x = map f s
  → Exists (λ s0 : Stream A, P (map f s0)) s
∀ s : Stream A,
  x = map f s
  → Exists (λ s0 : Stream A, P (map f s0)) s
  intros [a' s'] ->.A, B: Type
f: A → B
P: Stream B → Prop
a': A
s': Stream A
IHHEx: ∀ s : Stream A,
  tl (map f (Cons a' s')) = map f s
  → Exists (λ s0 : Stream A, P (map f s0)) s
HEx: Exists P (tl (map f (Cons a' s')))
Exists (λ s : Stream A, P (map f s)) (Cons a' s')
  constructor 2; cbn.A, B: Type
f: A → B
P: Stream B → Prop
a': A
s': Stream A
IHHEx: ∀ s : Stream A,
  tl (map f (Cons a' s')) = map f s
  → Exists (λ s0 : Stream A, P (map f s0)) s
HEx: Exists P (tl (map f (Cons a' s')))
Exists (λ s : Stream A, P (map f s)) s'
  by apply IHHEx.
Qed.

Lemma ForAll_tauto :
  forall [A : Type] (P : Stream A -> Prop),
    (forall s : Stream A, P s) -> forall s : Stream A, ForAll P s.∀ (A : Type) (P : Stream A → Prop),
  (∀ s : Stream A, P s) → ∀ s : Stream A, ForAll P s
Proof.∀ (A : Type) (P : Stream A → Prop),
  (∀ s : Stream A, P s) → ∀ s : Stream A, ForAll P s
  cofix CH.CH: ∀ (A : Type) (P : Stream A → Prop),
  (∀ s : Stream A, P s)
  → ∀ s : Stream A, ForAll P s
∀ (A : Type) (P : Stream A → Prop),
  (∀ s : Stream A, P s) → ∀ s : Stream A, ForAll P s
  by constructor; [| apply CH].
Qed.

Lemma forall_ForAll :
  forall [A B : Type] (P : A -> Stream B -> Prop) [s : Stream B],
    (forall (a : A), ForAll (P a) s) -> ForAll (fun s' => forall a, P a s') s.∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
Proof.∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
  cofix CH.CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
  intros A B P [b s] H.CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
ForAll (λ s' : Stream B, ∀ a : A, P a s') (Cons b s)
  constructor.CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
∀ a : A, P a (Cons b s)
CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
ForAll (λ s' : Stream B, ∀ a : A, P a s')
  (tl (Cons b s))
  -CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
∀ a : A, P a (Cons b s) by intro a; destruct (H a).
  -CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
ForAll (λ s' : Stream B, ∀ a : A, P a s')
  (tl (Cons b s)) apply CH.CH: ∀ (A B : Type) (P : A → Stream B → Prop) (s : Stream
                                                B),
  (∀ a : A, ForAll (P a) s)
  → ForAll (λ s' : Stream B, ∀ a : A, P a s') s
A, B: Type
P: A → Stream B → Prop
b: B
s: Stream B
H: ∀ a : A, ForAll (P a) (Cons b s)
∀ a : A, ForAll (P a) (tl (Cons b s))
    by intro a; destruct (H a).
Qed.

Lemma ForAll_impl :
  forall [A : Type] (P Q : Stream A -> Prop) (s : Stream A),
    ForAll (fun s => P s -> Q s) s -> ForAll P s -> ForAll Q s.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
Proof.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
  cofix CH.CH: ∀ (A : Type) (P Q : Stream A → Prop) (s : Stream
                                            A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
  intros A P Q [a s] []; inversion 1; subst.CH: ∀ (A : Type) (P Q : Stream A → Prop) (s : Stream
                                            A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
A: Type
P, Q: Stream A → Prop
a: A
s: Stream A
H: P (Cons a s) → Q (Cons a s)
H0: ForAll (λ s : Stream A, P s → Q s)
  (tl (Cons a s))
H1: ForAll P (Cons a s)
H2: P (Cons a s)
H3: ForAll P (tl (Cons a s))
ForAll Q (Cons a s)
  constructor; cbn; [by apply H |].CH: ∀ (A : Type) (P Q : Stream A → Prop) (s : Stream
                                            A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → ForAll P s → ForAll Q s
A: Type
P, Q: Stream A → Prop
a: A
s: Stream A
H: P (Cons a s) → Q (Cons a s)
H0: ForAll (λ s : Stream A, P s → Q s)
  (tl (Cons a s))
H1: ForAll P (Cons a s)
H2: P (Cons a s)
H3: ForAll P (tl (Cons a s))
ForAll Q s
  by apply (CH A P Q).
Qed.

Lemma Exists_impl :
  forall [A : Type] (P Q : Stream A -> Prop) (s : Stream A),
    ForAll (fun s => P s -> Q s) s -> Exists P s -> Exists Q s.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → Exists P s → Exists Q s
Proof.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  ForAll (λ s0 : Stream A, P s0 → Q s0) s
  → Exists P s → Exists Q s
  intros A P Q s Hall HEx.A: Type
P, Q: Stream A → Prop
s: Stream A
Hall: ForAll (λ s : Stream A, P s → Q s) s
HEx: Exists P s
Exists Q s
  induction HEx.A: Type
P, Q: Stream A → Prop
x: Stream A
Hall: ForAll (λ s : Stream A, P s → Q s) x
H: P x
Exists Q x
A: Type
P, Q: Stream A → Prop
x: Stream A
Hall: ForAll (λ s : Stream A, P s → Q s) x
HEx: Exists P (tl x)
IHHEx: ForAll (λ s : Stream A, P s → Q s) (tl x)
→ Exists Q (tl x)
Exists Q x
  -A: Type
P, Q: Stream A → Prop
x: Stream A
Hall: ForAll (λ s : Stream A, P s → Q s) x
H: P x
Exists Q x by apply Here, Hall.
  -A: Type
P, Q: Stream A → Prop
x: Stream A
Hall: ForAll (λ s : Stream A, P s → Q s) x
HEx: Exists P (tl x)
IHHEx: ForAll (λ s : Stream A, P s → Q s) (tl x)
→ Exists Q (tl x)
Exists Q x by apply Further, IHHEx; inversion Hall.
Qed.

Lemma not_Exists :
  forall [A : Type] (P : Stream A -> Prop) (s : Stream A),
    ~ Exists P s -> ForAll (fun s => ~ P s) s.∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s → ForAll (λ s0 : Stream A, ¬ P s0) s
Proof.∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s → ForAll (λ s0 : Stream A, ¬ P s0) s
  cofix CH.CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s → ForAll (λ s0 : Stream A, ¬ P s0) s
  intros A P [a s] H.CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
A: Type
P: Stream A → Prop
a: A
s: Stream A
H: ¬ Exists P (Cons a s)
ForAll (λ s : Stream A, ¬ P s) (Cons a s)
  constructor.CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
A: Type
P: Stream A → Prop
a: A
s: Stream A
H: ¬ Exists P (Cons a s)
¬ P (Cons a s)
CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
A: Type
P: Stream A → Prop
a: A
s: Stream A
H: ¬ Exists P (Cons a s)
ForAll (λ s : Stream A, ¬ P s) (tl (Cons a s))
  -CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
A: Type
P: Stream A → Prop
a: A
s: Stream A
H: ¬ Exists P (Cons a s)
¬ P (Cons a s) by contradict H; constructor.
  -CH: ∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ Exists P s
  → ForAll (λ s0 : Stream A, ¬ P s0) s
A: Type
P: Stream A → Prop
a: A
s: Stream A
H: ¬ Exists P (Cons a s)
ForAll (λ s : Stream A, ¬ P s) (tl (Cons a s)) by apply CH; contradict H; constructor.
Qed.

Lemma not_ForAll :
  forall [A : Type] (P : Stream A -> Prop) (s : Stream A),
    ~ ForAll P s -> Exists (fun s => ~ P s) s.∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ ForAll P s → Exists (λ s0 : Stream A, ¬ P s0) s
Proof.∀ (A : Type) (P : Stream A → Prop) (s : Stream A),
  ¬ ForAll P s → Exists (λ s0 : Stream A, ¬ P s0) s
  intros A P s H.A: Type
P: Stream A → Prop
s: Stream A
H: ¬ ForAll P s
Exists (λ s : Stream A, ¬ P s) s
  apply Classical_Prop.NNPP.A: Type
P: Stream A → Prop
s: Stream A
H: ¬ ForAll P s
¬ ¬ Exists (λ s : Stream A, ¬ P s) s
  contradict H.A: Type
P: Stream A → Prop
s: Stream A
H: ¬ Exists (λ s : Stream A, ¬ P s) s
ForAll P s
  apply not_Exists in H.A: Type
P: Stream A → Prop
s: Stream A
H: ForAll (λ s : Stream A, ¬ ¬ P s) s
ForAll P s
  revert H; apply ForAll_impl, ForAll_tauto.A: Type
P: Stream A → Prop
s: Stream A
∀ s : Stream A, ¬ ¬ P s → P s
  by intro; apply Classical_Prop.NNPP.
Qed.

Lemma not_Exists_ForAll :
  forall [A : Type] (s : Stream A),
    ~ (exists x : A, Exists (ForAll (λ s : Stream A, hd s = x)) s) ->
    forall x : A, ForAll (Exists (fun s => hd s <> x)) s.∀ (A : Type) (s : Stream A),
  ¬ (∃ x : A,
       Exists (ForAll (λ s0 : Stream A, hd s0 = x)) s)
  → ∀ x : A,
      ForAll (Exists (λ s0 : Stream A, hd s0 ≠ x)) s
Proof.∀ (A : Type) (s : Stream A),
  ¬ (∃ x : A,
       Exists (ForAll (λ s0 : Stream A, hd s0 = x)) s)
  → ∀ x : A,
      ForAll (Exists (λ s0 : Stream A, hd s0 ≠ x)) s
  intros A s Hnex x.A: Type
s: Stream A
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
x: A
ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
  assert (Hnex' : ~ Exists (ForAll (fun s : Stream A => hd s = x)) s) by firstorder.A: Type
s: Stream A
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
x: A
Hnex': ¬ Exists (ForAll (λ s : Stream A, hd s = x)) s
ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
  apply not_Exists in Hnex'.A: Type
s: Stream A
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
x: A
Hnex': ForAll
  (λ s : Stream A,
     ¬ ForAll (λ s0 : Stream A, hd s0 = x) s)
  s
ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
  revert Hnex'; apply ForAll_impl, ForAll_tauto.A: Type
s: Stream A
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
x: A
∀ s : Stream A,
  ¬ ForAll (λ s0 : Stream A, hd s0 = x) s
  → Exists (λ s0 : Stream A, hd s0 ≠ x) s
  clear; intros s Hnall.A: Type
x: A
s: Stream A
Hnall: ¬ ForAll (λ s : Stream A, hd s = x) s
Exists (λ s : Stream A, hd s ≠ x) s
  by apply not_ForAll in Hnall.
Qed.

Lemma use_Exists :
  forall [A : Type] (P Q : Stream A -> Prop) (s : Stream A),
    Exists P s -> ForAll Q s -> exists s', P s' /\ ForAll Q s'.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  Exists P s
  → ForAll Q s → ∃ s' : Stream A, P s' ∧ ForAll Q s'
Proof.∀ (A : Type) (P Q : Stream A → Prop) (s : Stream A),
  Exists P s
  → ForAll Q s → ∃ s' : Stream A, P s' ∧ ForAll Q s'
  induction 1.A: Type
P, Q: Stream A → Prop
x: Stream A
H: P x
ForAll Q x → ∃ s' : Stream A, P s' ∧ ForAll Q s'
A: Type
P, Q: Stream A → Prop
x: Stream A
H: Exists P (tl x)
IHExists: ForAll Q (tl x)
→ ∃ s' : Stream A, P s' ∧ ForAll Q s'
ForAll Q x → ∃ s' : Stream A, P s' ∧ ForAll Q s'
  -A: Type
P, Q: Stream A → Prop
x: Stream A
H: P x
ForAll Q x → ∃ s' : Stream A, P s' ∧ ForAll Q s' by exists x.
  -A: Type
P, Q: Stream A → Prop
x: Stream A
H: Exists P (tl x)
IHExists: ForAll Q (tl x)
→ ∃ s' : Stream A, P s' ∧ ForAll Q s'
ForAll Q x → ∃ s' : Stream A, P s' ∧ ForAll Q s' by inversion 1; subst; apply IHExists.
Qed.

Lemma Exists_Str_nth_tl [A : Type] (P : Stream A -> Prop)
  : forall s, Exists P s <-> exists n, P (Str_nth_tl n s).A: Type
P: Stream A → Prop
∀ s : Stream A,
  Exists P s ↔ (∃ n : nat, P (Str_nth_tl n s))
Proof.A: Type
P: Stream A → Prop
∀ s : Stream A,
  Exists P s ↔ (∃ n : nat, P (Str_nth_tl n s))
  intros s; split.A: Type
P: Stream A → Prop
s: Stream A
Exists P s → ∃ n : nat, P (Str_nth_tl n s)
A: Type
P: Stream A → Prop
s: Stream A
(∃ n : nat, P (Str_nth_tl n s)) → Exists P s
  -A: Type
P: Stream A → Prop
s: Stream A
Exists P s → ∃ n : nat, P (Str_nth_tl n s) induction 1; [by exists 0 |].A: Type
P: Stream A → Prop
x: Stream A
H: Exists P (tl x)
IHExists: ∃ n : nat, P (Str_nth_tl n (tl x))
∃ n : nat, P (Str_nth_tl n x)
    destruct IHExists as [n Hn].A: Type
P: Stream A → Prop
x: Stream A
H: Exists P (tl x)
n: nat
Hn: P (Str_nth_tl n (tl x))
∃ n : nat, P (Str_nth_tl n x)
    by exists (S n).
  -A: Type
P: Stream A → Prop
s: Stream A
(∃ n : nat, P (Str_nth_tl n s)) → Exists P s intros [n Hn].A: Type
P: Stream A → Prop
s: Stream A
n: nat
Hn: P (Str_nth_tl n s)
Exists P s revert s Hn.A: Type
P: Stream A → Prop
n: nat
∀ s : Stream A, P (Str_nth_tl n s) → Exists P s
    induction n; [by apply Here |].A: Type
P: Stream A → Prop
n: nat
IHn: ∀ s : Stream A, P (Str_nth_tl n s) → Exists P s
∀ s : Stream A, P (Str_nth_tl (S n) s) → Exists P s
    intros s Hs.A: Type
P: Stream A → Prop
n: nat
IHn: ∀ s : Stream A, P (Str_nth_tl n s) → Exists P s
s: Stream A
Hs: P (Str_nth_tl (S n) s)
Exists P s specialize (IHn (tl s) Hs).A: Type
P: Stream A → Prop
n: nat
s: Stream A
IHn: Exists P (tl s)
Hs: P (Str_nth_tl (S n) s)
Exists P s
    by apply Further.
Qed.

Retrieve an existential quantifier that works on elements from Exists, which works on substreams.

Definition Exists1 [A : Type] (P : A -> Prop) := Exists (fun s => P (hd s)).

Lemma Exists1_exists [A : Type] (P : A -> Prop) s
  : Exists1 P s <-> exists n, P (Str_nth n s).A: Type
P: A → Prop
s: Stream A
Exists1 P s ↔ (∃ n : nat, P (Str_nth n s))
Proof.A: Type
P: A → Prop
s: Stream A
Exists1 P s ↔ (∃ n : nat, P (Str_nth n s))
  split.A: Type
P: A → Prop
s: Stream A
Exists1 P s → ∃ n : nat, P (Str_nth n s)
A: Type
P: A → Prop
s: Stream A
(∃ n : nat, P (Str_nth n s)) → Exists1 P s
  -A: Type
P: A → Prop
s: Stream A
Exists1 P s → ∃ n : nat, P (Str_nth n s) induction 1.A: Type
P: A → Prop
x: Stream A
H: P (hd x)
∃ n : nat, P (Str_nth n x)
A: Type
P: A → Prop
x: Stream A
H: Exists (λ s : Stream A, P (hd s)) (tl x)
IHExists: ∃ n : nat, P (Str_nth n (tl x))
∃ n : nat, P (Str_nth n x)
    +A: Type
P: A → Prop
x: Stream A
H: P (hd x)
∃ n : nat, P (Str_nth n x) by exists 0.
    +A: Type
P: A → Prop
x: Stream A
H: Exists (λ s : Stream A, P (hd s)) (tl x)
IHExists: ∃ n : nat, P (Str_nth n (tl x))
∃ n : nat, P (Str_nth n x) destruct IHExists as [n Hp].A: Type
P: A → Prop
x: Stream A
H: Exists (λ s : Stream A, P (hd s)) (tl x)
n: nat
Hp: P (Str_nth n (tl x))
∃ n : nat, P (Str_nth n x)
      by exists (S n).
  -A: Type
P: A → Prop
s: Stream A
(∃ n : nat, P (Str_nth n s)) → Exists1 P s intros [n Hp].A: Type
P: A → Prop
s: Stream A
n: nat
Hp: P (Str_nth n s)
Exists1 P s revert s Hp.A: Type
P: A → Prop
n: nat
∀ s : Stream A, P (Str_nth n s) → Exists1 P s induction n; intros.A: Type
P: A → Prop
s: Stream A
Hp: P (Str_nth 0 s)
Exists1 P s
A: Type
P: A → Prop
n: nat
IHn: ∀ s : Stream A, P (Str_nth n s) → Exists1 P s
s: Stream A
Hp: P (Str_nth (S n) s)
Exists1 P s
    +A: Type
P: A → Prop
s: Stream A
Hp: P (Str_nth 0 s)
Exists1 P s by constructor.
    +A: Type
P: A → Prop
n: nat
IHn: ∀ s : Stream A, P (Str_nth n s) → Exists1 P s
s: Stream A
Hp: P (Str_nth (S n) s)
Exists1 P s by apply Further, IHn.
Qed.

Retrieve a universal quantifier that works on elements from ForAll, which works on substreams.

Definition ForAll1 [A : Type] (P : A -> Prop) := ForAll (fun s => P (hd s)).

Lemma ForAll1_subsumption [A : Type] (P Q : A -> Prop)
  (HPQ : forall a, P a -> Q a)
  : forall s, ForAll1 P s -> ForAll1 Q s.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A, ForAll1 P s → ForAll1 Q s
Proof.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A, ForAll1 P s → ForAll1 Q s
  by apply ForAll_subsumption; intro s; apply HPQ.
Qed.

Lemma ForAll1_forall [A : Type] (P : A -> Prop) s
  : ForAll1 P s <-> forall n, P (Str_nth n s).A: Type
P: A → Prop
s: Stream A
ForAll1 P s ↔ (∀ n : nat, P (Str_nth n s))
Proof.A: Type
P: A → Prop
s: Stream A
ForAll1 P s ↔ (∀ n : nat, P (Str_nth n s))
  split; intros.A: Type
P: A → Prop
s: Stream A
H: ForAll1 P s
n: nat
P (Str_nth n s)
A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
ForAll1 P s
  -A: Type
P: A → Prop
s: Stream A
H: ForAll1 P s
n: nat
P (Str_nth n s) by apply ForAll_Str_nth_tl with (m := n) in H; apply H.
  -A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
ForAll1 P s apply ForAll_coind with (fun s : Stream A => forall n : nat, P (Str_nth n s))
    ; intros.A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
x: Stream A
H0: ∀ n : nat, P (Str_nth n x)
P (hd x)
A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
x: Stream A
H0: ∀ n : nat, P (Str_nth n x)
n: nat
P (Str_nth n (tl x))
A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
n: nat
P (Str_nth n s)
    +A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
x: Stream A
H0: ∀ n : nat, P (Str_nth n x)
P (hd x) by specialize (H0 0).
    +A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
x: Stream A
H0: ∀ n : nat, P (Str_nth n x)
n: nat
P (Str_nth n (tl x)) by specialize (H0 (S n)).
    +A: Type
P: A → Prop
s: Stream A
H: ∀ n : nat, P (Str_nth n s)
n: nat
P (Str_nth n s) by apply H.
Qed.

Definition ForAll2 [A : Type] (R : A -> A -> Prop) := ForAll (fun s => R (hd s) (hd (tl s))).

Lemma ForAll2_subsumption [A : Type] (R1 R2 : A -> A -> Prop)
  (HR : forall a b, R1 a b -> R2 a b)
  : forall s, ForAll2 R1 s -> ForAll2 R2 s.A: Type
R1, R2: A → A → Prop
HR: ∀ a b : A, R1 a b → R2 a b
∀ s : Stream A, ForAll2 R1 s → ForAll2 R2 s
Proof.A: Type
R1, R2: A → A → Prop
HR: ∀ a b : A, R1 a b → R2 a b
∀ s : Stream A, ForAll2 R1 s → ForAll2 R2 s
  by apply ForAll_subsumption; intro s; apply HR.
Qed.

Lemma ForAll2_forall [A : Type] (R : A -> A -> Prop) s
  : ForAll2 R s <-> forall n, R (Str_nth n s) (Str_nth (S n) s).A: Type
R: A → A → Prop
s: Stream A
ForAll2 R s
↔ (∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
Proof.A: Type
R: A → A → Prop
s: Stream A
ForAll2 R s
↔ (∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
  split; intros.A: Type
R: A → A → Prop
s: Stream A
H: ForAll2 R s
n: nat
R (Str_nth n s) (Str_nth (S n) s)
A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
ForAll2 R s
  -A: Type
R: A → A → Prop
s: Stream A
H: ForAll2 R s
n: nat
R (Str_nth n s) (Str_nth (S n) s) apply ForAll_Str_nth_tl with (m := n), fHere in H.A: Type
R: A → A → Prop
s: Stream A
n: nat
H: R (hd (Str_nth_tl n s)) (hd (tl (Str_nth_tl n s)))
R (Str_nth n s) (Str_nth (S n) s)
    by rewrite tl_nth_tl in H.
  -A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
ForAll2 R s apply ForAll_coind with (fun s : Stream A => forall n : nat, R (Str_nth n s) (Str_nth (S n) s))
    ; intros.A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
x: Stream A
H0: ∀ n : nat, R (Str_nth n x) (Str_nth (S n) x)
R (hd x) (hd (tl x))
A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
x: Stream A
H0: ∀ n : nat, R (Str_nth n x) (Str_nth (S n) x)
n: nat
R (Str_nth n (tl x)) (Str_nth (S n) (tl x))
A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n: nat
R (Str_nth n s) (Str_nth (S n) s)
    +A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
x: Stream A
H0: ∀ n : nat, R (Str_nth n x) (Str_nth (S n) x)
R (hd x) (hd (tl x)) by apply (H0 0).
    +A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
x: Stream A
H0: ∀ n : nat, R (Str_nth n x) (Str_nth (S n) x)
n: nat
R (Str_nth n (tl x)) (Str_nth (S n) (tl x)) by apply (H0 (S n)).
    +A: Type
R: A → A → Prop
s: Stream A
H: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n: nat
R (Str_nth n s) (Str_nth (S n) s) by apply H.
Qed.

Lemma recons
  {A : Type}
  (s : Stream A)
  : Cons (hd s) (tl s) = s.A: Type
s: Stream A
Cons (hd s) (tl s) = s
Proof.A: Type
s: Stream A
Cons (hd s) (tl s) = s
  by case s.
Qed.

Appends a stream to a list, yielding a stream.

Definition stream_app
  {A : Type}
  (prefix : list A)
  (suffix : Stream A)
  : Stream A
  :=
  fold_right (@Cons A) suffix prefix.

Definition stream_app_cons {A}
  (a : A)
  (l : Stream A)
  : stream_app [a] l = Cons a l
  := eq_refl.

Lemma stream_app_assoc
  {A : Type}
  (l m : list A)
  (n : Stream A)
  : stream_app l (stream_app m n) = stream_app (l ++ m) n.A: Type
l, m: list A
n: Stream A
stream_app l (stream_app m n) = stream_app (l ++ m) n
Proof.A: Type
l, m: list A
n: Stream A
stream_app l (stream_app m n) = stream_app (l ++ m) n
  by induction l; cbn; f_equal.
Qed.

Lemma stream_app_f_equal
  {A : Type}
  (l1 l2 : list A)
  (s1 s2 : Stream A)
  (Hl : l1 = l2)
  (Hs : EqSt s1 s2)
  : EqSt (stream_app l1 s1) (stream_app l2 s2).A: Type
l1, l2: list A
s1, s2: Stream A
Hl: l1 = l2
Hs: EqSt s1 s2
EqSt (stream_app l1 s1) (stream_app l2 s2)
Proof.A: Type
l1, l2: list A
s1, s2: Stream A
Hl: l1 = l2
Hs: EqSt s1 s2
EqSt (stream_app l1 s1) (stream_app l2 s2)
  by subst; induction l2; [| constructor].
Qed.

Lemma stream_app_inj_l
  {A : Type}
  (l1 l2 : list A)
  (s : Stream A)
  (Heq : stream_app l1 s = stream_app l2 s)
  (Heq_len : length l1 = length l2)
  : l1 = l2.A: Type
l1, l2: list A
s: Stream A
Heq: stream_app l1 s = stream_app l2 s
Heq_len: length l1 = length l2
l1 = l2
Proof.A: Type
l1, l2: list A
s: Stream A
Heq: stream_app l1 s = stream_app l2 s
Heq_len: length l1 = length l2
l1 = l2
  generalize dependent l2.A: Type
l1: list A
s: Stream A
∀ l2 : list A,
  stream_app l1 s = stream_app l2 s
  → length l1 = length l2 → l1 = l2
  induction l1; intros; destruct l2; try done; try inversion Heq_len.A: Type
a: A
l1: list A
s: Stream A
IHl1: ∀ l2 : list A,
  stream_app l1 s = stream_app l2 s
  → length l1 = length l2 → l1 = l2
a0: A
l2: list A
Heq: stream_app (a :: l1) s = stream_app (a0 :: l2) s
Heq_len: length (a :: l1) = length (a0 :: l2)
H0: length l1 = length l2
a :: l1 = a0 :: l2
  inversion Heq.A: Type
a: A
l1: list A
s: Stream A
IHl1: ∀ l2 : list A,
  stream_app l1 s = stream_app l2 s
  → length l1 = length l2 → l1 = l2
a0: A
l2: list A
Heq: stream_app (a :: l1) s = stream_app (a0 :: l2) s
Heq_len: length (a :: l1) = length (a0 :: l2)
H0: length l1 = length l2
H1: a = a0
H2: stream_app l1 s = stream_app l2 s
a0 :: l1 = a0 :: l2
  by rewrite (IHl1 l2 H2 H0).
Qed.

Fixpoint stream_prefix
  {A : Type}
  (l : Stream A)
  (n : nat)
  : list A
  := match n, l with
  | 0, _ => []
  | S n, Cons a l => a :: stream_prefix l n
  end.

Lemma stream_prefix_nth
  {A : Type}
  (s : Stream A)
  (n : nat)
  (i : nat)
  (Hi : i < n)
  : nth_error (stream_prefix s n) i = Some (Str_nth i s).A: Type
s: Stream A
n, i: nat
Hi: i < n
nth_error (stream_prefix s n) i = Some (Str_nth i s)
Proof.A: Type
s: Stream A
n, i: nat
Hi: i < n
nth_error (stream_prefix s n) i = Some (Str_nth i s)
  revert s n Hi.A: Type
i: nat
∀ (s : Stream A) (n : nat),
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
  induction i; intros [a s] [| n] Hi; [by inversion Hi .. |].A: Type
i: nat
IHi: ∀ (s : Stream A) (n : nat),
i < n → nth_error (stream_prefix s n) i = Some (Str_nth i s)
a: A
s: Stream A
n: nat
Hi: S i < S n
nth_error (stream_prefix (Cons a s) (S n)) (S i) =
Some (Str_nth (S i) (Cons a s))
  by apply IHi; lia.
Qed.

Lemma stream_prefix_lookup
  {A : Type}
  (s : Stream A)
  (n : nat)
  (i : nat)
  (Hi : i < n)
  : stream_prefix s n !! i = Some (Str_nth i s).A: Type
s: Stream A
n, i: nat
Hi: i < n
stream_prefix s n !! i = Some (Str_nth i s)
Proof.A: Type
s: Stream A
n, i: nat
Hi: i < n
stream_prefix s n !! i = Some (Str_nth i s)
  revert s n Hi.A: Type
i: nat
∀ (s : Stream A) (n : nat),
  i < n → stream_prefix s n !! i = Some (Str_nth i s)
  induction i; intros [a s] [| n] Hi; [by inversion Hi .. |].A: Type
i: nat
IHi: ∀ (s : Stream A) (n : nat),
i < n → stream_prefix s n !! i = Some (Str_nth i s)
a: A
s: Stream A
n: nat
Hi: S i < S n
stream_prefix (Cons a s) (S n) !! S i =
Some (Str_nth (S i) (Cons a s))
  by apply IHi; lia.
Qed.

Lemma stream_prefix_S
  {A : Type}
  (s : Stream A)
  (n : nat)
  : stream_prefix s (S n) = stream_prefix s n ++ [Str_nth n s].A: Type
s: Stream A
n: nat
stream_prefix s (S n) =
stream_prefix s n ++ [Str_nth n s]
Proof.A: Type
s: Stream A
n: nat
stream_prefix s (S n) =
stream_prefix s n ++ [Str_nth n s]
  revert s.A: Type
n: nat
∀ s : Stream A,
  stream_prefix s (S n) =
  stream_prefix s n ++ [Str_nth n s]
  by induction n; intros; rewrite <- (recons s); cbn; f_equal; rewrite <- IHn.
Qed.

Lemma stream_prefix_EqSt
  {A : Type}
  (s1 s2 : Stream A)
  (Heq : EqSt s1 s2)
  : forall n : nat, stream_prefix s1 n = stream_prefix s2 n .A: Type
s1, s2: Stream A
Heq: EqSt s1 s2
∀ n : nat, stream_prefix s1 n = stream_prefix s2 n
Proof.A: Type
s1, s2: Stream A
Heq: EqSt s1 s2
∀ n : nat, stream_prefix s1 n = stream_prefix s2 n
  intro n; revert s1 s2 Heq.A: Type
n: nat
∀ s1 s2 : Stream A,
  EqSt s1 s2 → stream_prefix s1 n = stream_prefix s2 n
  induction n; [done |]; intros [a1 s1] [a2 s2] Heq.A: Type
n: nat
IHn: ∀ s1 s2 : Stream A, EqSt s1 s2 → stream_prefix s1 n = stream_prefix s2 n
a1: A
s1: Stream A
a2: A
s2: Stream A
Heq: EqSt (Cons a1 s1) (Cons a2 s2)
stream_prefix (Cons a1 s1) (S n) =
stream_prefix (Cons a2 s2) (S n)
  by inversion Heq; cbn in *; subst; erewrite IHn.
Qed.

Lemma EqSt_stream_prefix
  {A : Type}
  (s1 s2 : Stream A)
  (Hpref : forall n : nat, stream_prefix s1 n = stream_prefix s2 n)
  : EqSt s1 s2.A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
EqSt s1 s2
Proof.A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
EqSt s1 s2
  apply ntheq_eqst.A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
∀ n : nat, Str_nth n s1 = Str_nth n s2
  intro n.A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Str_nth n s1 = Str_nth n s2
  assert (Hlt : n < S n) by constructor.A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
Str_nth n s1 = Str_nth n s2
  assert (HSome : Some (Str_nth n s1) = Some (Str_nth n s2)).A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
Some (Str_nth n s1) = Some (Str_nth n s2)
A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
HSome: Some (Str_nth n s1) = Some (Str_nth n s2)
Str_nth n s1 = Str_nth n s2
  {A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
Some (Str_nth n s1) = Some (Str_nth n s2)
    rewrite <- (stream_prefix_nth  s1 (S n) n Hlt).A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
nth_error (stream_prefix s1 (S n)) n =
Some (Str_nth n s2)
    rewrite <- (stream_prefix_nth  s2 (S n) n Hlt).A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
nth_error (stream_prefix s1 (S n)) n =
nth_error (stream_prefix s2 (S n)) n
    by rewrite (Hpref (S n)).
  }A: Type
s1, s2: Stream A
Hpref: ∀ n : nat,
  stream_prefix s1 n = stream_prefix s2 n
n: nat
Hlt: n < S n
HSome: Some (Str_nth n s1) = Some (Str_nth n s2)
Str_nth n s1 = Str_nth n s2
  by inversion HSome.
Qed.

Lemma elem_of_stream_prefix
  {A : Type}
  (l : Stream A)
  (n : nat)
  (a : A)
  : a ∈ stream_prefix l n <-> exists k : nat, k < n /\ Str_nth k l = a.A: Type
l: Stream A
n: nat
a: A
a ∈ stream_prefix l n
↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
Proof.A: Type
l: Stream A
n: nat
a: A
a ∈ stream_prefix l n
↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
  revert l a.A: Type
n: nat
∀ (l : Stream A) (a : A),
  a ∈ stream_prefix l n
  ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
  induction n; simpl; split; intros.A: Type
l: Stream A
a: A
H: a ∈ []
∃ k : nat, k < 0 ∧ Str_nth k l = a
A: Type
l: Stream A
a: A
H: ∃ k : nat, k < 0 ∧ Str_nth k l = a
a ∈ []
A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
l: Stream A
a: A
H: a
∈ match l with
  | Cons a l => a :: stream_prefix l n
  end
∃ k : nat, k < S n ∧ Str_nth k l = a
A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
l: Stream A
a: A
H: ∃ k : nat, k < S n ∧ Str_nth k l = a
a
∈ match l with
  | Cons a l => a :: stream_prefix l n
  end
  -A: Type
l: Stream A
a: A
H: a ∈ []
∃ k : nat, k < 0 ∧ Str_nth k l = a by inversion H.
  -A: Type
l: Stream A
a: A
H: ∃ k : nat, k < 0 ∧ Str_nth k l = a
a ∈ [] by destruct H as [k [Hk _]]; lia.
  -A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
l: Stream A
a: A
H: a
∈ match l with
  | Cons a l => a :: stream_prefix l n
  end
∃ k : nat, k < S n ∧ Str_nth k l = a destruct l as (b, l).A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
H: a ∈ b :: stream_prefix l n
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = a
    inversion H; subst.A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
H: b ∈ b :: stream_prefix l n
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = b
A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
H: a ∈ b :: stream_prefix l n
H2: a ∈ stream_prefix l n
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = a
    +A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
H: b ∈ b :: stream_prefix l n
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = b by exists 0; split; [lia |].
    +A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
H: a ∈ b :: stream_prefix l n
H2: a ∈ stream_prefix l n
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = a apply IHn in H2 as [k [Hlt Heq]].A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
H: a ∈ b :: stream_prefix l n
k: nat
Hlt: k < n
Heq: Str_nth k l = a
∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = a
      by exists (S k); split; [lia |].
  -A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
l: Stream A
a: A
H: ∃ k : nat, k < S n ∧ Str_nth k l = a
a
∈ match l with
  | Cons a l => a :: stream_prefix l n
  end destruct l as (b, l).A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
H: ∃ k : nat, k < S n ∧ Str_nth k (Cons b l) = a
a ∈ b :: stream_prefix l n
    destruct H as [k [Hlt Heq]].A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
k: nat
Hlt: k < S n
Heq: Str_nth k (Cons b l) = a
a ∈ b :: stream_prefix l n
    destruct k.A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
Hlt: 0 < S n
Heq: Str_nth 0 (Cons b l) = a
a ∈ b :: stream_prefix l n
A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
k: nat
Hlt: S k < S n
Heq: Str_nth (S k) (Cons b l) = a
a ∈ b :: stream_prefix l n
    +A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
Hlt: 0 < S n
Heq: Str_nth 0 (Cons b l) = a
a ∈ b :: stream_prefix l n by unfold Str_nth in Heq; simpl in Heq; subst; left.
    +A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ Str_nth k l = a)
b: A
l: Stream A
a: A
k: nat
Hlt: S k < S n
Heq: Str_nth (S k) (Cons b l) = a
a ∈ b :: stream_prefix l n unfold Str_nth in *; simpl in Heq.A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ hd (Str_nth_tl k l) = a)
b: A
l: Stream A
a: A
k: nat
Hlt: S k < S n
Heq: hd (Str_nth_tl k l) = a
a ∈ b :: stream_prefix l n
      right; apply IHn.A: Type
n: nat
IHn: ∀ (l : Stream A) (a : A),
a ∈ stream_prefix l n ↔ (∃ k : nat, k < n ∧ hd (Str_nth_tl k l) = a)
b: A
l: Stream A
a: A
k: nat
Hlt: S k < S n
Heq: hd (Str_nth_tl k l) = a
∃ k : nat, k < n ∧ hd (Str_nth_tl k l) = a
      by exists k; split; [lia |].
Qed.

Lemma stream_prefix_app_l
  {A : Type}
  (l : list A)
  (s : Stream A)
  (n : nat)
  (Hle : n <= length l)
  : stream_prefix (stream_app l s) n = take n l.A: Type
l: list A
s: Stream A
n: nat
Hle: n ≤ length l
stream_prefix (stream_app l s) n = take n l
Proof.A: Type
l: list A
s: Stream A
n: nat
Hle: n ≤ length l
stream_prefix (stream_app l s) n = take n l
  revert n Hle; induction l; intros [| n] Hle; [by inversion Hle.. |].A: Type
a: A
l: list A
s: Stream A
IHl: ∀ n : nat, n ≤ length l → stream_prefix (stream_app l s) n = take n l
n: nat
Hle: S n ≤ length (a :: l)
stream_prefix (stream_app (a :: l) s) (S n) =
take (S n) (a :: l)
  by cbn in *; rewrite IHl; [| lia].
Qed.

Lemma stream_prefix_app_r
  {A : Type}
  (l : list A)
  (s : Stream A)
  (n : nat)
  (Hge : n >= length l)
  : stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l).A: Type
l: list A
s: Stream A
n: nat
Hge: n ≥ length l
stream_prefix (stream_app l s) n =
l ++ stream_prefix s (n - length l)
Proof.A: Type
l: list A
s: Stream A
n: nat
Hge: n ≥ length l
stream_prefix (stream_app l s) n =
l ++ stream_prefix s (n - length l)
  generalize dependent l.A: Type
s: Stream A
n: nat
∀ l : list A,
  n ≥ length l
  → stream_prefix (stream_app l s) n =
    l ++ stream_prefix s (n - length l)
  generalize dependent s.A: Type
n: nat
∀ (s : Stream A) (l : list A),
  n ≥ length l
  → stream_prefix (stream_app l s) n =
    l ++ stream_prefix s (n - length l)
  induction n.A: Type
∀ (s : Stream A) (l : list A),
  0 ≥ length l
  → stream_prefix (stream_app l s) 0 =
    l ++ stream_prefix s (0 - length l)
A: Type
n: nat
IHn: ∀ (s : Stream A) (l : list A),
n ≥ length l
→ stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l)
∀ (s : Stream A) (l : list A),
  S n ≥ length l
  → stream_prefix (stream_app l s) (S n) =
    l ++ stream_prefix s (S n - length l)
  -A: Type
∀ (s : Stream A) (l : list A),
  0 ≥ length l
  → stream_prefix (stream_app l s) 0 =
    l ++ stream_prefix s (0 - length l) by intros s [| a l] Hge; cbn in *; [| lia].
  -A: Type
n: nat
IHn: ∀ (s : Stream A) (l : list A),
n ≥ length l
→ stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l)
∀ (s : Stream A) (l : list A),
  S n ≥ length l
  → stream_prefix (stream_app l s) (S n) =
    l ++ stream_prefix s (S n - length l) intros s [| a l] Hge; cbn in *; [done |].A: Type
n: nat
IHn: ∀ (s : Stream A) (l : list A),
n ≥ length l
→ stream_prefix (stream_app l s) n = l ++ stream_prefix s (n - length l)
s: Stream A
a: A
l: list A
Hge: S n ≥ S (length l)
a :: stream_prefix (foldr (Cons (A:=A)) s l) n =
a :: l ++ stream_prefix s (n - length l)
    by rewrite <- IHn; [| lia].
Qed.

Lemma stream_prefix_map
  {A B : Type}
  (f : A -> B)
  (l : Stream A)
  (n : nat)
  : List.map f (stream_prefix l n) = stream_prefix (Streams.map f l) n.A, B: Type
f: A → B
l: Stream A
n: nat
List.map f (stream_prefix l n) =
stream_prefix (map f l) n
Proof.A, B: Type
f: A → B
l: Stream A
n: nat
List.map f (stream_prefix l n) =
stream_prefix (map f l) n
  by revert l; induction n; intros [a l]; cbn; rewrite ?IHn.
Qed.

Lemma stream_prefix_length
  {A : Type}
  (l : Stream A)
  (n : nat)
  : length (stream_prefix l n) = n.A: Type
l: Stream A
n: nat
length (stream_prefix l n) = n
Proof.A: Type
l: Stream A
n: nat
length (stream_prefix l n) = n
  by revert l; induction n; intros [a l]; cbn; rewrite ?IHn.
Qed.

The following two lemmas connect forall quantifiers looking at one element or two consecutive elements at a time with corresponding list quantifiers applied on their finite prefixes.

Lemma stream_prefix_ForAll
  {A : Type}
  (P : A -> Prop)
  (s : Stream A)
  : ForAll1 P s <-> forall n : nat, Forall P (stream_prefix s n).A: Type
P: A → Prop
s: Stream A
ForAll1 P s
↔ (∀ n : nat, Forall P (stream_prefix s n))
Proof.A: Type
P: A → Prop
s: Stream A
ForAll1 P s
↔ (∀ n : nat, Forall P (stream_prefix s n))
  rewrite ForAll1_forall.A: Type
P: A → Prop
s: Stream A
(∀ n : nat, P (Str_nth n s))
↔ (∀ n : nat, Forall P (stream_prefix s n))
  setoid_rewrite (Forall_nth P (hd s)).A: Type
P: A → Prop
s: Stream A
(∀ n : nat, P (Str_nth n s))
↔ (∀ n i : nat,
     i < length (stream_prefix s n)
     → P (nth i (stream_prefix s n) (hd s)))
  setoid_rewrite stream_prefix_length.A: Type
P: A → Prop
s: Stream A
(∀ n : nat, P (Str_nth n s))
↔ (∀ n i : nat,
     i < n → P (nth i (stream_prefix s n) (hd s)))
  specialize (stream_prefix_nth s) as Hi.A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
(∀ n : nat, P (Str_nth n s))
↔ (∀ n i : nat,
     i < n → P (nth i (stream_prefix s n) (hd s)))
  split.A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
(∀ n : nat, P (Str_nth n s))
→ ∀ n i : nat,
    i < n → P (nth i (stream_prefix s n) (hd s))
A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
(∀ n i : nat,
   i < n → P (nth i (stream_prefix s n) (hd s)))
→ ∀ n : nat, P (Str_nth n s)
  -A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
(∀ n : nat, P (Str_nth n s))
→ ∀ n i : nat,
    i < n → P (nth i (stream_prefix s n) (hd s)) intros Hp n i Hlt.A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
Hp: ∀ n : nat, P (Str_nth n s)
n, i: nat
Hlt: i < n
P (nth i (stream_prefix s n) (hd s))
    specialize (Hi _ _ Hlt).A: Type
P: A → Prop
s: Stream A
n, i: nat
Hi: nth_error (stream_prefix s n) i =
Some (Str_nth i s)
Hp: ∀ n : nat, P (Str_nth n s)
Hlt: i < n
P (nth i (stream_prefix s n) (hd s))
    by apply nth_error_nth with (d := hd s) in Hi; rewrite Hi.
  -A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
(∀ n i : nat,
   i < n → P (nth i (stream_prefix s n) (hd s)))
→ ∀ n : nat, P (Str_nth n s) intros Hp n.A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
Hp: ∀ n i : nat,
  i < n → P (nth i (stream_prefix s n) (hd s))
n: nat
P (Str_nth n s)
    assert (Hn : n < S n) by lia.A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
Hp: ∀ n i : nat,
  i < n → P (nth i (stream_prefix s n) (hd s))
n: nat
Hn: n < S n
P (Str_nth n s)
    specialize (Hp _ _ Hn).A: Type
P: A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → nth_error (stream_prefix s n) i =
    Some (Str_nth i s)
n: nat
Hp: P (nth n (stream_prefix s (S n)) (hd s))
Hn: n < S n
P (Str_nth n s)
    specialize (Hi _ _ Hn).A: Type
P: A → Prop
s: Stream A
n: nat
Hi: nth_error (stream_prefix s (S n)) n =
Some (Str_nth n s)
Hp: P (nth n (stream_prefix s (S n)) (hd s))
Hn: n < S n
P (Str_nth n s)
    apply nth_error_nth with (d := hd s) in Hi.A: Type
P: A → Prop
s: Stream A
n: nat
Hi: nth n (stream_prefix s (S n)) (hd s) =
Str_nth n s
Hp: P (nth n (stream_prefix s (S n)) (hd s))
Hn: n < S n
P (Str_nth n s)
    by rewrite Hi in Hp.
Qed.

Lemma stream_prefix_ForAll2
  {A : Type}
  (R : A -> A -> Prop)
  (s : Stream A)
  : ForAll2 R s <-> forall n : nat, ForAllSuffix2 R (stream_prefix s n).A: Type
R: A → A → Prop
s: Stream A
ForAll2 R s
↔ (∀ n : nat, ForAllSuffix2 R (stream_prefix s n))
Proof.A: Type
R: A → A → Prop
s: Stream A
ForAll2 R s
↔ (∀ n : nat, ForAllSuffix2 R (stream_prefix s n))
  rewrite ForAll2_forall.A: Type
R: A → A → Prop
s: Stream A
(∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
↔ (∀ n : nat, ForAllSuffix2 R (stream_prefix s n))
  setoid_rewrite (ForAllSuffix2_lookup R).A: Type
R: A → A → Prop
s: Stream A
(∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
↔ (∀ (n n0 : nat) (a b : A),
     stream_prefix s n !! n0 = Some a
     → stream_prefix s n !! S n0 = Some b → R a b)
  specialize (stream_prefix_lookup s) as Hi.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
↔ (∀ (n n0 : nat) (a b : A),
     stream_prefix s n !! n0 = Some a
     → stream_prefix s n !! S n0 = Some b → R a b)
  split.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
→ ∀ (n n0 : nat) (a b : A),
    stream_prefix s n !! n0 = Some a
    → stream_prefix s n !! S n0 = Some b → R a b
A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ (n n0 : nat) (a b : A),
   stream_prefix s n !! n0 = Some a
   → stream_prefix s n !! S n0 = Some b → R a b)
→ ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
  -A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ n : nat, R (Str_nth n s) (Str_nth (S n) s))
→ ∀ (n n0 : nat) (a b : A),
    stream_prefix s n !! n0 = Some a
    → stream_prefix s n !! S n0 = Some b → R a b intros Hp n i.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b
    destruct (decide (n <= S i)).A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
l: n ≤ S i
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b
A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
n0: ¬ n ≤ S i
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b
    +A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
l: n ≤ S i
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b intros.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
l: n ≤ S i
a, b: A
H: stream_prefix s n !! i = Some a
H0: stream_prefix s n !! S i = Some b
R a b rewrite lookup_ge_None_2 in H0; [done |].A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
l: n ≤ S i
a, b: A
H: stream_prefix s n !! i = Some a
H0: stream_prefix s n !! S i = Some b
length (stream_prefix s n) ≤ S i
      by rewrite stream_prefix_length.
    +A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
n0: ¬ n ≤ S i
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b pose proof (stream_prefix_length s n) as Hlen.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
n0: ¬ n ≤ S i
Hlen: length (stream_prefix s n) = n
∀ a b : A,
  stream_prefix s n !! i = Some a
  → stream_prefix s n !! S i = Some b → R a b
      rewrite (Hi n i), (Hi n (S i)) by lia.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s)
n, i: nat
n0: ¬ n ≤ S i
Hlen: length (stream_prefix s n) = n
∀ a b : A,
  Some (Str_nth i s) = Some a
  → Some (Str_nth (S i) s) = Some b → R a b
      by do 2 inversion 1; subst.
  -A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ (n n0 : nat) (a b : A),
   stream_prefix s n !! n0 = Some a
   → stream_prefix s n !! S n0 = Some b → R a b)
→ ∀ n : nat, R (Str_nth n s) (Str_nth (S n) s) intros Hp n.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ (n n0 : nat) (a b : A),
  stream_prefix s n !! n0 = Some a
  → stream_prefix s n !! S n0 = Some b → R a b
n: nat
R (Str_nth n s) (Str_nth (S n) s)
    specialize (Hp (S (S n)) n).A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
n: nat
Hp: ∀ a b : A,
  stream_prefix s (S (S n)) !! n = Some a
  → stream_prefix s (S (S n)) !! S n = Some b
    → R a b
R (Str_nth n s) (Str_nth (S n) s)
    rewrite !Hi in Hp by lia.A: Type
R: A → A → Prop
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
n: nat
Hp: ∀ a b : A,
  Some (Str_nth n s) = Some a
  → Some (Str_nth (S n) s) = Some b → R a b
R (Str_nth n s) (Str_nth (S n) s)
    by apply Hp.
Qed.

Lemma ForAll2_transitive_lookup [A : Type] (R : A -> A -> Prop) {HT : Transitive R}
  : forall l, ForAll2 R l <-> forall m n, m < n -> R (Str_nth m l) (Str_nth n l).A: Type
R: A → A → Prop
HT: Transitive R
∀ l : Stream A,
  ForAll2 R l
  ↔ (∀ m n : nat,
       m < n → R (Str_nth m l) (Str_nth n l))
Proof.A: Type
R: A → A → Prop
HT: Transitive R
∀ l : Stream A,
  ForAll2 R l
  ↔ (∀ m n : nat,
       m < n → R (Str_nth m l) (Str_nth n l))
  setoid_rewrite stream_prefix_ForAll2.A: Type
R: A → A → Prop
HT: Transitive R
∀ l : Stream A,
  (∀ n : nat, ForAllSuffix2 R (stream_prefix l n))
  ↔ (∀ m n : nat,
       m < n → R (Str_nth m l) (Str_nth n l))
  setoid_rewrite ForAllSuffix2_transitive_lookup; [| done].A: Type
R: A → A → Prop
HT: Transitive R
∀ l : Stream A,
  (∀ (n m n0 : nat) (a b : A),
     m < n0
     → stream_prefix l n !! m = Some a
       → stream_prefix l n !! n0 = Some b → R a b)
  ↔ (∀ m n : nat,
       m < n → R (Str_nth m l) (Str_nth n l))
  intros s.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
(∀ (n m n0 : nat) (a b : A),
   m < n0
   → stream_prefix s n !! m = Some a
     → stream_prefix s n !! n0 = Some b → R a b)
↔ (∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s))
  specialize (stream_prefix_lookup s) as Hi.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ (n m n0 : nat) (a b : A),
   m < n0
   → stream_prefix s n !! m = Some a
     → stream_prefix s n !! n0 = Some b → R a b)
↔ (∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s))
  split.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ (n m n0 : nat) (a b : A),
   m < n0
   → stream_prefix s n !! m = Some a
     → stream_prefix s n !! n0 = Some b → R a b)
→ ∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s)
A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s))
→ ∀ (n m n0 : nat) (a b : A),
    m < n0
    → stream_prefix s n !! m = Some a
      → stream_prefix s n !! n0 = Some b → R a b
  -A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ (n m n0 : nat) (a b : A),
   m < n0
   → stream_prefix s n !! m = Some a
     → stream_prefix s n !! n0 = Some b → R a b)
→ ∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s) intros Hp i j Hij.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ (n m n0 : nat) (a b : A),
  m < n0
  → stream_prefix s n !! m = Some a
    → stream_prefix s n !! n0 = Some b → R a b
i, j: nat
Hij: i < j
R (Str_nth i s) (Str_nth j s)
    specialize (Hp (S j) i j (Str_nth i s) (Str_nth j s) Hij).A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
i, j: nat
Hp: stream_prefix s (S j) !! i = Some (Str_nth i s)
→ stream_prefix s (S j) !! j = Some (Str_nth j s)
  → R (Str_nth i s) (Str_nth j s)
Hij: i < j
R (Str_nth i s) (Str_nth j s)
    rewrite !Hi in Hp by lia.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
i, j: nat
Hp: Some (Str_nth i s) = Some (Str_nth i s)
→ Some (Str_nth j s) = Some (Str_nth j s)
  → R (Str_nth i s) (Str_nth j s)
Hij: i < j
R (Str_nth i s) (Str_nth j s)
    by apply Hp.
  -A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
(∀ m n : nat, m < n → R (Str_nth m s) (Str_nth n s))
→ ∀ (n m n0 : nat) (a b : A),
    m < n0
    → stream_prefix s n !! m = Some a
      → stream_prefix s n !! n0 = Some b → R a b intros Hp n i j a b Hlt Ha Hb.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ m n : nat,
  m < n → R (Str_nth m s) (Str_nth n s)
n, i, j: nat
a, b: A
Hlt: i < j
Ha: stream_prefix s n !! i = Some a
Hb: stream_prefix s n !! j = Some b
R a b
    apply lookup_lt_Some in Hb as Hltj.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ m n : nat,
  m < n → R (Str_nth m s) (Str_nth n s)
n, i, j: nat
a, b: A
Hlt: i < j
Ha: stream_prefix s n !! i = Some a
Hb: stream_prefix s n !! j = Some b
Hltj: j < length (stream_prefix s n)
R a b
    rewrite stream_prefix_length in Hltj.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ m n : nat,
  m < n → R (Str_nth m s) (Str_nth n s)
n, i, j: nat
a, b: A
Hlt: i < j
Ha: stream_prefix s n !! i = Some a
Hb: stream_prefix s n !! j = Some b
Hltj: j < n
R a b
    rewrite Hi in Ha, Hb by lia.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ m n : nat,
  m < n → R (Str_nth m s) (Str_nth n s)
n, i, j: nat
a, b: A
Hlt: i < j
Ha: Some (Str_nth i s) = Some a
Hb: Some (Str_nth j s) = Some b
Hltj: j < n
R a b
    inversion Ha; inversion Hb.A: Type
R: A → A → Prop
HT: Transitive R
s: Stream A
Hi: ∀ n i : nat,
  i < n
  → stream_prefix s n !! i = Some (Str_nth i s)
Hp: ∀ m n : nat,
  m < n → R (Str_nth m s) (Str_nth n s)
n, i, j: nat
a, b: A
Hlt: i < j
Ha: Some (Str_nth i s) = Some a
Hb: Some (Str_nth j s) = Some b
Hltj: j < n
H0: Str_nth i s = a
H1: Str_nth j s = b
R (Str_nth i s) (Str_nth j s)
    by apply Hp.
Qed.

Lemma ForAll2_strict_lookup_rev [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R}
  (l : Stream A) (Hl : ForAll2 R l)
  : forall m n, R (Str_nth m l) (Str_nth n l) -> m < n.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
∀ m n : nat, R (Str_nth m l) (Str_nth n l) → m < n
Proof.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
∀ m n : nat, R (Str_nth m l) (Str_nth n l) → m < n
  intros m n Hr.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
m < n
  rewrite ForAll2_transitive_lookup in Hl by typeclasses eauto.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
m < n
  destruct (Nat.lt_total m n) as [Hlt | [-> | Hgt]]; [done | |].A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
n: nat
Hr: R (Str_nth n l) (Str_nth n l)
n < n
A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
Hgt: n < m
m < n
  -A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
n: nat
Hr: R (Str_nth n l) (Str_nth n l)
n < n by eapply StrictOrder_Irreflexive in Hr.
  -A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
Hgt: n < m
m < n elim (StrictOrder_Irreflexive (Str_nth n l)).A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
Hgt: n < m
R (Str_nth n l) (Str_nth n l)
    transitivity (Str_nth m l); [| done].A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hr: R (Str_nth m l) (Str_nth n l)
Hgt: n < m
R (Str_nth n l) (Str_nth m l)
    by apply Hl.
Qed.

Lemma ForAll2_strict_lookup [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R}
  : forall l, ForAll2 R l <-> (forall m n, m < n <-> R (Str_nth m l) (Str_nth n l)).A: Type
R: A → A → Prop
HR: StrictOrder R
∀ l : Stream A,
  ForAll2 R l
  ↔ (∀ m n : nat,
       m < n ↔ R (Str_nth m l) (Str_nth n l))
Proof.A: Type
R: A → A → Prop
HR: StrictOrder R
∀ l : Stream A,
  ForAll2 R l
  ↔ (∀ m n : nat,
       m < n ↔ R (Str_nth m l) (Str_nth n l))
  split.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
ForAll2 R l
→ ∀ m n : nat, m < n ↔ R (Str_nth m l) (Str_nth n l)
A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
(∀ m n : nat, m < n ↔ R (Str_nth m l) (Str_nth n l))
→ ForAll2 R l
  -A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
ForAll2 R l
→ ∀ m n : nat, m < n ↔ R (Str_nth m l) (Str_nth n l) intro Hall; split.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ForAll2 R l
m, n: nat
m < n → R (Str_nth m l) (Str_nth n l)
A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ForAll2 R l
m, n: nat
R (Str_nth m l) (Str_nth n l) → m < n
    +A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ForAll2 R l
m, n: nat
m < n → R (Str_nth m l) (Str_nth n l) by apply ForAll2_transitive_lookup; [typeclasses eauto |].
    +A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ForAll2 R l
m, n: nat
R (Str_nth m l) (Str_nth n l) → m < n by apply ForAll2_strict_lookup_rev.
  -A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
(∀ m n : nat, m < n ↔ R (Str_nth m l) (Str_nth n l))
→ ForAll2 R l intro Hall.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ∀ m n : nat,
  m < n ↔ R (Str_nth m l) (Str_nth n l)
ForAll2 R l
    apply ForAll2_transitive_lookup; [typeclasses eauto |].A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hall: ∀ m n : nat,
  m < n ↔ R (Str_nth m l) (Str_nth n l)
∀ m n : nat, m < n → R (Str_nth m l) (Str_nth n l)
    by intros; apply Hall.
Qed.

Lemma ForAll2_strict_lookup_inj
 [A : Type] (R : A -> A -> Prop) {HR : StrictOrder R}
  (l : Stream A) (Hl : ForAll2 R l)
  : forall m n, Str_nth m l = Str_nth n l -> m = n.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
∀ m n : nat, Str_nth m l = Str_nth n l → m = n
Proof.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
∀ m n : nat, Str_nth m l = Str_nth n l → m = n
  intros m n Hmn.A: Type
R: A → A → Prop
HR: StrictOrder R
l: Stream A
Hl: ForAll2 R l
m, n: nat
Hmn: Str_nth m l = Str_nth n l
m = n
  destruct HR as [HI HT].A: Type
R: A → A → Prop
HI: Irreflexive R
HT: Transitive R
l: Stream A
Hl: ForAll2 R l
m, n: nat
Hmn: Str_nth m l = Str_nth n l
m = n
  rewrite ForAll2_transitive_lookup in Hl by done.A: Type
R: A → A → Prop
HI: Irreflexive R
HT: Transitive R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hmn: Str_nth m l = Str_nth n l
m = n
  destruct (decide (m = n)); [done |].A: Type
R: A → A → Prop
HI: Irreflexive R
HT: Transitive R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hmn: Str_nth m l = Str_nth n l
n0: m ≠ n
m = n
  elim (HI (Str_nth n l)).A: Type
R: A → A → Prop
HI: Irreflexive R
HT: Transitive R
l: Stream A
Hl: ∀ m n : nat,
  m < n → R (Str_nth m l) (Str_nth n l)
m, n: nat
Hmn: Str_nth m l = Str_nth n l
n0: m ≠ n
R (Str_nth n l) (Str_nth n l)
  by destruct (decide (m < n))
  ; [specialize (Hl m n) | specialize (Hl n m)]; (spec Hl; [lia |])
  ; rewrite Hmn in Hl.
Qed.

Definition stream_suffix
  {A : Type}
  (l : Stream A)
  (n : nat)
  : Stream A
  := Str_nth_tl n l.

Lemma stream_suffix_S
  {A : Type}
  (l : Stream A)
  (n : nat)
  : stream_suffix l n = Cons (Str_nth n l) (stream_suffix l (S n)).A: Type
l: Stream A
n: nat
stream_suffix l n =
Cons (Str_nth n l) (stream_suffix l (S n))
Proof.A: Type
l: Stream A
n: nat
stream_suffix l n =
Cons (Str_nth n l) (stream_suffix l (S n))
  revert l.A: Type
n: nat
∀ l : Stream A,
  stream_suffix l n =
  Cons (Str_nth n l) (stream_suffix l (S n)) induction n; intros.A: Type
l: Stream A
stream_suffix l 0 =
Cons (Str_nth 0 l) (stream_suffix l 1)
A: Type
n: nat
IHn: ∀ l : Stream A,
stream_suffix l n = Cons (Str_nth n l) (stream_suffix l (S n))
l: Stream A
stream_suffix l (S n) =
Cons (Str_nth (S n) l) (stream_suffix l (S (S n)))
  -A: Type
l: Stream A
stream_suffix l 0 =
Cons (Str_nth 0 l) (stream_suffix l 1) by destruct l.
  -A: Type
n: nat
IHn: ∀ l : Stream A,
stream_suffix l n = Cons (Str_nth n l) (stream_suffix l (S n))
l: Stream A
stream_suffix l (S n) =
Cons (Str_nth (S n) l) (stream_suffix l (S (S n))) by apply IHn.
Qed.

Lemma stream_suffix_nth
  {A : Type}
  (s : Stream A)
  (n : nat)
  (i : nat)
  : Str_nth i (stream_suffix s n) = Str_nth (i + n) s.A: Type
s: Stream A
n, i: nat
Str_nth i (stream_suffix s n) = Str_nth (i + n) s
Proof.A: Type
s: Stream A
n, i: nat
Str_nth i (stream_suffix s n) = Str_nth (i + n) s
  by apply Str_nth_plus.
Qed.

Lemma stream_prefix_suffix
  {A : Type}
  (l : Stream A)
  (n : nat)
  : stream_app (stream_prefix l n) (stream_suffix l n) = l.A: Type
l: Stream A
n: nat
stream_app (stream_prefix l n) (stream_suffix l n) = l
Proof.A: Type
l: Stream A
n: nat
stream_app (stream_prefix l n) (stream_suffix l n) = l
  generalize dependent l.A: Type
n: nat
∀ l : Stream A,
  stream_app (stream_prefix l n) (stream_suffix l n) =
  l unfold stream_suffix.A: Type
n: nat
∀ l : Stream A,
  stream_app (stream_prefix l n) (Str_nth_tl n l) = l
  induction n; [done |]; intros [a l]; cbn.A: Type
n: nat
IHn: ∀ l : Stream A, stream_app (stream_prefix l n) (Str_nth_tl n l) = l
a: A
l: Stream A
Cons a
  (foldr (Cons (A:=A)) (Str_nth_tl n l)
     (stream_prefix l n)) = Cons a l
  by f_equal; apply IHn.
Qed.

Lemma stream_prefix_prefix
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  (Hn : n1 <= n2)
  : take n1 (stream_prefix l n2) = stream_prefix l n1.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
take n1 (stream_prefix l n2) = stream_prefix l n1
Proof.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
take n1 (stream_prefix l n2) = stream_prefix l n1
  revert l n2 Hn.A: Type
n1: nat
∀ (l : Stream A) (n2 : nat),
  n1 ≤ n2
  → take n1 (stream_prefix l n2) = stream_prefix l n1
  induction n1; intros [a l]; intros [| n2] Hn; simpl; [by inversion Hn.. |].A: Type
n1: nat
IHn1: ∀ (l : Stream A) (n2 : nat),
  n1 ≤ n2
  → take n1 (stream_prefix l n2) =
    stream_prefix l n1
a: A
l: Stream A
n2: nat
Hn: S n1 ≤ S n2
a :: take n1 (stream_prefix l n2) =
a :: stream_prefix l n1
  by rewrite IHn1; [| lia].
Qed.

Lemma stream_prefix_of
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  (Hn : n1 <= n2)
  : stream_prefix l n1 `prefix_of` stream_prefix l n2.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 `prefix_of` stream_prefix l n2
Proof.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 `prefix_of` stream_prefix l n2
  rewrite <- (stream_prefix_prefix l n1 n2 Hn).A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
take n1 (stream_prefix l n2)
`prefix_of` stream_prefix l n2
  by apply prefix_of_take.
Qed.

Definition stream_segment
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  : list A
  := drop n1 (stream_prefix l n2).

Lemma stream_segment_nth
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  (Hn : n1 <= n2)
  (i : nat)
  (Hi1 : n1 <= i)
  (Hi2 : i < n2)
  : nth_error (stream_segment l n1 n2) (i - n1) = Some (Str_nth i l).A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
i: nat
Hi1: n1 ≤ i
Hi2: i < n2
nth_error (stream_segment l n1 n2) (i - n1) =
Some (Str_nth i l)
Proof.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
i: nat
Hi1: n1 ≤ i
Hi2: i < n2
nth_error (stream_segment l n1 n2) (i - n1) =
Some (Str_nth i l)
  unfold stream_segment.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
i: nat
Hi1: n1 ≤ i
Hi2: i < n2
nth_error (drop n1 (stream_prefix l n2)) (i - n1) =
Some (Str_nth i l)
  rewrite drop_nth; [| done].A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
i: nat
Hi1: n1 ≤ i
Hi2: i < n2
nth_error (stream_prefix l n2) i = Some (Str_nth i l)
  by apply stream_prefix_nth.
Qed.

Compute the sublist of stream l which starts at index n1 and ends before index n2.

Definition stream_segment_alt
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  : list A
  := stream_prefix (stream_suffix l n1) (n2 - n1).

Lemma stream_segment_alt_iff
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  : stream_segment l n1 n2 = stream_segment_alt l n1 n2.A: Type
l: Stream A
n1, n2: nat
stream_segment l n1 n2 = stream_segment_alt l n1 n2
Proof.A: Type
l: Stream A
n1, n2: nat
stream_segment l n1 n2 = stream_segment_alt l n1 n2
  apply nth_error_eq.A: Type
l: Stream A
n1, n2: nat
∀ n : nat,
  nth_error (stream_segment l n1 n2) n =
  nth_error (stream_segment_alt l n1 n2) n
  intro k.A: Type
l: Stream A
n1, n2, k: nat
nth_error (stream_segment l n1 n2) k =
nth_error (stream_segment_alt l n1 n2) k
  unfold stream_segment_alt.A: Type
l: Stream A
n1, n2, k: nat
nth_error (stream_segment l n1 n2) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k unfold stream_segment.A: Type
l: Stream A
n1, n2, k: nat
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k
  destruct (decide (n2 - n1 <= k)).A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k
A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k
  -A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k specialize (nth_error_None (drop n1 (stream_prefix l n2)) k); intros [_ H].A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k
    specialize (nth_error_None (stream_prefix (stream_suffix l n1) (n2 - n1)) k); intros [_ H_alt].A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
H_alt: length
  (stream_prefix (stream_suffix l n1)
     (n2 - n1)) ≤ k
→ nth_error
    (stream_prefix (stream_suffix l n1)
       (n2 - n1)) k = None
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k
    rewrite H, H_alt; [done | |].A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
H_alt: length
  (stream_prefix (stream_suffix l n1)
     (n2 - n1)) ≤ k
→ nth_error
    (stream_prefix (stream_suffix l n1)
       (n2 - n1)) k = None
length (stream_prefix (stream_suffix l n1) (n2 - n1))
≤ k
A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
H_alt: length
  (stream_prefix (stream_suffix l n1)
     (n2 - n1)) ≤ k
→ nth_error
    (stream_prefix (stream_suffix l n1)
       (n2 - n1)) k = None
length (drop n1 (stream_prefix l n2)) ≤ k
    +A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
H_alt: length
  (stream_prefix (stream_suffix l n1)
     (n2 - n1)) ≤ k
→ nth_error
    (stream_prefix (stream_suffix l n1)
       (n2 - n1)) k = None
length (stream_prefix (stream_suffix l n1) (n2 - n1))
≤ k by rewrite stream_prefix_length.
    +A: Type
l: Stream A
n1, n2, k: nat
l0: n2 - n1 ≤ k
H: length (drop n1 (stream_prefix l n2)) ≤ k
→ nth_error (drop n1 (stream_prefix l n2)) k =
  None
H_alt: length
  (stream_prefix (stream_suffix l n1)
     (n2 - n1)) ≤ k
→ nth_error
    (stream_prefix (stream_suffix l n1)
       (n2 - n1)) k = None
length (drop n1 (stream_prefix l n2)) ≤ k by rewrite drop_length, stream_prefix_length.
  -A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
nth_error (drop n1 (stream_prefix l n2)) k =
nth_error
  (stream_prefix (stream_suffix l n1) (n2 - n1)) k rewrite stream_prefix_nth, stream_suffix_nth by lia.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    assert (Hle : n1 <= n1 + k) by lia.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
Hle: n1 ≤ n1 + k
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    specialize (drop_nth (n1 + k) n1 (stream_prefix l n2) Hle)
    ; intro Heq.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
Hle: n1 ≤ n1 + k
Heq: nth_error (drop n1 (stream_prefix l n2)) (n1 + k - n1) =
nth_error (stream_prefix l n2) (n1 + k)
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    clear Hle.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
Heq: nth_error (drop n1 (stream_prefix l n2)) (n1 + k - n1) =
nth_error (stream_prefix l n2) (n1 + k)
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    assert (Hs : n1 + k - n1 = k) by lia.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
Heq: nth_error (drop n1 (stream_prefix l n2)) (n1 + k - n1) =
nth_error (stream_prefix l n2) (n1 + k)
Hs: n1 + k - n1 = k
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    rewrite Hs in Heq.A: Type
l: Stream A
n1, n2, k: nat
n: ¬ n2 - n1 ≤ k
Heq: nth_error (drop n1 (stream_prefix l n2)) k =
nth_error (stream_prefix l n2) (n1 + k)
Hs: n1 + k - n1 = k
nth_error (drop n1 (stream_prefix l n2)) k =
Some (Str_nth (k + n1) l)
    by rewrite Heq, stream_prefix_nth; [do 2 f_equal |]; lia.
Qed.

Lemma stream_prefix_segment
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  (Hn : n1 <= n2)
  : stream_prefix l n1 ++ stream_segment l n1 n2 = stream_prefix l n2.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 ++ stream_segment l n1 n2 =
stream_prefix l n2
Proof.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 ++ stream_segment l n1 n2 =
stream_prefix l n2
  unfold stream_segment.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 ++ drop n1 (stream_prefix l n2) =
stream_prefix l n2
  rewrite <- (take_drop n1 (stream_prefix l n2)) at 2.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_prefix l n1 ++ drop n1 (stream_prefix l n2) =
take n1 (stream_prefix l n2) ++
drop n1 (stream_prefix l n2)
  by rewrite stream_prefix_prefix.
Qed.

Lemma stream_prefix_segment_suffix
  {A : Type}
  (l : Stream A)
  (n1 n2 : nat)
  (Hn : n1 <= n2)
  : stream_app
      (stream_prefix l n1 ++ stream_segment l n1 n2)
      (stream_suffix l n2)
  = l.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_app
  (stream_prefix l n1 ++ stream_segment l n1 n2)
  (stream_suffix l n2) = l
Proof.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_app
  (stream_prefix l n1 ++ stream_segment l n1 n2)
  (stream_suffix l n2) = l
  rewrite <- (stream_prefix_suffix l n2) at 4.A: Type
l: Stream A
n1, n2: nat
Hn: n1 ≤ n2
stream_app
  (stream_prefix l n1 ++ stream_segment l n1 n2)
  (stream_suffix l n2) =
stream_app (stream_prefix l n2) (stream_suffix l n2)
  by rewrite stream_prefix_segment.
Qed.

Lemma stream_segment_app
  {A : Type}
  (l : Stream A)
  (n1 n2 n3 : nat)
  (H12 : n1 <= n2)
  (H23 : n2 <= n3)
  : stream_segment l n1 n2 ++ stream_segment l n2 n3 = stream_segment l n1 n3.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
Proof.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
  assert (Hle : n1 <= n3) by lia.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
  specialize (stream_prefix_segment_suffix l n1 n3 Hle); intro Hl1.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) = l
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
  specialize (stream_prefix_segment_suffix l n2 n3 H23); intro Hl2.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) = l
Hl2: stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3) = l
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
  rewrite <- Hl2 in Hl1 at 4.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
Hl2: stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3) = l
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3 clear Hl2.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
  apply stream_app_inj_l in Hl1.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n2 ++ stream_segment l n2 n3
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
length (stream_prefix l n1 ++ stream_segment l n1 n3) =
length (stream_prefix l n2 ++ stream_segment l n2 n3)
  -A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n2 ++ stream_segment l n2 n3
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3 specialize (take_drop n1 (stream_prefix l n2)); intro Hl2.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n2 ++ stream_segment l n2 n3
Hl2: take n1 (stream_prefix l n2) ++ drop n1 (stream_prefix l n2) =
stream_prefix l n2
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
    specialize (stream_prefix_prefix l n1 n2 H12); intro Hl3.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n2 ++ stream_segment l n2 n3
Hl2: take n1 (stream_prefix l n2) ++ drop n1 (stream_prefix l n2) =
stream_prefix l n2
Hl3: take n1 (stream_prefix l n2) = stream_prefix l n1
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
    rewrite Hl3 in Hl2.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n2 ++ stream_segment l n2 n3
Hl2: stream_prefix l n1 ++ drop n1 (stream_prefix l n2) = stream_prefix l n2
Hl3: take n1 (stream_prefix l n2) = stream_prefix l n1
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
    rewrite <- Hl2, <- app_assoc in Hl1.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_prefix l n1 ++ stream_segment l n1 n3 =
stream_prefix l n1 ++ drop n1 (stream_prefix l n2) ++ stream_segment l n2 n3
Hl2: stream_prefix l n1 ++ drop n1 (stream_prefix l n2) = stream_prefix l n2
Hl3: take n1 (stream_prefix l n2) = stream_prefix l n1
stream_segment l n1 n2 ++ stream_segment l n2 n3 =
stream_segment l n1 n3
    by apply app_inv_head in Hl1.
  -A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
length (stream_prefix l n1 ++ stream_segment l n1 n3) =
length (stream_prefix l n2 ++ stream_segment l n2 n3) repeat rewrite app_length.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
length (stream_prefix l n1) +
length (stream_segment l n1 n3) =
length (stream_prefix l n2) +
length (stream_segment l n2 n3)
    unfold stream_segment.A: Type
l: Stream A
n1, n2, n3: nat
H12: n1 ≤ n2
H23: n2 ≤ n3
Hle: n1 ≤ n3
Hl1: stream_app (stream_prefix l n1 ++ stream_segment l n1 n3)
(stream_suffix l n3) =
stream_app (stream_prefix l n2 ++ stream_segment l n2 n3)
(stream_suffix l n3)
length (stream_prefix l n1) +
length (drop n1 (stream_prefix l n3)) =
length (stream_prefix l n2) +
length (drop n2 (stream_prefix l n3))
    by rewrite !drop_length, !stream_prefix_length; lia.
Qed.

Definition monotone_nat_stream_prop
  (s : Stream nat)
  := forall n1 n2 : nat, n1 < n2 <-> Str_nth n1 s < Str_nth n2 s.

Lemma monotone_nat_stream_prop_from_successor s
  : ForAll2 lt s <-> monotone_nat_stream_prop s.s: Stream nat
ForAll2 lt s ↔ monotone_nat_stream_prop s
Proof.s: Stream nat
ForAll2 lt s ↔ monotone_nat_stream_prop s by apply ForAll2_strict_lookup; typeclasses eauto. Qed.

Lemma monotone_nat_stream_rev
  (s : Stream nat)
  (Hs : monotone_nat_stream_prop s)
  : forall n1 n2, Str_nth n1  s <= Str_nth n2 s -> n1 <= n2.s: Stream nat
Hs: monotone_nat_stream_prop s
∀ n1 n2 : nat, Str_nth n1 s ≤ Str_nth n2 s → n1 ≤ n2
Proof.s: Stream nat
Hs: monotone_nat_stream_prop s
∀ n1 n2 : nat, Str_nth n1 s ≤ Str_nth n2 s → n1 ≤ n2
  intros n1 n2 Hle.s: Stream nat
Hs: monotone_nat_stream_prop s
n1, n2: nat
Hle: Str_nth n1 s ≤ Str_nth n2 s
n1 ≤ n2
  destruct (decide (n2 < n1)) as [Hlt |]; [| by lia].s: Stream nat
Hs: monotone_nat_stream_prop s
n1, n2: nat
Hle: Str_nth n1 s ≤ Str_nth n2 s
Hlt: n2 < n1
n1 ≤ n2
  by apply Hs in Hlt; lia.
Qed.

Lemma monotone_nat_stream_find s (Hs : monotone_nat_stream_prop s) (n : nat)
  : n < hd s \/ exists k, Str_nth k s = n \/ Str_nth k s < n < Str_nth (S k) s.s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
n < hd s
∨ (∃ k : nat,
     Str_nth k s = n
     ∨ Str_nth k s < n < Str_nth (S k) s)
Proof.s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
n < hd s
∨ (∃ k : nat,
     Str_nth k s = n
     ∨ Str_nth k s < n < Str_nth (S k) s)
  induction n.s: Stream nat
Hs: monotone_nat_stream_prop s
0 < hd s
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s)
s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
IHn: n < hd s ∨ (∃ k : nat, Str_nth k s = n ∨ Str_nth k s < n < Str_nth (S k) s)
S n < hd s
∨ (∃ k : nat,
     Str_nth k s = S n
     ∨ Str_nth k s < S n < Str_nth (S k) s)
  -s: Stream nat
Hs: monotone_nat_stream_prop s
0 < hd s
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s) destruct (hd s) eqn: Hhd.s: Stream nat
Hs: monotone_nat_stream_prop s
Hhd: hd s = 0
0 < 0
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s)
s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
Hhd: hd s = S n
0 < S n
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s)
    +s: Stream nat
Hs: monotone_nat_stream_prop s
Hhd: hd s = 0
0 < 0
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s) by right; exists 0; left.
    +s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
Hhd: hd s = S n
0 < S n
∨ (∃ k : nat,
     Str_nth k s = 0
     ∨ Str_nth k s < 0 < Str_nth (S k) s) by left; lia.
  -s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
IHn: n < hd s ∨ (∃ k : nat, Str_nth k s = n ∨ Str_nth k s < n < Str_nth (S k) s)
S n < hd s
∨ (∃ k : nat,
     Str_nth k s = S n
     ∨ Str_nth k s < S n < Str_nth (S k) s) destruct (decide (hd s <= S n)); [| by left; lia].s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
IHn: n < hd s ∨ (∃ k : nat, Str_nth k s = n ∨ Str_nth k s < n < Str_nth (S k) s)
l: hd s ≤ S n
S n < hd s
∨ (∃ k : nat,
     Str_nth k s = S n
     ∨ Str_nth k s < S n < Str_nth (S k) s)
    right.s: Stream nat
Hs: monotone_nat_stream_prop s
n: nat
IHn: n < hd s ∨ (∃ k : nat, Str_nth k s = n ∨ Str_nth k s < n < Str_nth (S k) s)
l: hd s ≤ S n
∃ k : nat,
  Str_nth k s = S n
  ∨ Str_nth k s < S n < Str_nth (S k) s
    destruct IHn as [Hlt | [k Hk]]
    ; [by exists 0; left; cbv in *; lia |].s: Stream nat
Hs: monotone_nat_stream_prop s
n, k: nat
Hk: Str_nth k s = n
∨ Str_nth k s < n < Str_nth (S k) s
l: hd s ≤ S n
∃ k : nat,
  Str_nth k s = S n
  ∨ Str_nth k s < S n < Str_nth (S k) s
    destruct (decide (Str_nth (S k) s = S n))
    ; [by exists (S k); left |].s: Stream nat
Hs: monotone_nat_stream_prop s
n, k: nat
Hk: Str_nth k s = n
∨ Str_nth k s < n < Str_nth (S k) s
l: hd s ≤ S n
n0: Str_nth (S k) s ≠ S n
∃ k : nat,
  Str_nth k s = S n
  ∨ Str_nth k s < S n < Str_nth (S k) s
    exists k; right.s: Stream nat
Hs: monotone_nat_stream_prop s
n, k: nat
Hk: Str_nth k s = n
∨ Str_nth k s < n < Str_nth (S k) s
l: hd s ≤ S n
n0: Str_nth (S k) s ≠ S n
Str_nth k s < S n < Str_nth (S k) s
    cut (Str_nth k s < Str_nth (S k) s); [by lia |].s: Stream nat
Hs: monotone_nat_stream_prop s
n, k: nat
Hk: Str_nth k s = n
∨ Str_nth k s < n < Str_nth (S k) s
l: hd s ≤ S n
n0: Str_nth (S k) s ≠ S n
Str_nth k s < Str_nth (S k) s
    by apply (Hs k (S k)); lia.
Qed.

Definition monotone_nat_stream :=
  {s : Stream nat | monotone_nat_stream_prop s}.

Lemma monotone_nat_stream_tl
  (s : Stream nat)
  (Hs : monotone_nat_stream_prop s)
  : monotone_nat_stream_prop (tl s).s: Stream nat
Hs: monotone_nat_stream_prop s
monotone_nat_stream_prop (tl s)
Proof.s: Stream nat
Hs: monotone_nat_stream_prop s
monotone_nat_stream_prop (tl s)
  by intros n1 n2; etransitivity; [| by apply (Hs (S n1) (S n2))]; lia.
Qed.

The stream of all natural numbers greater than or equal to n.

CoFixpoint nat_sequence_from (n : nat) : Stream nat
  := Cons n (nat_sequence_from (S n)).

The stream of all natural numbers.

Definition nat_sequence : Stream nat := nat_sequence_from 0.

Lemma nat_sequence_from_nth : forall m n, Str_nth n (nat_sequence_from m) = n + m.∀ m n : nat, Str_nth n (nat_sequence_from m) = n + m
Proof.∀ m n : nat, Str_nth n (nat_sequence_from m) = n + m
  intros m n; revert m.n: nat
∀ m : nat, Str_nth n (nat_sequence_from m) = n + m
  induction n; cbn; intros; [done |].n: nat
IHn: ∀ m : nat, Str_nth n (nat_sequence_from m) = n + m
m: nat
Str_nth (S n) (nat_sequence_from m) = S (n + m)
  by unfold Str_nth in IHn |- *; cbn; rewrite IHn; lia.
Qed.

Lemma nat_sequence_nth : forall n, Str_nth n nat_sequence = n.∀ n : nat, Str_nth n nat_sequence = n
Proof.∀ n : nat, Str_nth n nat_sequence = n
  by intros; unfold nat_sequence; rewrite nat_sequence_from_nth; lia.
Qed.

Lemma nat_sequence_from_sorted : forall n, ForAll2 lt (nat_sequence_from n).∀ n : nat, ForAll2 lt (nat_sequence_from n)
Proof.∀ n : nat, ForAll2 lt (nat_sequence_from n)
  intro n; apply ForAll2_forall; intro m.n, m: nat
Str_nth m (nat_sequence_from n) <
Str_nth (S m) (nat_sequence_from n)
  by rewrite !nat_sequence_from_nth; lia.
Qed.

Definition nat_sequence_sorted : ForAll2 lt nat_sequence :=
  nat_sequence_from_sorted 0.

Lemma nat_sequence_from_prefix_sorted
  : forall m n, LocallySorted lt (stream_prefix (nat_sequence_from m) n).∀ m n : nat,
  LocallySorted lt
    (stream_prefix (nat_sequence_from m) n)
Proof.∀ m n : nat,
  LocallySorted lt
    (stream_prefix (nat_sequence_from m) n)
  by intros; apply LocallySorted_ForAll2, stream_prefix_ForAll2, nat_sequence_from_sorted.
Qed.

Definition nat_sequence_prefix_sorted
  : forall n, LocallySorted lt (stream_prefix nat_sequence n) :=
  nat_sequence_from_prefix_sorted 0.

Definition stream_subsequence
  {A : Type}
  (s : Stream A)
  (ns : Stream nat)
  : Stream A
  := Streams.map (fun k => Str_nth k s) ns.

Lemma stream_prefix_nth_last
  {A : Type}
  (l : Stream A)
  (n : nat)
  (_last : A)
  : List.last (stream_prefix l (S n)) _last = Str_nth n l.A: Type
l: Stream A
n: nat
_last: A
List.last (stream_prefix l (S n)) _last = Str_nth n l
Proof.A: Type
l: Stream A
n: nat
_last: A
List.last (stream_prefix l (S n)) _last = Str_nth n l
  specialize (nth_error_last n (stream_prefix l (S n))); intro Hlast.A: Type
l: Stream A
n: nat
_last: A
Hlast: S n = length (stream_prefix l (S n))
→ ∀ _last : A,
    nth_error (stream_prefix l (S n)) n =
    Some
      (List.last (stream_prefix l (S n)) _last)
List.last (stream_prefix l (S n)) _last = Str_nth n l
  specialize (stream_prefix_length l (S n)); intro Hpref_len.A: Type
l: Stream A
n: nat
_last: A
Hlast: S n = length (stream_prefix l (S n))
→ ∀ _last : A,
    nth_error (stream_prefix l (S n)) n =
    Some
      (List.last (stream_prefix l (S n)) _last)
Hpref_len: length (stream_prefix l (S n)) = S n
List.last (stream_prefix l (S n)) _last = Str_nth n l
  symmetry in Hpref_len.A: Type
l: Stream A
n: nat
_last: A
Hlast: S n = length (stream_prefix l (S n))
→ ∀ _last : A,
    nth_error (stream_prefix l (S n)) n =
    Some
      (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
List.last (stream_prefix l (S n)) _last = Str_nth n l
  specialize (Hlast Hpref_len _last).A: Type
l: Stream A
n: nat
_last: A
Hlast: nth_error (stream_prefix l (S n)) n =
Some (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
List.last (stream_prefix l (S n)) _last = Str_nth n l
  specialize (stream_prefix_nth l (S n) n); intro Hnth.A: Type
l: Stream A
n: nat
_last: A
Hlast: nth_error (stream_prefix l (S n)) n =
Some (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
Hnth: n < S n
→ nth_error (stream_prefix l (S n)) n =
  Some (Str_nth n l)
List.last (stream_prefix l (S n)) _last = Str_nth n l
  assert (Hlt : n < S n) by constructor.A: Type
l: Stream A
n: nat
_last: A
Hlast: nth_error (stream_prefix l (S n)) n =
Some (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
Hnth: n < S n
→ nth_error (stream_prefix l (S n)) n =
  Some (Str_nth n l)
Hlt: n < S n
List.last (stream_prefix l (S n)) _last = Str_nth n l
  specialize (Hnth Hlt).A: Type
l: Stream A
n: nat
_last: A
Hlast: nth_error (stream_prefix l (S n)) n =
Some (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
Hnth: nth_error (stream_prefix l (S n)) n =
Some (Str_nth n l)
Hlt: n < S n
List.last (stream_prefix l (S n)) _last = Str_nth n l
  rewrite Hnth in Hlast.A: Type
l: Stream A
n: nat
_last: A
Hlast: Some (Str_nth n l) =
Some (List.last (stream_prefix l (S n)) _last)
Hpref_len: S n = length (stream_prefix l (S n))
Hnth: nth_error (stream_prefix l (S n)) n =
Some (Str_nth n l)
Hlt: n < S n
List.last (stream_prefix l (S n)) _last = Str_nth n l
  by inversion Hlast.
Qed.

Section sec_infinitely_often.

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

Definition InfinitelyOften : Stream A -> Prop :=
  ForAll (Exists1 P).

Definition FinitelyMany : Stream A -> Prop :=
  Exists (ForAll1 (fun a => ~ P a)).

Definition FinitelyManyBound (s : Stream A) : Type :=
  { n : nat | ForAll1 (fun a => ~ P a) (Str_nth_tl n s)}.

Lemma FinitelyMany_from_bound
  : forall s, FinitelyManyBound s -> FinitelyMany s.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ s : Stream A, FinitelyManyBound s → FinitelyMany s
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ s : Stream A, FinitelyManyBound s → FinitelyMany s
  intros s [n Hn].A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
Hn: ForAll1 (λ a : A, ¬ P a) (Str_nth_tl n s)
FinitelyMany s
  apply Exists_Str_nth_tl.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
n: nat
Hn: ForAll1 (λ a : A, ¬ P a) (Str_nth_tl n s)
∃ n : nat, ForAll1 (λ a : A, ¬ P a) (Str_nth_tl n s)
  by exists n.
Qed.

Lemma InfinitelyOften_tl s
  : InfinitelyOften s -> InfinitelyOften (tl s).A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
InfinitelyOften s → InfinitelyOften (tl s)
Proof.A: Type
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
s: Stream A
InfinitelyOften s → InfinitelyOften (tl s) by inversion 1. Qed.

Definition InfinitelyOften_nth_tl
  : forall n s, InfinitelyOften s -> InfinitelyOften (Str_nth_tl n s)
  := (@ForAll_Str_nth_tl _ (Exists1 P)).

End sec_infinitely_often.

Lemma InfinitelyOften_impl [A : Type] (P Q : A -> Prop) (HPQ : forall a, P a -> Q a)
  : forall s, InfinitelyOften P s -> InfinitelyOften Q s.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A,
  InfinitelyOften P s → InfinitelyOften Q s
Proof.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A,
  InfinitelyOften P s → InfinitelyOften Q s
  unfold InfinitelyOften.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
  cofix IH.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
  intros [a s] H.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
a: A
s: Stream A
H: ForAll (Exists1 P) (Cons a s)
ForAll (Exists1 Q) (Cons a s)
  inversion H.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
a: A
s: Stream A
H: ForAll (Exists1 P) (Cons a s)
H0: Exists1 P (Cons a s)
H1: ForAll (Exists1 P) (tl (Cons a s))
ForAll (Exists1 Q) (Cons a s) simpl in H1.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
a: A
s: Stream A
H: ForAll (Exists1 P) (Cons a s)
H0: Exists1 P (Cons a s)
H1: ForAll (Exists1 P) s
ForAll (Exists1 Q) (Cons a s) apply IH in H1.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
a: A
s: Stream A
H: ForAll (Exists1 P) (Cons a s)
H0: Exists1 P (Cons a s)
H1: ForAll (Exists1 Q) s
ForAll (Exists1 Q) (Cons a s)
  constructor; [| done].A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
IH: ∀ s : Stream A,
  ForAll (Exists1 P) s → ForAll (Exists1 Q) s
a: A
s: Stream A
H: ForAll (Exists1 P) (Cons a s)
H0: Exists1 P (Cons a s)
H1: ForAll (Exists1 Q) s
Exists1 Q (Cons a s)
  by rewrite Exists1_exists in *; firstorder.
Qed.

Lemma FinitelyManyBound_impl_rev
 [A : Type] (P Q : A -> Prop) (HPQ : forall a, P a -> Q a)
 : forall s, FinitelyManyBound Q s -> FinitelyManyBound P s.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A,
  FinitelyManyBound Q s → FinitelyManyBound P s
Proof.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
∀ s : Stream A,
  FinitelyManyBound Q s → FinitelyManyBound P s
  intros s [n Hn].A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
s: Stream A
n: nat
Hn: ForAll1 (λ a : A, ¬ Q a) (Str_nth_tl n s)
FinitelyManyBound P s
  exists n.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
s: Stream A
n: nat
Hn: ForAll1 (λ a : A, ¬ Q a) (Str_nth_tl n s)
ForAll1 (λ a : A, ¬ P a) (Str_nth_tl n s)
  apply ForAll1_forall.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
s: Stream A
n: nat
Hn: ForAll1 (λ a : A, ¬ Q a) (Str_nth_tl n s)
∀ n0 : nat, ¬ P (Str_nth n0 (Str_nth_tl n s))
  rewrite ForAll1_forall in Hn.A: Type
P, Q: A → Prop
HPQ: ∀ a : A, P a → Q a
s: Stream A
n: nat
Hn: ∀ n0 : nat, ¬ Q (Str_nth n0 (Str_nth_tl n s))
∀ n0 : nat, ¬ P (Str_nth n0 (Str_nth_tl n s))
  by firstorder.
Qed.

Prepend a non-empty list to a stream.

Definition stream_prepend {A} (nel : ne_list A) (s : Stream A) : Stream A :=
  (cofix prepend (l : ne_list A) :=
    Cons (ne_list_hd l) (from_option prepend s (ne_list_tl l))) nel.

Concatenate a stream of non-empty lists.

CoFixpoint stream_concat {A} (s : Stream (ne_list A)) : Stream A :=
  stream_prepend (hd s) (stream_concat (tl s)).

Lemma stream_prepend_prefix {A} (nel : ne_list A) (s : Stream A) :
  stream_prefix (stream_prepend nel s) (ne_list_length nel) = ne_list_to_list nel.A: Type
nel: ne_list A
s: Stream A
stream_prefix (stream_prepend nel s)
  (ne_list_length nel) = ne_list_to_list nel
Proof.A: Type
nel: ne_list A
s: Stream A
stream_prefix (stream_prepend nel s)
  (ne_list_length nel) = ne_list_to_list nel
  by induction nel; [| cbn; f_equal].
Qed.

Lemma stream_prepend_prefix_l
  {A : Type}
  (l : ne_list A)
  (s : Stream A)
  : forall n : nat, n <= ne_list_length l ->
    stream_prefix (stream_prepend l s) n = take n (ne_list_to_list l).A: Type
l: ne_list A
s: Stream A
∀ n : nat,
  n ≤ ne_list_length l
  → stream_prefix (stream_prepend l s) n =
    take n (ne_list_to_list l)
Proof.A: Type
l: ne_list A
s: Stream A
∀ n : nat,
  n ≤ ne_list_length l
  → stream_prefix (stream_prepend l s) n =
    take n (ne_list_to_list l)
  induction l; intros [| n] Hle; cbn; [done | | done |].A: Type
a: A
s: Stream A
n: nat
Hle: S n ≤ ne_list_length (nel_singl a)
a :: stream_prefix s n = a :: take n []
A: Type
a: A
l: ne_list A
s: Stream A
IHl: ∀ n : nat,
n ≤ ne_list_length l
→ stream_prefix (stream_prepend l s) n = take n (ne_list_to_list l)
n: nat
Hle: S n ≤ ne_list_length (a ::: l)
a
:: stream_prefix
     ((cofix prepend (l : ne_list A) : Stream A :=
         Cons (ne_list_hd l)
           (from_option prepend s (ne_list_tl l))) l)
     n =
a
:: take n
     ((fix fold (l : ne_list A) : list A :=
         match l with
         | nel_singl a => [a]
         | a ::: tl => a :: fold tl
         end) l)
  -A: Type
a: A
s: Stream A
n: nat
Hle: S n ≤ ne_list_length (nel_singl a)
a :: stream_prefix s n = a :: take n [] by cbn in Hle; replace n with 0 by lia.
  -A: Type
a: A
l: ne_list A
s: Stream A
IHl: ∀ n : nat,
n ≤ ne_list_length l
→ stream_prefix (stream_prepend l s) n = take n (ne_list_to_list l)
n: nat
Hle: S n ≤ ne_list_length (a ::: l)
a
:: stream_prefix
     ((cofix prepend (l : ne_list A) : Stream A :=
         Cons (ne_list_hd l)
           (from_option prepend s (ne_list_tl l))) l)
     n =
a
:: take n
     ((fix fold (l : ne_list A) : list A :=
         match l with
         | nel_singl a => [a]
         | a ::: tl => a :: fold tl
         end) l) by cbn in *; rewrite IHl; [| cbv in *; lia].
Qed.

Lemma stream_prepend_prefix_r
  {A : Type}
  (n : nat)
  : forall l : ne_list A, n >= ne_list_length l ->
    forall (s : Stream A),
      stream_prefix (stream_prepend l s) n
        =
      ne_list_to_list l ++ stream_prefix s (n - ne_list_length l).A: Type
n: nat
∀ l : ne_list A,
  n ≥ ne_list_length l
  → ∀ s : Stream A,
      stream_prefix (stream_prepend l s) n =
      ne_list_to_list l ++
      stream_prefix s (n - ne_list_length l)
Proof.A: Type
n: nat
∀ l : ne_list A,
  n ≥ ne_list_length l
  → ∀ s : Stream A,
      stream_prefix (stream_prepend l s) n =
      ne_list_to_list l ++
      stream_prefix s (n - ne_list_length l)
  induction n; intros [| a l] Hge s; cbn in *; [by lia.. | |].A: Type
n: nat
IHn: ∀ l : ne_list A,
n ≥ ne_list_length l
→ ∀ s : Stream A,
stream_prefix (stream_prepend l s) n =
ne_list_to_list l ++ stream_prefix s (n - ne_list_length l)
a: A
Hge: S n ≥ 1
s: Stream A
a :: stream_prefix s n = a :: stream_prefix s (n - 0)
A: Type
n: nat
IHn: ∀ l : ne_list A,
n ≥ ne_list_length l
→ ∀ s : Stream A,
stream_prefix (stream_prepend l s) n =
ne_list_to_list l ++ stream_prefix s (n - ne_list_length l)
a: A
l: ne_list A
Hge: S n
≥ S
(length
((fix fold (l : ne_list A) : list A :=
match l with
| nel_singl a => [a]
| a ::: tl => a :: fold tl
end) l))
s: Stream A
a
:: stream_prefix
     ((cofix prepend (l : ne_list A) : Stream A :=
         Cons (ne_list_hd l)
           (from_option prepend s (ne_list_tl l))) l)
     n =
a
:: (fix fold (l : ne_list A) : list A :=
      match l with
      | nel_singl a => [a]
      | a ::: tl => a :: fold tl
      end) l ++
   stream_prefix s
     (n -
      length
        ((fix fold (l : ne_list A) : list A :=
            match l with
            | nel_singl a => [a]
            | a ::: tl => a :: fold tl
            end) l))
  -A: Type
n: nat
IHn: ∀ l : ne_list A,
n ≥ ne_list_length l
→ ∀ s : Stream A,
stream_prefix (stream_prepend l s) n =
ne_list_to_list l ++ stream_prefix s (n - ne_list_length l)
a: A
Hge: S n ≥ 1
s: Stream A
a :: stream_prefix s n = a :: stream_prefix s (n - 0) by rewrite Nat.sub_0_r.
  -A: Type
n: nat
IHn: ∀ l : ne_list A,
n ≥ ne_list_length l
→ ∀ s : Stream A,
stream_prefix (stream_prepend l s) n =
ne_list_to_list l ++ stream_prefix s (n - ne_list_length l)
a: A
l: ne_list A
Hge: S n
≥ S
(length
((fix fold (l : ne_list A) : list A :=
match l with
| nel_singl a => [a]
| a ::: tl => a :: fold tl
end) l))
s: Stream A
a
:: stream_prefix
     ((cofix prepend (l : ne_list A) : Stream A :=
         Cons (ne_list_hd l)
           (from_option prepend s (ne_list_tl l))) l)
     n =
a
:: (fix fold (l : ne_list A) : list A :=
      match l with
      | nel_singl a => [a]
      | a ::: tl => a :: fold tl
      end) l ++
   stream_prefix s
     (n -
      length
        ((fix fold (l : ne_list A) : list A :=
            match l with
            | nel_singl a => [a]
            | a ::: tl => a :: fold tl
            end) l)) by rewrite <- IHn; [| cbv in *; lia].
Qed.

Lemma stream_concat_unroll {A} (a : ne_list A) (s : Stream (ne_list A)) :
  stream_concat (Cons a s) = stream_prepend a (stream_concat s).A: Type
a: ne_list A
s: Stream (ne_list A)
stream_concat (Cons a s) =
stream_prepend a (stream_concat s)
Proof.A: Type
a: ne_list A
s: Stream (ne_list A)
stream_concat (Cons a s) =
stream_prepend a (stream_concat s) by apply stream_eq_hd_tl. Qed.

Lemma stream_concat_prefix {A} (s : Stream (ne_list A)) n len
  (prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)))
  : len = length prefix ->
    stream_prefix (stream_concat s) len = prefix.A: Type
s: Stream (ne_list A)
n, len: nat
prefix:= mjoin
  (List.map ne_list_to_list
     (stream_prefix s n)): list A
len = length prefix
→ stream_prefix (stream_concat s) len = prefix
Proof.A: Type
s: Stream (ne_list A)
n, len: nat
prefix:= mjoin
  (List.map ne_list_to_list
     (stream_prefix s n)): list A
len = length prefix
→ stream_prefix (stream_concat s) len = prefix
  intros ->; revert s prefix.A: Type
n: nat
∀ s : Stream (ne_list A),
  let prefix :=
    mjoin
      (List.map ne_list_to_list (stream_prefix s n))
    in
  stream_prefix (stream_concat s) (length prefix) =
  prefix
  induction n; [done |].A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
∀ s : Stream (ne_list A),
  let prefix :=
    mjoin
      (List.map ne_list_to_list
         (stream_prefix s (S n))) in
  stream_prefix (stream_concat s) (length prefix) =
  prefix
  intros [n0 s]; cbn.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
stream_prefix (stream_concat (Cons n0 s))
  (length
     (ne_list_to_list n0 ++
      mjoin
        (List.map ne_list_to_list (stream_prefix s n)))) =
ne_list_to_list n0 ++
mjoin (List.map ne_list_to_list (stream_prefix s n))
  rewrite app_length.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
stream_prefix (stream_concat (Cons n0 s))
  (length (ne_list_to_list n0) +
   length
     (mjoin
        (List.map ne_list_to_list (stream_prefix s n)))) =
ne_list_to_list n0 ++
mjoin (List.map ne_list_to_list (stream_prefix s n))
  assert (Hge :
    length (ne_list_to_list n0) + length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
    ≥ length (ne_list_to_list n0)) by lia.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
Hge: length (ne_list_to_list n0) +
length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
≥ length (ne_list_to_list n0)
stream_prefix (stream_concat (Cons n0 s))
  (length (ne_list_to_list n0) +
   length
     (mjoin
        (List.map ne_list_to_list (stream_prefix s n)))) =
ne_list_to_list n0 ++
mjoin (List.map ne_list_to_list (stream_prefix s n))
  rewrite stream_concat_unroll, stream_prepend_prefix_r by done.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
Hge: length (ne_list_to_list n0) +
length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
≥ length (ne_list_to_list n0)
ne_list_to_list n0 ++
stream_prefix (stream_concat s)
  (length (ne_list_to_list n0) +
   length
     (mjoin
        (List.map ne_list_to_list (stream_prefix s n))) -
   ne_list_length n0) =
ne_list_to_list n0 ++
mjoin (List.map ne_list_to_list (stream_prefix s n))
  rewrite <- IHn at 2.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
Hge: length (ne_list_to_list n0) +
length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
≥ length (ne_list_to_list n0)
ne_list_to_list n0 ++
stream_prefix (stream_concat s)
  (length (ne_list_to_list n0) +
   length
     (mjoin
        (List.map ne_list_to_list (stream_prefix s n))) -
   ne_list_length n0) =
ne_list_to_list n0 ++
stream_prefix (stream_concat s)
  (length
     (mjoin
        (List.map ne_list_to_list (stream_prefix s n))))
  do 2 f_equal.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
Hge: length (ne_list_to_list n0) +
length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
≥ length (ne_list_to_list n0)
length (ne_list_to_list n0) +
length
  (mjoin
     (List.map ne_list_to_list (stream_prefix s n))) -
ne_list_length n0 =
length
  (mjoin
     (List.map ne_list_to_list (stream_prefix s n)))
  rewrite Nat.add_comm.A: Type
n: nat
IHn: ∀ s : Stream (ne_list A),
let prefix := mjoin (List.map ne_list_to_list (stream_prefix s n)) in
stream_prefix (stream_concat s) (length prefix) = prefix
n0: ne_list A
s: Stream (ne_list A)
Hge: length (ne_list_to_list n0) +
length (mjoin (List.map ne_list_to_list (stream_prefix s n)))
≥ length (ne_list_to_list n0)
length
  (mjoin
     (List.map ne_list_to_list (stream_prefix s n))) +
length (ne_list_to_list n0) - ne_list_length n0 =
length
  (mjoin
     (List.map ne_list_to_list (stream_prefix s n)))
  by apply Nat.add_sub.
Qed.

Section sec_temporal.

Definition progress [A : Type] (R : A -> A -> Prop) : Stream A -> Prop :=
  ForAll (fun s => let x := hd s in let a := hd (tl s) in a = x \/ R a x).

Lemma refutation :
  forall [A : Type] [R : A -> A-> Prop] (HR : well_founded R) [s : Stream A],
    ~ ForAll (fun s => Exists (fun x => R (hd x) (hd s)) s) s.∀ (A : Type) (R : A → A → Prop),
  wf R
  → ∀ s : Stream A,
      ¬ ForAll
          (λ s0 : Stream A,
             Exists (λ x : Stream A, R (hd x) (hd s0))
               s0) s
Proof.∀ (A : Type) (R : A → A → Prop),
  wf R
  → ∀ s : Stream A,
      ¬ ForAll
          (λ s0 : Stream A,
             Exists (λ x : Stream A, R (hd x) (hd s0))
               s0) s
  intros A R HR [h t]; revert t.A: Type
R: A → A → Prop
HR: wf R
h: A
∀ t : Stream A,
  ¬ ForAll
      (λ s : Stream A,
         Exists (λ x : Stream A, R (hd x) (hd s)) s)
      (Cons h t)
  specialize (HR h).A: Type
R: A → A → Prop
h: A
HR: Acc R h
∀ t : Stream A,
  ¬ ForAll
      (λ s : Stream A,
         Exists (λ x : Stream A, R (hd x) (hd s)) s)
      (Cons h t)
  induction HR as [h' _ IH].A: Type
R: A → A → Prop
h': A
IH: ∀ y : A,
  R y h'
  → ∀ t : Stream A,
      ¬ ForAll
          (λ s : Stream A,
             Exists
               (λ x : Stream A, R (hd x) (hd s))
               s) (Cons y t)
∀ t : Stream A,
  ¬ ForAll
      (λ s : Stream A,
         Exists (λ x : Stream A, R (hd x) (hd s)) s)
      (Cons h' t)
  intros t HF.A: Type
R: A → A → Prop
h': A
IH: ∀ y : A,
  R y h'
  → ∀ t : Stream A,
      ¬ ForAll
          (λ s : Stream A,
             Exists
               (λ x : Stream A, R (hd x) (hd s))
               s) (Cons y t)
t: Stream A
HF: ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (Cons h' t)
False
  destruct (id HF).A: Type
R: A → A → Prop
h': A
IH: ∀ y : A,
  R y h'
  → ∀ t : Stream A,
      ¬ ForAll
          (λ s : Stream A,
             Exists
               (λ x : Stream A, R (hd x) (hd s))
               s) (Cons y t)
t: Stream A
HF: ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (Cons h' t)
H: Exists (λ x : Stream A, R (hd x) (hd (Cons h' t)))
  (Cons h' t)
f: ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (tl (Cons h' t))
False
  destruct (use_Exists _ _ _ H HF) as [[a' s'] [Ha' H1']].A: Type
R: A → A → Prop
h': A
IH: ∀ y : A,
  R y h'
  → ∀ t : Stream A,
      ¬ ForAll
          (λ s : Stream A,
             Exists
               (λ x : Stream A, R (hd x) (hd s))
               s) (Cons y t)
t: Stream A
HF: ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (Cons h' t)
H: Exists (λ x : Stream A, R (hd x) (hd (Cons h' t)))
  (Cons h' t)
f: ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (tl (Cons h' t))
a': A
s': Stream A
Ha': R (hd (Cons a' s')) (hd (Cons h' t))
H1': ForAll (λ s : Stream A, Exists (λ x : Stream A, R (hd x) (hd s)) s)
(Cons a' s')
False
  by eapply IH; eauto.
Qed.

Lemma progress_Exists_neq :
  forall [A : Type] [R : A -> A -> Prop] (s : Stream A),
    progress R s -> ForAll (Exists (fun s' => hd s' <> hd s)) s ->
      Exists (fun s' => R (hd s') (hd s)) s.∀ (A : Type) (R : A → A → Prop) (s : Stream A),
  progress R s
  → ForAll (Exists (λ s' : Stream A, hd s' ≠ hd s)) s
    → Exists (λ s' : Stream A, R (hd s') (hd s)) s
Proof.∀ (A : Type) (R : A → A → Prop) (s : Stream A),
  progress R s
  → ForAll (Exists (λ s' : Stream A, hd s' ≠ hd s)) s
    → Exists (λ s' : Stream A, R (hd s') (hd s)) s
  intros A R [a s] Hprogress Hex; cbn.A: Type
R: A → A → Prop
a: A
s: Stream A
Hprogress: progress R (Cons a s)
Hex: ForAll
  (Exists
     (λ s' : Stream A, hd s' ≠ hd (Cons a s)))
  (Cons a s)
Exists (λ s' : Stream A, R (hd s') a) (Cons a s)
  generalize (eq_refl : hd (Cons a s) = a).A: Type
R: A → A → Prop
a: A
s: Stream A
Hprogress: progress R (Cons a s)
Hex: ForAll
  (Exists
     (λ s' : Stream A, hd s' ≠ hd (Cons a s)))
  (Cons a s)
hd (Cons a s) = a
→ Exists (λ s' : Stream A, R (hd s') a) (Cons a s)
  destruct Hex as [Hex _].A: Type
R: A → A → Prop
a: A
s: Stream A
Hprogress: progress R (Cons a s)
Hex: Exists (λ s' : Stream A, hd s' ≠ hd (Cons a s))
  (Cons a s)
hd (Cons a s) = a
→ Exists (λ s' : Stream A, R (hd s') a) (Cons a s)
  revert Hprogress; induction Hex; intros Hprogress <-; [by cbn in H; congruence |].A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists
  (λ s' : Stream A, hd s' ≠ hd (Cons (hd x) s))
  (tl x)
Hprogress: progress R x
Exists (λ s' : Stream A, R (hd s') (hd x)) x
  constructor 2.A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists
  (λ s' : Stream A, hd s' ≠ hd (Cons (hd x) s))
  (tl x)
Hprogress: progress R x
Exists (λ s' : Stream A, R (hd s') (hd x)) (tl x)
  inversion Hprogress as [[] ?]; cbn in *.A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists (λ s' : Stream A, hd s' ≠ hd x) (tl x)
Hprogress: progress R x
H: hd (tl x) = hd x
H0: ForAll
  (λ s : Stream A,
     hd (tl s) = hd s ∨ R (hd (tl s)) (hd s))
  (tl x)
Exists (λ s' : Stream A, R (hd s') (hd x)) (tl x)
A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists (λ s' : Stream A, hd s' ≠ hd x) (tl x)
Hprogress: progress R x
H: R (hd (tl x)) (hd x)
H0: ForAll
  (λ s : Stream A,
     hd (tl s) = hd s ∨ R (hd (tl s)) (hd s))
  (tl x)
Exists (λ s' : Stream A, R (hd s') (hd x)) (tl x)
  -A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists (λ s' : Stream A, hd s' ≠ hd x) (tl x)
Hprogress: progress R x
H: hd (tl x) = hd x
H0: ForAll
  (λ s : Stream A,
     hd (tl s) = hd s ∨ R (hd (tl s)) (hd s))
  (tl x)
Exists (λ s' : Stream A, R (hd s') (hd x)) (tl x) by apply IHHex.
  -A: Type
R: A → A → Prop
s, x: Stream A
IHHex: progress R (tl x)
→ hd (tl x) = hd x
  → Exists (λ s' : Stream A, R (hd s') (hd x))
      (tl x)
Hex: Exists (λ s' : Stream A, hd s' ≠ hd x) (tl x)
Hprogress: progress R x
H: R (hd (tl x)) (hd x)
H0: ForAll
  (λ s : Stream A,
     hd (tl s) = hd s ∨ R (hd (tl s)) (hd s))
  (tl x)
Exists (λ s' : Stream A, R (hd s') (hd x)) (tl x) by constructor.
Qed.

Lemma stabilization :
  forall [A : Type] [R : A -> A-> Prop] (HR : well_founded R) [s : Stream A],
    progress R s -> exists x : A, Exists (ForAll (fun s => hd s = x)) s.∀ (A : Type) (R : A → A → Prop),
  wf R
  → ∀ s : Stream A,
      progress R s
      → ∃ x : A,
          Exists (ForAll (λ s0 : Stream A, hd s0 = x))
            s
Proof.∀ (A : Type) (R : A → A → Prop),
  wf R
  → ∀ s : Stream A,
      progress R s
      → ∃ x : A,
          Exists (ForAll (λ s0 : Stream A, hd s0 = x))
            s
  intros A R HR s Hprogress.A: Type
R: A → A → Prop
HR: wf R
s: Stream A
Hprogress: progress R s
∃ x : A, Exists (ForAll (λ s : Stream A, hd s = x)) s
  apply Classical_Prop.NNPP; intros Hnex.A: Type
R: A → A → Prop
HR: wf R
s: Stream A
Hprogress: progress R s
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
False
  assert (H : forall x : A, ForAll (Exists (fun s => hd s <> x)) s)
    by (apply not_Exists_ForAll; done).A: Type
R: A → A → Prop
HR: wf R
s: Stream A
Hprogress: progress R s
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
False
  apply (@refutation _ _ HR s).A: Type
R: A → A → Prop
HR: wf R
s: Stream A
Hprogress: progress R s
Hnex: ¬ (∃ x : A,
     Exists (ForAll (λ s : Stream A, hd s = x))
       s)
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s) s
  clear Hnex; revert s Hprogress H.A: Type
R: A → A → Prop
HR: wf R
∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists (λ x : Stream A, R (hd x) (hd s0))
             s0) s
  cofix CH.A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists (λ x : Stream A, R (hd x) (hd s0))
             s0) s
  constructor.A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
Exists (λ x : Stream A, R (hd x) (hd s)) s
A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (tl s)
  -A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
Exists (λ x : Stream A, R (hd x) (hd s)) s by apply progress_Exists_neq.
  -A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
ForAll
  (λ s : Stream A,
     Exists (λ x : Stream A, R (hd x) (hd s)) s)
  (tl s) apply CH.A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
progress R (tl s)
A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) (tl s)
    +A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
progress R (tl s) by apply Hprogress.
    +A: Type
R: A → A → Prop
HR: wf R
CH: ∀ s : Stream A,
  progress R s
  → (∀ x : A,
       ForAll
         (Exists (λ s0 : Stream A, hd s0 ≠ x)) s)
    → ForAll
        (λ s0 : Stream A,
           Exists
             (λ x : Stream A, R (hd x) (hd s0))
             s0) s
s: Stream A
Hprogress: progress R s
H: ∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) s
∀ x : A,
  ForAll (Exists (λ s : Stream A, hd s ≠ x)) (tl s) by apply H.
Qed.

End sec_temporal.