Require Import List Arith Nat Lia Relations Bool.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list fin_base.

Set Implicit Arguments.

Section finite_t_upto.

  Variable (X : Type) (R : X X Prop).

  Definition fin_t_upto (P : X Type) :=
     { l : _ & ( x, P x y, In y l R x y)
              *( x y, In x l R x y P y) }%type.

  Definition finite_t_upto :=
     { l : _ | x, y, In y l R x y }.

  Fact finite_t_fin_upto : (finite_t_upto fin_t_upto ( _ True))
                         * (fin_t_upto ( _ True) finite_t_upto).
  Proof.
    split.
    + intros (l & Hl); exists l; split; auto.
    + intros (l & & ); exists l; firstorder.
  Qed.


End finite_t_upto.

Arguments finite_t_upto : clear implicits.

Section finite_t_weak_dec_powerset.


  Variable (X : Type).

  Let wdec (R : X Prop) := x, R x R x.

  Let pset_fin_t (l : list X) : { ll | R (_ : wdec R),
                                         T, In T ll
                                      x, In x l R x T x }.
  Proof.
    induction l as [ | x l IHl ].
    + exists (( _ True) :: nil).
      intros R HR; exists ( _ True); simpl; split; tauto.
    + destruct IHl as (ll & Hll).
      exists (map ( T a xa T a) ll map ( T a x=a T a) ll).
      intros R HR.
      destruct (Hll R) as (T & & ); auto.
      destruct (HR x) as [ | ].
      * exists ( a x = a T a); split.
        - apply in_or_app; right.
          apply in_map_iff; exists T; auto.
        - intros y [ | H ]; simpl; try tauto.
          rewrite ; auto; split; auto.
          intros [ | ]; auto.
          apply ; auto.
      * exists ( a x a T a); split.
        - apply in_or_app; left.
          apply in_map_iff; exists T; auto.
        - intros y [ | H ]; simpl; split; try tauto.
          ++ rewrite ; auto; split; auto.
             contradict ; subst; auto.
          ++ rewrite ; tauto.
  Qed.


  Theorem finite_t_weak_dec_powerset :
              finite_t X
            { l | R, wdec R T, In T l
                            x, R x T x }.
  Proof.
    intros (l & Hl).
    destruct (pset_fin_t l) as (ll & Hll).
    exists ll.
    intros R HR.
    destruct (Hll _ HR) as (T & & ).
    exists T; split; auto.
  Qed.


End finite_t_weak_dec_powerset.


Theorem finite_t_weak_dec_rels X :
            finite_t X { l | R : X X Prop,
                                  ( x y, R x y R x y)
                                 T, In T l x y, R x y T x y }.
Proof.
  intros HX.
  set (Y := (X*X)%type).
  destruct (@finite_t_weak_dec_powerset Y) as (l & Hl).
  + unfold Y; apply finite_t_prod; auto.
  + exists (map ( P x y P (x,y)) l).
    intros R HR.
    destruct (Hl ( c R (fst c) (snd c))) as (T & & ).
    * intros []; apply HR.
    * exists ( x y T (x,y)); split.
      - apply in_map_iff; exists T; auto.
      - intros x y; apply ( (x,y)).
Qed.