Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Logic.Classical.
Require Export Coq.Logic.Classical_Prop.
Require Export Coq.Logic.FunctionalExtensionality.
Require Export Coq.Classes.Equivalence.
Require Export Coq.Classes.Morphisms.
Require Import Logic.lib.Coqlib.
Require Import Logic.lib.NatChoice.

Definition stream (A: Type): Type := {h: nat -> option A | forall x y, x < y -> h x = None -> h y = None}.

Definition stream_get {A: Type} (h: stream A) (n: nat) := proj1_sig h n.

Coercion stream_get: stream >-> Funclass.

Lemma stream_sound1: forall {A: Type} (h: stream A) (x y: nat), x <= y -> h x = None -> h y = None.
Proof.
(* Goal: forall (A : Type) (h : stream A) (x y : nat) (_ : le x y) (_ : @eq (option A) (@stream_get A h x) (@None A)), @eq (option A) (@stream_get A h y) (@None A) *)
  intros ? [h ?] ? ? ?.
(* Goal: forall _ : @eq (option A) (@stream_get A (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h e) x) (@None A), @eq (option A) (@stream_get A (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h e) y) (@None A) *)
  destruct H; auto; simpl.
(* Goal: forall _ : @eq (option A) (h x) (@None A), @eq (option A) (h (S m)) (@None A) *)
  apply (e x (S m)).
(* Goal: le n (S n) *)
  omega.
Qed.

Lemma stream_sound2: forall {A: Type} (h: stream A) (x y: nat), x <= y -> (exists a, h y = Some a) -> (exists a, h x = Some a).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: @ex A (fun a : A => @eq (option A) (@stream_get A h x) (@Some A a)) *)
  pose proof stream_sound1 h x y H.
(* Goal: @ex A (fun a : A => @eq (option A) (@stream_get A h x) (@Some A a)) *)
  destruct (h x), (h y), H0; eauto.
(* Goal: @ex A (fun a : A => @eq (option A) (@None A) (@Some A a)) *)
  specialize (H1 eq_refl).
(* Goal: False *)
  congruence.
Qed.

Lemma stream_extensionality {A: Type}: forall h1 h2: stream A, (forall n, h1 n = h2 n) -> h1 = h2.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: @eq (stream A) h1 h2 *)
  destruct h1 as [h1 ?H], h2 as [h2 ?H]; simpl in *.
(* Goal: @eq (stream A) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H0) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h2 H1) *)
  assert (h1 = h2) by (extensionality n; auto).
(* Goal: @eq (stream A) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H0) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h2 H1) *)
  subst h2.
(* Goal: @eq (stream A) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H0) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H1) *)
  assert (H0 = H1) by (apply proof_irrelevance).
(* Goal: @eq (stream A) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H0) (@exist (forall _ : nat, option A) (fun h : forall _ : nat, option A => forall (x y : nat) (_ : lt x y) (_ : @eq (option A) (h x) (@None A)), @eq (option A) (h y) (@None A)) h1 H1) *)
  subst H1.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  auto.
Qed.

Tactic Notation "stream_extensionality" ident(x) :=
  match goal with
    [ |- ?X = ?Y ] =>
     apply stream_extensionality; intro x
  end.

Definition is_n_stream {A: Type} (n: nat) (h: stream A): Prop :=
  h n = None /\ forall n', n' < n -> h n' <> None.

Definition is_fin_stream {A: Type} (h: stream A): Prop :=
  exists n, h n = None.

Definition is_inf_stream {A: Type} (h: stream A): Prop :=
  forall n, h n <> None.

Definition is_at_least_n_stream {A: Type} (n: nat) (h: stream A): Prop :=
  forall n', n' < n -> h n' <> None.

Definition is_at_most_n_stream {A: Type} (n: nat) (h: stream A): Prop :=
  h n = None.

Definition is_empty_stream {A: Type}: stream A -> Prop :=
  is_n_stream 0.

Lemma n_stream_inf_stream_conflict {A: Type}: forall (h: stream A) (n: nat),
  is_n_stream n h ->
  is_inf_stream h ->
  False.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: False *)
  destruct H.
(* Goal: False *)
  exact (H0 _ H).
Qed.

Lemma is_n_stream_pf {A: Type}: forall (h: stream A) (n m: nat),
  is_n_stream m h ->
  is_n_stream n h ->
  n = m.
