Require Import List Arith Nat Lia Relations Bool.

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

Local Infix "∈" := In (at level 70, no associativity).
Local Infix "⊆" := incl (at level 70, no associativity).
Local Notation "P ≅ Q" := ((P Q) * (Q P))%type (at level 70, no associativity).

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, y l R x y)
              *( x y, x l R x y P y) }%type.

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

  Fact finite_t_fin_upto : finite_t_upto fin_t_upto ( _ True).
  Proof. split; intros []; red; eauto; 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 | length ll = 2 ^ (length l)
                                      R, wdec R
                                    T, T ll
                                      x, x l R x T x }.
  Proof.
    induction l as [ | x l IHl ].
    + exists (( _ True) :: nil); split; auto.
      intros R HR; exists ( _ True); simpl; split; tauto.
    + destruct IHl as (ll & Hl & Hll).
      exists (map ( T a xa T a) ll map ( T a x=a T a) ll); split.
      1: rewrite app_length, !map_length; simpl; .
      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 (h : finite_t X) :
            { ll | length ll = 2 ^ (length (proj1_sig h))
                  R, wdec R T, T ll x, R x T x }.
  Proof.
    destruct h as (l & Hl).
    destruct (pset_fin_t l) as (ll & H & Hll).
    exists ll; split; auto.
    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
         { ll | R,
                      ( x y : X, R x y R x y)
                    T, T ll x y, R x y T x y }.
Proof.
  intros h.
  destruct finite_t_weak_dec_powerset with (h := finite_t_prod h h)
    as (l & _ & Hl).
  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.