Require Import Classical List Lia.

Definition sequence_of A := nat -> A.
Definition normal_subsequence := { sub: nat -> nat | forall i, sub i < sub (S i) }.
Definition normal_subsequence_of A (s: sequence_of A) (sub: normal_subsequence): sequence_of A :=
  fun n => s (proj1_sig sub n).

Definition finite_elements A (P: A -> Prop) (s: sequence_of A) :=
  exists (L: list nat), forall n, P (s n) -> In n L.

Definition infinite_elements A (P: A -> Prop) (s: sequence_of A) :=
  exists (sub: normal_subsequence), forall n, P (s (proj1_sig sub n)).

Theorem nats_not_in_the_list (L: list nat): exists n, forall i, (n < i)%nat -> List.In i L -> False.
Proof.
  pose (proj1 (List.list_max_le L (List.list_max L)) (le_n _)).
  rewrite List.Forall_forall in f.
  exists (List.list_max L). intros.
  apply f in H0. lia.
Qed.

Theorem finite_and_infinite A (P: A -> Prop) (s: sequence_of A):
  finite_elements A P s <-> ~ infinite_elements A P s.
Proof.
  split; intros.
  + intro. unfold finite_elements, infinite_elements in *.
    destruct H as [L H]. destruct H0 as [sub H0].
    destruct (nats_not_in_the_list L).
    assert (forall i, i <= proj1_sig sub i)%nat.
    { intros. induction i. lia. destruct sub. simpl in *. pose (l i). lia. }
    unfold normal_subsequence_of in H0.
    assert (forall n, List.In (proj1_sig sub n) L).
    { intros. apply H. eauto. }
    pose (H1 (proj1_sig sub (S x))). apply f.
    - pose (H2 (S x)). lia.
    - eauto.
  + admit.
Admitted.

Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
  refine (let H := (_ : type) in _).

Theorem finite_and_infinite A (P: A -> Prop) (s: sequence_of A):
  finite_elements A P s <-> ~ infinite_elements A P s.
Proof.
  split; intros.
  + intro. unfold finite_elements, infinite_elements in *.
    destruct H as [L H]. destruct H0 as [sub H0].
    destruct (nats_not_in_the_list L).
    assert (forall i, i <= proj1_sig sub i)%nat.
    { intros. induction i. lia. destruct sub. simpl in *. pose (l i). lia. }
    unfold normal_subsequence_of in H0.
    assert (forall n, List.In (proj1_sig sub n) L).
    { intros. apply H. eauto. }
    pose (H1 (proj1_sig sub (S x))). apply f.
    - pose (H2 (S x)). lia.
    - eauto.
  + unfold finite_elements, infinite_elements in *. simpl.
    assert (~ (forall L: list nat, exists n: nat, P (s n) /\ ~ In n L)).
    { intro. apply H. clear H. apply functional_choice in H0. destruct H0 as [f H0].
      transparent assert (function: (nat -> nat)). Unshelve.
      2: { intro n. induction n.
           + exact (f nil).
           + exact (f (seq 0 (S IHn))). }
      transparent assert (sub: normal_subsequence). Unshelve.
      2: { exists function. intros. induction i.
           + abstract (destruct (H0 (seq 0 (S (f nil)))) as [H1 H2]; rewrite in_seq in H2; simpl in *; lia).
           + abstract (destruct (H0 (seq 0 (S (f (seq O (S (function i))))))) as [H1 H2];
             rewrite in_seq in H2; simpl in *; lia). }
      exists sub. intro. unfold sub. simpl. destruct n.
      + simpl. apply H0.
      + simpl. apply H0. }
    apply not_all_not_ex. intro. apply H0. intros. apply not_all_not_ex. intro. apply (H1 L).
    intro. pose proof (H2 n). tauto.
Qed.