Proof.
  intros ?.
  assert (forall n m, n < m -> is_n_stream m h -> is_n_stream n h -> False).
  Focus 1. {
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
    intros.
    destruct H0, H1.
    specialize (H2 n H).
(* Goal: False *)
    congruence.
  } Unfocus.
  intros; destruct (lt_eq_lt_dec n m) as [[?H | ?H] | ?H].
  + specialize (H _ _ H2 H0 H1); contradiction.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + auto.
  + specialize (H _ _ H2 H1 H0); contradiction.
Qed.

Lemma at_most_n_stream_Sn {A: Type}: forall (h: stream A) (n: nat),
  is_at_most_n_stream (S n) h <->
  is_at_most_n_stream n h \/ is_n_stream (S n) h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_at_most_n_stream A (S n) h) (or (@is_at_most_n_stream A n h) (@is_n_stream A (S n) h)) *)
  split; [intro | intros [? | ?]].
  + destruct (h n) eqn:?H.
    - right.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      split; auto.
(* Goal: forall (n' : nat) (_ : lt n' (S n)), not (@eq (option A) (@stream_get A h n') (@None A)) *)
      intros; intro.
(* Goal: False *)
      rewrite (stream_sound1 h n' n) in H0 by (auto; omega).
(* Goal: False *)
      congruence.
    - left.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      auto.
  + hnf in H |- *.
(* Goal: @eq (option A) (@stream_get A h (S n)) (@None A) *)
    rewrite (stream_sound1 h n (S n)) by (auto; omega).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + destruct H; auto.
Qed.

Lemma at_most_n_stream_0 {A: Type}: forall (h: stream A),
  is_at_most_n_stream 0 h <-> is_n_stream 0 h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros; split; intros.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + split; auto.
(* Goal: le n (S n) *)
    intros; omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + destruct H; auto.
Qed.

Lemma at_most_n_stream_spec {A: Type}: forall (h: stream A) (n: nat),
  is_at_most_n_stream n h <->
  exists m, m <= n /\ is_n_stream m h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_at_least_n_stream A n h) (or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h)) *)
  induction n.
  + rewrite at_most_n_stream_0.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
    split; intros.
    - exists 0; split; [omega | auto].
    - destruct H as [m [? ?]].
(* Goal: le n (S n) *)
      replace m with 0 in H0 by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      auto.
  + rewrite at_most_n_stream_Sn.
(* Goal: iff (and (@is_at_least_n_stream A n h) (not (@is_n_stream A n h))) (or (@ex nat (fun m : nat => and (ge m (S n)) (@is_n_stream A m h))) (@is_inf_stream A h)) *)
    rewrite IHn.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
    split; intros.
    - destruct H as [[m [? ?]] | ?].
      * exists m; split; [omega | auto].
      * exists (S n); split; [omega | auto].
    - destruct H as [m [? ?]].
(* Goal: or (@ex nat (fun m : nat => and (le m n) (@is_n_stream A m h))) (@is_n_stream A (S n) h) *)
      destruct (le_gt_dec m n).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      * left; exists m; split; auto.
(* Goal: or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
      * right.
(* Goal: le n (S n) *)
        replace (S n) with m by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
        auto.
Qed.

Lemma is_fin_stream_spec {A}: forall (h: stream A),
  is_fin_stream h <-> exists n, is_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_inf_stream A h) (forall n : nat, not (@is_n_stream A n h)) *)
  split; intro.
  + destruct H as [n ?].
(* Goal: @ex nat (fun n : nat => @is_n_stream A n h) *)
    apply at_most_n_stream_spec in H.
(* Goal: @ex nat (fun n : nat => @is_n_stream A n h) *)
    destruct H as [m [? ?]].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    exists m; auto.
  + destruct H as [n [? ?]].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    exists n; auto.
Qed.

Lemma at_most_n_stream_mono {A: Type}: forall (h: stream A) (n m: nat),
  n <= m ->
  is_at_most_n_stream n h ->
  is_at_most_n_stream m h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  rewrite at_most_n_stream_spec in H0 |- *.
(* Goal: @ex nat (fun m0 : nat => and (le m0 m) (@is_n_stream A m0 h)) *)
  destruct H0 as [m0 [? ?]].
(* Goal: @ex nat (fun m0 : nat => and (le m0 m) (@is_n_stream A m0 h)) *)
  exists m0.
(* Goal: and (ge m0 n) (@is_n_stream A m0 h) *)
  split; [omega | auto].
Qed.

