Set Implicit Arguments.
Require Import Lia List.
From Undecidability.HOU Require Import std.lists.basics std.misc std.enumerable std.decidable.
Import ListNotations.

Set Default Proof Using "Type".

Section Reductions.

  Variable (X Y Z: Type).
  Implicit Types (P: X Prop) (Q: Y Prop) (R: Z Prop).

  Definition Neg {X} (P: X Prop) (x: X) := P x.

  Definition reduction {X Y: Type} (P: X Prop) (Q: Y Prop) :=
     f, x, P x Q (f x).

  Notation "P ⪯ Q" := (reduction P Q) (at level 60).

  Lemma reduction_transitive P Q R:
    P Q Q R P R.
  Proof.
    intros [f ] [g ]; exists (f >> g).
    intros x; rewrite , . reflexivity.
  Qed.


  Lemma reduction_reflexive P: P P.
  Proof.
    exists id; reflexivity.
  Qed.


  Lemma reduction_neg P Q: P Q Neg P Neg Q.
  Proof.
    intros [f H]; exists f; unfold Neg; firstorder.
  Qed.


End Reductions.

Hint Resolve reduction_reflexive reduction_transitive : core.
Notation "P ⪯ Q" := (reduction P Q) (at level 60).


Section enum_red.

  Variables (X Y : Type) (p : X Prop) (q : Y Prop).
  Variables (f : X Y) (Hf : x, p x q (f x)).

  Variables (Lq : _) (qe : enum q Lq).

  Variables ( : X).

  Variables (d : Dis Y).

  Fixpoint L (LX : enumT X) n :=
    match n with
    | 0 []
    | S n L LX n [ x | x L_T X n, (f x Lq n) ]
    end.

  Lemma enum_red LX :
    enum p (L LX).
  Proof using qe q Hf.
    split.
    - intros ?. cbn; eauto.
    - split.
      + intros H.
        eapply Hf in H. eapply qe in H as []. destruct (el_T x) as [ ?].
        exists (1 + + ). cbn. in_app 2.
        in_collect x; [|eapply dec_decb]; eapply cum_ge'; eauto; try .
        eapply qe.
      + intros [m H]. induction m.
        * inversion H.
        * cbn in H. inv_collect.
          eapply Hf. eapply qe. eapply decb_dec in H. eauto.
  Qed.


End enum_red.

Lemma enumerable_red X Y (p : X Prop) (q : Y Prop) :
  p q enumerable__T X Dis Y enumerable q enumerable p.
Proof.
  intros [f] H' d [L' ] % enumerable_enum;
    eapply enum_enumT in H'; destruct H' as [H'].
  eapply enumerable_enum; exists (L f L' d H'). eapply enum_red; eauto.
Qed.


Section enum_red2.

  Variables (X Y Z : Type) (p : X Prop) (q : Y Prop).
  Variables (f : X Y) (Hf : x, p x q (f x)).
  Variables (g: Y Z) (Hg: y1 y2, g = g q q ).

  Variables (Lq : _) (qe : enum q Lq).

  Variables (d : Dis Z).

  Variable (LX: enumT X).

  Fixpoint Lalt n :=
    match n with
    | 0 []
    | S n Lalt n [ x | x L_T X n, (g (f x) map g (Lq n)) ]
    end.

  Lemma enum_red2:
    enum p Lalt.
  Proof using qe q Hg Hf.
    split; eauto.
    split.
    - intros H. eapply Hf in H. eapply qe in H as []. destruct (el_T x) as [ ?].
      exists (1 + + ). cbn. in_app 2.
      in_collect x; [|eapply dec_decb]. eapply cum_ge'; eauto; try .
      eapply in_map, cum_ge'; eauto; try . eapply qe.
    - intros [m H]. induction m.
      + inversion H.
      + cbn in H. inv_collect. eapply decb_dec in H.
        inv_collect. eapply Hf, (Hg H), qe; eauto.
  Qed.


End enum_red2.

Lemma enumerable_red2 X Y Z (g: Y Z) (p : X Prop) (q : Y Prop) :
  p q enumerable__T X Dis Z ( y1 y2, g = g q q ) enumerable q enumerable p.
Proof.
  intros [f] H' d [L' ] % enumerable_enum;
    eapply enum_enumT in H'; destruct H' as [H'].
  eapply enumerable_enum; exists (Lalt f g L' d H'). eapply enum_red2; eauto.
Qed.