From PCF2.external.Synthetic Require Import DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts.
Require Import PCF2.external.Shared.Dec.
Require Cantor.
Require Import List.
Import ListNotations.

#[global]
Instance list_in_dec X (x : X) (A : list X) :
  eq_dec X dec (In x A).
Proof.
  intros D. apply in_dec. exact D.
Qed.


Definition cumulative {X} (L: list X) :=
   n, A, L (S n) = L n A.
#[export] Hint Extern 0 (cumulative _) intros ?; cbn; eauto : core.

Lemma cum_ge {X} {L: list X} {n m} :
  cumulative L m n A, L m = L n A.
Proof.
  induction 2 as [|m _ IH].
  - exists nil. now rewrite app_nil_r.
  - destruct (H m) as (A&), IH as [B ].
    exists (B A). now rewrite app_assoc.
Qed.


Lemma cum_ge' {X} {L: list X} {x n m} :
  cumulative L In x (L n) m n In x (L m).
Proof.
  intros ? H [A ] % (cum_ge (L := L)). apply in_app_iff. eauto. eauto.
Qed.


Definition list_enumerator {X} (L: list X) (p : X Prop) :=
   x, p x m, In x (L m).
Definition list_enumerable {X} (p : X Prop) :=
   L, list_enumerator L p.