Lemma at_most_n_stream_is_fin_stream {A: Type}: forall (h: stream A) (n: nat),
  is_at_most_n_stream n h ->
  is_fin_stream h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: @is_fin_stream A h *)
  rewrite at_most_n_stream_spec in H.
(* Goal: @is_fin_stream A h *)
  rewrite is_fin_stream_spec.
(* Goal: @ex nat (fun n : nat => @is_n_stream A n h) *)
  destruct H as [m [? ?]].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  exists m; auto.
Qed.

Lemma n_stream_or_inf_stream {A: Type}: forall (h: stream A),
  (exists n, is_n_stream n h) \/ is_inf_stream h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: or (@ex nat (fun n : nat => @is_n_stream A n h)) (@is_inf_stream A h) *)
  destruct (classic (is_fin_stream h)).
  + left.
(* Goal: @ex nat (fun n : nat => @is_n_stream A n h) *)
    rewrite is_fin_stream_spec in H.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
  + right.
(* Goal: forall (n' : nat) (_ : lt n' (S n)), not (@eq (option A) (@stream_get A h n') (@None A)) *)
    hnf; intros; intro.
(* Goal: False *)
    apply H; clear H.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    exists n; auto.
Qed.

Lemma at_least_n_stream_Sn {A: Type}: forall (h: stream A) (n: nat),
  is_at_least_n_stream (S n) h <->
  is_at_least_n_stream n h /\ ~ is_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_at_least_n_stream A (S n) h) (and (@is_at_least_n_stream A n h) (not (@is_n_stream A n h))) *)
  split; [intro | intros [? ?]].
  + split.
    - hnf in H |- *.
(* Goal: le n (S n) *)
      intros; apply H; omega.
    - intros [? ?].
(* Goal: False *)
      exact (H n (le_n _) H0).
  + hnf in H |- *.
(* Goal: forall (n' : nat) (_ : lt n' (S n)), not (@eq (option A) (@stream_get A h n') (@None A)) *)
    intros; intro.
(* Goal: False *)
    apply H0; clear H0.
(* Goal: and (or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h)) (not (@is_n_stream A n h)) *)
    split.
    - specialize ((fun HH => H n' HH H2): ~ n' < n).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      replace n with n' by omega; auto.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    - intros; apply H; auto.
Qed.

Lemma at_least_n_stream_0 {A: Type}: forall (h: stream A),
  is_at_least_n_stream 0 h <-> True.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  split; auto.
(* Goal: forall _ : True, @is_at_least_n_stream A O h *)
  intros _.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
(* Goal: le n (S n) *)
  omega.
Qed.

Lemma at_least_n_stream_spec {A: Type}: forall (h: stream A) (n: nat),
  is_at_least_n_stream n h <->
  (exists m, m >= n /\ is_n_stream m h) \/ is_inf_stream h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_at_least_n_stream A n h) (or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h)) *)
  induction n.
  + rewrite at_least_n_stream_0.
(* Goal: forall _ : True, @is_at_least_n_stream A O h *)
    split; auto; intros _.
(* Goal: or (@ex nat (fun m : nat => and (ge m O) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    destruct (n_stream_or_inf_stream h) as [[m ?] | ?].
    - left; exists m; split; [omega | auto].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    - right; auto.
  + rewrite at_least_n_stream_Sn.
(* Goal: iff (and (@is_at_least_n_stream A n h) (not (@is_n_stream A n h))) (or (@ex nat (fun m : nat => and (ge m (S n)) (@is_n_stream A m h))) (@is_inf_stream A h)) *)
    rewrite IHn.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
    split; intros.
    - destruct H as [[[m [? ?]] | ?] ?].
      * left; exists m; split; [| auto].
(* Goal: ge m (S n) *)
        destruct (Nat.eq_dec m n); [subst; tauto | omega].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      * right; auto.
    - destruct H as [[m [? ?]] | ?].
      * split.
       ++ left; exists m; split; [omega | auto].
       ++ intro.
(* Goal: False *)
          pose proof (is_n_stream_pf _ _ _ H0 H1).
(* Goal: le n (S n) *)
          omega.
      * split.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
       ++ right; auto.
       ++ intros [? ?].
(* Goal: False *)
          exact (H _ H0).
Qed.

Lemma is_inf_stream_spec {A}: forall (h: stream A),
  is_inf_stream h <-> forall n, ~ is_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: iff (@is_inf_stream A h) (forall n : nat, not (@is_n_stream A n h)) *)
  split; intro.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  + intros.
(* Goal: not (@is_n_stream A n h) *)
    intros [? ?].
(* Goal: False *)
    exact (H _ H0).
  + destruct (n_stream_or_inf_stream h) as [[m ?] | ?]; [| auto].
(* Goal: @is_inf_stream A h *)
    exfalso.
(* Goal: False *)
    exact (H _ H0).
Qed.

Lemma at_least_n_stream_mono {A: Type}: forall (h: stream A) (n m: nat),
  n <= m ->
  is_at_least_n_stream m h ->
  is_at_least_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  rewrite at_least_n_stream_spec in H0 |- *.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  destruct H0 as [[m0 [? ?]] | ?].
  + left; exists m0.
(* Goal: and (ge m0 n) (@is_n_stream A m0 h) *)
    split; [omega | auto].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + right; auto.
Qed.

Lemma inf_stream_is_at_least_n_stream_is_fin_stream {A: Type}: forall (h: stream A) (n: nat),
  is_inf_stream h ->
  is_at_least_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: @is_at_least_n_stream A (S n) h *)
  rewrite at_least_n_stream_spec.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  auto.
Qed.

Lemma at_most_n_stream_or_at_least_Sn_stream {A: Type}: forall (h: stream A) (n: nat),
  is_at_most_n_stream n h \/ is_at_least_n_stream (S n) h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A (S n) h) *)
  destruct (n_stream_or_inf_stream h) as [[m ?] | ?]; [destruct (lt_dec n m) |].
  + right.
