Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Wf_nat.
Require Import Logic.lib.Coqlib.
Require Import Logic.lib.Stream.SigStream.
Require Import Logic.lib.Stream.SigStream.
Require Import Logic.lib.Stream.StreamFunctions.

Lemma cut2_exists {A: Type}: forall (h: stream A) (P: A -> Prop),
  (exists h1 h2,
     is_fin_stream h1 /\
     h = stream_app h1 h2 /\
     (forall n a, h1 n = Some a -> ~ P a) /\
     (exists a, h2 0 = Some a /\ P a)) \/
  (forall n a, h n = Some a -> ~ P a).
Proof.
(* Goal: forall (h : stream A) (P : forall _ : A, Prop), or (@ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a)))))))) (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h n) (@Some A a)), not (P a)) *)
  intros.
(* Goal: or (@ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a)))))))) (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h n) (@Some A a)), not (P a)) *)
  destruct (classic (exists n a, h n = Some a /\ P a)).
  + left.
    apply (dec_inh_nat_subset_has_unique_least_element
             _ (fun n => classic _)) in H.
(* Goal: @ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a))))))) *)
    destruct H as [n [[? ?] _]].
(* Goal: @ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a))))))) *)
    destruct H as [a [? ?]].
(* Goal: @ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a))))))) *)
    exists (fstn_stream n h), (skipn_stream n h).
(* Goal: and (@is_fin_stream A (@fstn_stream A n h)) (and (@eq (stream A) h (@stream_app A (@fstn_stream A n h) (@skipn_stream A n h))) (and (forall (n0 : nat) (a : A) (_ : @eq (option A) (@stream_get A (@fstn_stream A n h) n0) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A (@skipn_stream A n h) O) (@Some A a)) (P a))))) *)
    split; [| split; [| split]].
    - apply fstn_stream_is_fin_stream.
    - symmetry; apply stream_app_fstn_skipn.
    - clear H H1 a.
(* Goal: forall (n0 : nat) (a : A) (_ : @eq (option A) (@stream_get A (@fstn_stream A n h) n0) (@Some A a)), not (P a) *)
      intros; intro.
      destruct (lt_dec n0 n);
        [| rewrite fstn_stream_None in H by omega; congruence].
(* Goal: False *)
      rewrite fstn_stream_Some in H by auto.
(* Goal: False *)
      specialize (H0 n0 (ex_intro _ a (conj H H1))).
(* Goal: False *)
      omega.
    - exists a; split; auto.
  + right.
(* Goal: forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h n) (@Some A a)), not (P a) *)
    firstorder.
Qed.

Lemma cut_omega_exists {A: Type}: forall (h: stream A) (P: A -> Prop),
  (exists a, h 0 = Some a /\ P a) ->
  (exists hs,
     (forall n, is_fin_stream (hs n)) /\
     h = stream_capp hs /\
     (forall m n a, hs m (S n) = Some a -> ~ P a) /\
     (forall n, exists a, hs n 0 = Some a /\ P a)) \/
  (exists hs: list (stream A),
     (Forall is_fin_stream hs) /\
     h = fold_right stream_app empty_stream hs /\
     (Forall (fun h0: stream A => forall n a, h0 (S n) = Some a -> ~ P a) hs) /\
     (Forall (fun h0: stream A => exists a, h0 0 = Some a /\ P a) hs)).
Proof.
(* Goal: forall (h : stream A) (P : forall _ : A, Prop), or (@ex (stream A) (fun h1 : stream A => @ex (stream A) (fun h2 : stream A => and (@is_fin_stream A h1) (and (@eq (stream A) h (@stream_app A h1 h2)) (and (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h1 n) (@Some A a)), not (P a)) (@ex A (fun a : A => and (@eq (option A) (@stream_get A h2 O) (@Some A a)) (P a)))))))) (forall (n : nat) (a : A) (_ : @eq (option A) (@stream_get A h n) (@Some A a)), not (P a)) *)
  intros.
Abort.