Definition list_enumerator__T' X f := x : X, n : , In x (f n).
Notation list_enumerator__T f X := (list_enumerator__T' X f).
Definition list_enumerable__T X := f : list X, list_enumerator__T f X.
Definition inf_list_enumerable__T X := { f : list X | list_enumerator__T f X }.

Section enumerator_list_enumerator.

  Variable X : Type.
  Variable p : X Prop.
  Variables (e : option X).

  Let T (n : ) : list X := match e n with Some x [x] | None [] end.

  Lemma enumerator_to_list_enumerator : x, ( n, e n = Some x) ( n, In x (T n)).
  Proof.
    split; intros [n H].
    - exists n. unfold T. rewrite H. firstorder.
    - unfold T in *. destruct (e n) eqn:E. inversion H; subst. eauto. inversion . inversion H.
  Qed.


End enumerator_list_enumerator.

Lemma enumerable_list_enumerable {X} {p : X Prop} :
  enumerable p list_enumerable p.
Proof.
  intros [f Hf]. eexists.
  unfold list_enumerator.
  intros x. rewrite enumerator_to_list_enumerator.
  eapply Hf.
Qed.


Lemma enumerable__T_list_enumerable {X} :
  enumerable__T X list_enumerable__T X.
Proof.
  intros [f Hf]. eexists.
  unfold list_enumerator.
  intros x. rewrite enumerator_to_list_enumerator.
  eapply Hf.
Qed.


Section enumerator_list_enumerator.

  Variable X : Type.
  Variables (T : list X).

  Let e (n : ) : option X :=
    let (n, m) := Cantor.of_nat n in
    nth_error (T n) m.

  Lemma list_enumerator_to_enumerator : x, ( n, e n = Some x) ( n, In x (T n)).
  Proof.
    split; intros [k H].
    - unfold e in *.
      destruct (Cantor.of_nat k) as (n, m).
      exists n. eapply (nth_error_In _ _ H).
    - unfold e in *.
      eapply In_nth_error in H as [m].
      exists (Cantor.to_nat (k, m)). now rewrite Cantor.cancel_of_to, H.
  Qed.


End enumerator_list_enumerator.

Lemma list_enumerator_enumerator {X} {p : X Prop} {T} :
  list_enumerator T p enumerator ( n let (n, m) := Cantor.of_nat n in
    nth_error (T n) m) p.
Proof.
  unfold list_enumerator.
  intros H x. rewrite list_enumerator_to_enumerator. eauto.
Qed.


Lemma list_enumerable_enumerable {X} {p : X Prop} :
  list_enumerable p enumerable p.
Proof.
  intros [T HT]. eexists.
  unfold list_enumerator.
  intros x. rewrite list_enumerator_to_enumerator.
  eapply HT.
Qed.


Lemma list_enumerable__T_enumerable {X} :
  list_enumerable__T X enumerable__T X.
Proof.
  intros [T HT]. eexists.
  unfold list_enumerator.
  intros x. rewrite list_enumerator_to_enumerator.
  eapply HT.
Qed.


Lemma enum_enumT {X} :
  enumerable__T X list_enumerable__T X.
Proof.
  split.
  eapply enumerable__T_list_enumerable.
  eapply list_enumerable__T_enumerable.
Qed.


Definition to_cumul {X} (L : list X) := fix f n :=
  match n with 0 [] | S n f n L n end.

Lemma to_cumul_cumulative {X} (L : list X) :
  cumulative (to_cumul L).
Proof.
  eauto.
Qed.


Lemma to_cumul_spec {X} (L : list X) x :
  ( n, In x (L n)) n, In x (to_cumul L n).
Proof.
  split.
  - intros [n H].
    exists (S n). cbn. eapply in_app_iff. eauto.
  - intros [n H].
    induction n; cbn in *.
    + inversion H.
    + eapply in_app_iff in H as [H | H]; eauto.
Qed.


Lemma cumul_In {X} (L : list X) x n :
  In x (L n) In x (to_cumul L (S n)).
Proof.
  intros H. cbn. eapply in_app_iff. eauto.
Qed.


Lemma In_cumul {X} (L : list X) x n :
  In x (to_cumul L n) n, In x (L n).
Proof.
  intros H. eapply to_cumul_spec. eauto.
Qed.


#[export] Hint Resolve cumul_In In_cumul : core.

Lemma list_enumerator_to_cumul {X} {p : X Prop} {L} :
  list_enumerator L p list_enumerator (to_cumul L) p.
Proof.
  unfold list_enumerator.
  intros. rewrite H.
  eapply to_cumul_spec.
Qed.


Lemma cumul_spec__T {X} {L} :
  list_enumerator__T L X list_enumerator__T (to_cumul L) X.
Proof.
  unfold list_enumerator__T.
  intros. now rewrite to_cumul_spec.
Qed.


Lemma cumul_spec {X} {L} {p : X Prop} :
  list_enumerator L p list_enumerator (to_cumul L) p.
Proof.
  unfold list_enumerator.
  intros. now rewrite to_cumul_spec.
Qed.


Notation cumul := (to_cumul).

Section L_list_def.
  Context {X : Type}.
  Variable (L : list X).

Fixpoint L_list (n : ) : list (list X) :=
  match n
  with
  | 0 [ [] ]
  | S n L_list n map ( '(x, L) x :: L) (list_prod (cumul L n) (L_list n))
  end.
End L_list_def.

Lemma L_list_cumulative {X} L : cumulative (@L_list X L).
Proof.
  intros ?; cbn; eauto.
Qed.


Lemma enumerator__T_list {X} L :
  list_enumerator__T L X list_enumerator__T (L_list L) (list X).
Proof.
  intros H l.
  induction l.
  - exists 0. cbn. eauto.
  - destruct IHl as [n IH].
    destruct (cumul_spec__T H a) as [m ?].
    exists (1 + n + m). cbn. intros. apply in_app_iff. right.
    apply (in_map ( '(x, L) x :: L) _ (a, l)).
    apply in_prod.
    all: eapply cum_ge'; eauto using L_list_cumulative; .
Qed.


Lemma enumerable_list {X} : list_enumerable__T X list_enumerable__T (list X).
Proof.
  intros [L H].
  eexists. now eapply enumerator__T_list.
Qed.


#[export] Hint Extern 4 match goal with [H : list_enumerator _ ?p |- ?p _ ] eapply H end : core.

Require Import PCF2.external.Shared.Dec.


Definition L_T {X : Type} {f : list X} {H : list_enumerator__T f X} : list X.
Proof.
  exact (cumul f).
Defined.

Arguments L_T _ {_ _} _, {_ _ _}.

#[export] Hint Unfold L_T : core.
#[export] Hint Resolve cumul_In : core.

Existing Class list_enumerator__T'.

Definition el_T {X} {f} `{list_enumerator__T f X} : list_enumerator__T L_T X.
Proof.
  now eapply cumul_spec__T.
Defined.


#[global]
Existing Instance enumerator__T_list.

#[global]
Instance enumerator__T_to_list {X} {f} :
  list_enumerator__T f X enumerator__T ( n let (n, m) := Cantor.of_nat n in nth_error (f n) m) X | 100.
Proof.
  intros H x. eapply list_enumerator_to_enumerator in H. exact H.
Qed.


#[global]
Instance enumerator__T_of_list {X} {f} :
  enumerator__T f X list_enumerator__T ( n match f n with Some x [x] | None [] end) X | 100.
Proof.
  intros H x. eapply enumerator_to_list_enumerator. eauto.
Qed.


Existing Class inf_list_enumerable__T.
#[global]
Instance inf_to_enumerator {X} :
   H : inf_list_enumerable__T X, list_enumerator__T (proj1_sig H) X | 100.
Proof.
  intros [? H]. eapply H.
Defined.



#[export] Hint Unfold enumerable list_enumerable : core.

#[export] Hint Resolve enumerable_list_enumerable
     list_enumerable_enumerable : core.

Lemma enumerable_enum {X} {p : X Prop} :
  enumerable p list_enumerable p.
Proof.
  split; eauto.
Qed.