(* Goal: @is_at_least_n_stream A (S n) h *)
    rewrite at_least_n_stream_spec.
(* Goal: or (@ex nat (fun m : nat => and (ge m (S n)) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    left; exists m.
(* Goal: and (le m n) (@is_n_stream A m h) *)
    split; [omega | tauto].
  + left.
(* Goal: @is_at_most_n_stream A n h *)
    rewrite at_most_n_stream_spec.
(* Goal: @ex nat (fun m : nat => and (le m n) (@is_n_stream A m h)) *)
    exists m.
(* Goal: and (le m n) (@is_n_stream A m h) *)
    split; [omega | tauto].
  + right.
(* Goal: @is_at_least_n_stream A (S n) h *)
    rewrite at_least_n_stream_spec.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    right; auto.
Qed.

Lemma at_most_n_stream_or_at_least_n_stream {A: Type}: forall (h: stream A) (n: nat),
  is_at_most_n_stream n h \/ is_at_least_n_stream n h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  destruct (at_most_n_stream_or_at_least_Sn_stream h n).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + left; auto.
  + right.
(* Goal: @is_at_least_n_stream A n h *)
    eapply at_least_n_stream_mono; [| eassumption].
(* Goal: le n (S n) *)
    omega.
Qed.

(*
Definition stream_coincide {A: Type} (n: nat) (h1 h2: stream A): Prop :=
  forall m, m < n -> h1 m = h2 m.

Definition stream_app {A: Type} (h1 h2 h: stream A): Prop :=
  exists n,
    h1 n = None /\
    stream_coincide n h1 h /\
    (forall m, h (m + n) = h2 m).

Definition prefix_stream {A: Type} (h1 h2: stream A): Prop :=
  forall n, h1 n = None \/ h1 n = h2 n.

Definition strict_prefix_stream {A: Type} (h1 h2: stream A): Prop :=
  prefix_stream h1 h2 /\ exists n, h1 n <> h2 n.

Definition n_bounded_prefix_stream {A: Type} (m: nat) (h1 h2: stream A): Prop :=
  forall n, (h1 n = None /\ h2 (n + m) = None) \/ h1 n = h2 n.

Lemma stream_coincide_sym {A: Type}: forall (h1 h2: stream A) n,
  stream_coincide n h1 h2 ->
  stream_coincide n h2 h1.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
(* Goal: False *)
  specialize (H m H0); congruence.
Qed.

Lemma stream_coincide_trans {A: Type}: forall (h1 h2 h3: stream A) n,
  stream_coincide n h1 h2 ->
  stream_coincide n h2 h3 ->
  stream_coincide n h1 h3.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
  specialize (H m H1);
(* Goal: False *)
  specialize (H0 m H1); congruence.
Qed.

Lemma stream_coincide_weaken {A: Type}: forall n m (h1 h2: stream A),
  n <= m ->
  stream_coincide m h1 h2 ->
  stream_coincide n h1 h2.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  intros n0 ?.
  apply H0.
(* Goal: le n (S n) *)
  omega.
Qed.

Lemma is_n_stream_None {A: Type}: forall n m (h: stream A), n <= m -> is_n_stream n h -> h m = None.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  destruct H0.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  apply (stream_sound1 h n m); auto.
Qed.

Lemma fstn_stream_coincide {A: Type}: forall n (h: stream A),
  stream_coincide n h (fstn_stream n h).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  intros m ?.
(* Goal: le n (S n) *)
  rewrite fstn_stream_Some by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  auto.
Qed.

Lemma prefix_stream_refl {A: Type}: forall (h: stream A), prefix_stream h h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  right; auto.
Qed.

Lemma prefix_stream_trans {A: Type}: forall (h1 h2 h3: stream A), prefix_stream h1 h2 -> prefix_stream h2 h3 -> prefix_stream h1 h3.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf in H, H0 |- *; intros.
  specialize (H n); specialize (H0 n).
  destruct H, H0.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + left; auto.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + left; auto.
(* Goal: False *)
  + left; congruence.
(* Goal: False *)
  + right; congruence.
Qed.

Lemma prefix_stream_anti_sym {A: Type}: forall (h1 h2: stream A), prefix_stream h1 h2 -> prefix_stream h2 h1 -> h1 = h2.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  stream_extensionality n.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
  specialize (H n); specialize (H0 n).
(* Goal: False *)
  destruct H, H0; congruence.
Qed.

Lemma prefix_stream_comparable {A: Type}: forall (h1 h2 h: stream A), prefix_stream h1 h -> prefix_stream h2 h -> prefix_stream h1 h2 \/ prefix_stream h2 h1.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  destruct (classic (exists n, h1 n <> h2 n /\ h1 n <> None)); [right | left].
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  + hnf; intros.
    destruct H1 as [m [? ?]].
    destruct (H0 n); [auto |].
    destruct (H n); [| right; congruence].
    assert (m < n).
    Focus 1. {
(* Goal: le n (S n) *)
      destruct (le_dec n m); try omega.
      exfalso; apply H2.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      eapply stream_sound1; eauto.
    } Unfocus.
    destruct (H m); [congruence |].
    destruct (H0 m); [| congruence].
(* Goal: or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A (S n) h) *)
    left.
(* Goal: le n (S n) *)
    apply stream_sound1 with m; auto. omega.
  + hnf; intros n.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    destruct (classic (h1 n = None)), (classic (h1 n = h2 n)); try tauto.
(* Goal: @is_inf_stream A h *)
    exfalso.
    apply H1.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    eexists; eauto.
Qed.

Lemma fstn_stream_finite {A: Type}: forall n (h: stream A), is_fin_stream (fstn_stream n h).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  exists n.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  rewrite fstn_stream_None; auto.
Qed.

Lemma fstn_stream_prefix {A: Type}: forall n (h: stream A), prefix_stream (fstn_stream n h) h.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  hnf; intros m.
  destruct (le_dec n m).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + rewrite fstn_stream_None; auto.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + rewrite fstn_stream_Some; auto.
(* Goal: le n (S n) *)
    omega.
Qed.

Lemma prefix_stream_coincide {A: Type}: forall n (h1 h2: stream A),
  prefix_stream h1 h2 ->
  is_at_least_n_stream n h1 ->
  stream_coincide n h1 h2.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
  specialize (H m).
  specialize (H0 m H1).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  tauto.
Qed.

Lemma is_at_least_n_stream_fstn_stream {A: Type}: forall n m (h: stream A), n <= m -> (is_at_least_n_stream n (fstn_stream m h) <-> is_at_least_n_stream n h).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  split; intros; hnf; intros.
  + specialize (H0 n' H1).
(* Goal: le n (S n) *)
    rewrite fstn_stream_Some in H0 by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
  + specialize (H0 n' H1).
(* Goal: le n (S n) *)
    rewrite fstn_stream_Some by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
Qed.

Lemma squeeze_stream_coincide {A: Type}: forall n (h1 h2: stream A),
  prefix_stream (fstn_stream n h1) h2 ->
  prefix_stream h2 h1 ->
  stream_coincide n h1 h2.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  hnf; intros.
  specialize (H m).
  specialize (H0 m).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  rewrite fstn_stream_Some in H by auto.
(* Goal: False *)
  destruct H, H0; congruence.
Qed.

Fixpoint app_fin_inf {A: Type} (l: list A) (f: nat -> A) :=
  match l with
  | nil => f
  | qa :: l0 => fun n => 
                match n with
                | 0 => qa
                | S m => app_fin_inf l0 f m
                end
  end.

Lemma app_fin_inf_list {A: Type}: forall l (h: nat -> A) m, m < length l -> Some (app_fin_inf l h m) = nth_error l m.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  revert l H; induction m; intros; simpl.
  + destruct l; [simpl in H; omega |].
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    simpl; auto.
  + destruct l; [simpl in H; omega |].
    simpl.
    apply IHm.
(* Goal: le n (S n) *)
    simpl in H; omega.
Qed.

Lemma app_fin_inf_fun {A: Type}: forall l (h: nat -> A) m, length l <= m -> app_fin_inf l h m = h (m - length l).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  revert m H; induction l; intros; simpl.
(* Goal: le n (S n) *)
  + f_equal; omega.
  + destruct m; [simpl in H; omega |].
    rewrite IHl by (simpl in H; omega).
    f_equal.
Qed.

Lemma length_firstn_list_from_fun: forall {A} (f: nat -> A) n, length (fisrtn_list_from_fun f n) = n.
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  induction n; simpl; auto.
  rewrite app_length, IHn.
  simpl.
(* Goal: le n (S n) *)
  omega.
Qed.

Lemma nth_error_firstn_list_from_fun: forall {A} (f: nat -> A) n m, m < n -> nth_error (fisrtn_list_from_fun f n) m = Some (f m).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  revert m H; induction n; intros; simpl.
(* Goal: le n (S n) *)
  + omega.
  + destruct (le_dec n m).
    - assert (n = m) by omega; subst.
      replace m with (length (fisrtn_list_from_fun f m) + 0) at 3 by (rewrite length_firstn_list_from_fun; omega).
      rewrite nth_error_app.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      simpl; auto.
    - rewrite nth_error_app1 by (rewrite length_firstn_list_from_fun; omega).
(* Goal: le n (S n) *)
      apply IHn; omega.
Qed.

Lemma fstn_app_inf_fin {A: Type}: forall l (h: nat -> A) n,
  n >= length l ->
  fstn_stream n (inf_stream (app_fin_inf l h)) = fin_stream (l ++ fisrtn_list_from_fun h (n - length l)).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  stream_extensionality m.
  destruct (le_dec n m).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
  + rewrite fstn_stream_None by auto.
    simpl.
    symmetry.
    apply nth_error_None_iff.
    rewrite app_length.
    rewrite length_firstn_list_from_fun.
(* Goal: le n (S n) *)
    omega.
(* Goal: le n (S n) *)
  + rewrite fstn_stream_Some by omega.
    simpl.
    destruct (le_dec (length l) m).
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    - rewrite app_fin_inf_fun by auto.
(* Goal: le n (S n) *)
      replace m with (length l + (m - length l)) at 2 by omega.
      rewrite nth_error_app.
(* Goal: le n (S n) *)
      rewrite nth_error_firstn_list_from_fun by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      auto.
(* Goal: le n (S n) *)
    - rewrite nth_error_app1 by omega.
(* Goal: le n (S n) *)
      rewrite app_fin_inf_list by omega.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
      auto.
Qed.

Lemma inf_stream_construction {A: Type}: forall (P: stream A -> Prop) (init: list A),
  P (fin_stream init) ->
  (forall l, P (fin_stream l) -> exists qa, P (fin_stream (l ++ qa :: nil))) ->
  exists h, is_inf_stream h /\ forall n, n >= length init -> P (fstn_stream n h).
Proof.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  intros.
  pose (Q := fun l => P (fin_stream (init ++ l))).
  destruct (nat_stepwise_choice Q) as [h ?].
  + hnf.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    rewrite app_nil_r; auto.
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
  + subst Q; simpl; intros.
    specialize (H0 _ H1).
    destruct H0 as [qa ?]; exists qa.
    rewrite app_assoc.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
  + exists (inf_stream (app_fin_inf init h)).
    split; [apply inf_stream_inf |].
(* Goal: forall (h : stream A) (n : nat), or (@is_at_most_n_stream A n h) (@is_at_least_n_stream A n h) *)
    intros.
    specialize (H1 (n - length init)).
    unfold Q in H1.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    rewrite (fstn_app_inf_fin init h n) by auto.
(* Goal: or (@ex nat (fun m : nat => and (ge m n) (@is_n_stream A m h))) (@is_inf_stream A h) *)
    auto.
Qed.

*)