Require Import List Arith Lia Eqdep_dec Bool.

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

From Undecidability.Shared.Libs.DLW.Vec
  Require Import pos vec.

From Undecidability.TRAKHTENBROT
  Require Import notations decidable fol_ops membership hfs.

Set Default Proof Using "Type".

Set Implicit Arguments.


Section bt_model_n.


  Variable (X : Type) (Xfin : finite_t X) (Xdiscr : discrete X) (x0 : X) (nt : nat).

  Notation "∅" := hfs_empty.
  Infix "∈" := hfs_mem.
  Notation "x ⊆ y" := (forall u, u ∈ x -> u ∈ y).
  Notation "⟬ x , y ⟭" := (hfs_opair x y).


  Section the_model.

    Local Definition X_surj_hfs : { d : hfs &
                     { f : hfs -> X &
                     { g : X -> hfs |
                        hfs_transitive d
                     /\ ∅ ∈ d
                     /\ (forall p, g p ∈ d)
                     /\ (forall x, x ∈ d -> exists p, x = g p)
                     /\ (forall p, f (g p) = p)
                     }}}.
    Proof using x0 Xfin Xdiscr.
      destruct (finite_t_discrete_bij_t_pos Xfin)
        as ([ | n ] & Hn); auto.
      1: { exfalso; destruct Hn as (f & g & H1 & H2).
           generalize (f x0); intro p; invert pos p. }
      destruct Hn as (f & g & H1 & H2).
      destruct (hfs_pos_n_transitive n)
        as (l & g' & f' & G1 & G0 & G2 & G3 & G4).
      exists l, (fun x => g (g' x)), (fun x => f' (f x)); msplit 4; auto.
      + intros x Hx.
        destruct (G3 x Hx) as (p & Hp).
        exists (g p); rewrite H2; auto.
      + intros p; rewrite G4; auto.
    Qed.


    Local Definition d := projT1 X_surj_hfs.
    Local Definition s := projT1 (projT2 X_surj_hfs).
    Local Definition i := proj1_sig (projT2 (projT2 (X_surj_hfs))).

    Let Hd : hfs_transitive d. Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.
    Let Hempty : ∅ ∈ d. Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.

    Local Fact Hs : forall x, s (i x) = x.
    Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.

    Local Fact Hi : forall x, i x ∈ d.
    Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.

    Local Fact Hi' : forall s, s ∈ d -> exists x, s = i x.
    Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.


    Local Definition p := iter hfs_pow d (1+(2*nt)).

    Local Fact Hp1 : hfs_transitive p.
    Proof. apply hfs_iter_pow_trans; auto. Qed.

    Local Fact Hp2 : d ∈ p.
    Proof.
      apply hfs_iter_pow_le with (n := 1); simpl; auto; try lia.
      apply hfs_pow_spec; auto.
    Qed.

    Local Fact Hp5 n v : (forall p, vec_pos v p ∈ d) -> @hfs_tuple n v ∈ iter hfs_pow d (2*n).
    Proof. apply hfs_tuple_pow; auto. Qed.

    Local Fact Hp6 n v : n <= nt -> (forall p, vec_pos v p ∈ d) -> @hfs_tuple n v ∈ p.
    Proof.
      intros L H; apply Hp5 in H.
      revert H; apply hfs_iter_pow_le; try lia; auto.
    Qed.

  End the_model.

  Variable (R : vec X nt -> Prop).
  Hypothesis HR : forall v, { R v } + { ~ R v }.

  Hint Resolve finite_t_prod hfs_mem_fin_t : core.
  Hint Resolve Hp1 Hp2 Hp5 Hp6 Hs Hi Hi' : core.

  Section the_relation.


    Let encode_R : { r | r ∈ p
                      /\ (forall v, @hfs_tuple nt v ∈ r -> forall q, vec_pos v q ∈ d)
                      /\ forall v, R v <-> hfs_tuple (vec_map i v) ∈ r }.
    Proof.
      set (P v := R (vec_map s v) /\ forall q, vec_pos v q ∈ d).
      set (f := @hfs_tuple nt).
      destruct hfs_comprehension with (P := P) (f := f) as (r & Hr).
      + apply fin_t_dec.
        * intros; apply HR.
        * apply fin_t_vec with (P := fun t => t ∈ d).
          apply hfs_mem_fin_t.
      + exists r; msplit 2.
        * unfold p; rewrite plus_comm, iter_plus with (b := 1).
          apply hfs_pow_spec; intros x; rewrite Hr.
          intros (v & H1 & <-).
          apply Hp5, H1.
        * unfold f; intros v.
          rewrite Hr.
          intros (w & H1 & H2).
          apply hfs_tuple_spec in H2; subst w.
          apply H1.
        * intros v.
          rewrite Hr.
          split.
          - exists (vec_map i v); split; auto.
            split; auto.
            ++ rewrite vec_map_map.
               revert H; apply fol_equiv_ext.
               f_equal; apply vec_pos_ext; intro; rew vec.
            ++ intro; rew vec.
          - intros (w & (H1 & _) & H2).
            apply hfs_tuple_spec in H2.
            revert H1; subst w; apply fol_equiv_ext.
            f_equal; apply vec_pos_ext; intro; rew vec.
    Qed.

    Local Definition r := proj1_sig encode_R.

    Local Fact Hr1 : r ∈ p.
    Proof. apply (proj2_sig encode_R). Qed.

    Local Fact Hr2 v : @hfs_tuple nt v ∈ r -> forall q, vec_pos v q ∈ d.
    Proof. apply (proj2_sig encode_R). Qed.

    Local Fact Hr3 v : R v <-> hfs_tuple (vec_map i v) ∈ r.
    Proof. apply (proj2_sig encode_R). Qed.

  End the_relation.

  Hint Resolve Hr1 Hr2 Hr3 : core.


  Local Definition p_bool x := if hfs_mem_dec x p then true else false.

  Local Fact p_bool_spec x : x ∈ p <-> p_bool x = true.
  Proof.
    unfold p_bool.
    destruct (hfs_mem_dec x p); split; try tauto; discriminate.
  Qed.

  Local Fact p_bool_spec1 x : x ∈ p -> p_bool x = true.
  Proof. apply p_bool_spec. Qed.

  Local Fact p_bool_spec2 x : p_bool x = true -> x ∈ p.
  Proof. apply p_bool_spec. Qed.

  Local Definition Y := sig (fun x => p_bool x = true).

  Notation π1 := (@proj1_sig _ (fun x => p_bool x = true)).

  Hint Resolve p_bool_spec p_bool_spec1 p_bool_spec2 : core.

  Local Fact eqY : forall x y : Y, π1 x = π1 y -> x = y.
  Proof.
    intros (x & Hx) (y & Hy); simpl.
    intros; subst; f_equal; apply UIP_dec, bool_dec.
  Qed.

  Local Fact HY : finite_t Y.
  Proof.
    apply fin_t_finite_t.
    + intros; apply UIP_dec, bool_dec.
    + generalize (hfs_mem_fin_t p); apply fin_t_equiv.
      intros x; auto.
  Qed.


  Local Fact discrY : discrete Y.
  Proof.
    intros (x & Hx) (y & Hy).
    destruct (hfs_eq_dec x y) as [ -> | D ].
    + left; f_equal; apply UIP_dec, bool_dec.
    + right; contradict D; inversion D; auto.
  Qed.

  Local Definition mem (x y : Y) := π1 x ∈ π1 y.

  Local Fact mem_dec : forall x y, { mem x y } + { ~ mem x y }.
  Proof.
    intros (a & ?) (b & ?); unfold mem; simpl; apply hfs_mem_dec.
  Qed.

  Local Definition yd : Y := exist _ _ (p_bool_spec1 Hp2).
  Local Definition yr : Y := exist _ _ (p_bool_spec1 Hr1).

  Local Fact fa_mem_Y (P : _ -> Prop) :
                           (forall a, a ∈ p -> P a)
                       <-> (forall a, P (π1 a)).
  Proof.
    split.
    + intros H (a & Ha); simpl; auto.
    + intros H a Ha.
      apply (H (exist _ _ (p_bool_spec1 Ha))).
  Qed.

  Local Fact ex_mem_Y (P : _ -> Prop) :
                           (exists a, a ∈ p /\ P a)
                       <-> (exists a, P (π1 a)).
  Proof.
    split.
    + intros (a & H & Ha).
      exists (exist _ a (p_bool_spec1 H)); auto.
    + intros ((a & Ha) & H); simpl in *; eauto.
  Qed.

  Local Fact mem_fa_Y (P : _ -> Prop) k : k ∈ p -> (forall a, P a -> a ∈ p)
                       -> (forall a, a ∈ k <-> P a)
                       <-> (forall a, π1 a ∈ k <-> P (π1 a)).
  Proof.
    intros H1 H2.
    rewrite <- fa_mem_Y with (P := fun a => a ∈ k <-> P a).
    split.
    + intros H ? _; auto.
    + intros H a; split.
      * intros Ha; apply H; auto.
        apply (Hp1 Ha); auto.
      * intros Ha; apply H; auto.
  Qed.


  Local Fact mem_equiv_Y u v :
                        u ∈ p
                     -> v ∈ p
                     -> (forall y : Y, π1 y ∈ u <-> π1 y ∈ v)
                    <-> (forall x : hfs, x ∈ u <-> x ∈ v).
  Proof.
    intros Hu Hv.
    symmetry; apply mem_fa_Y; auto.
    intros s Hs; apply (Hp1 Hs); auto.
  Qed.

  Local Fact is_equiv : forall x y, mb_equiv mem x y <-> π1 x = π1 y.
  Proof.
    intros (x & Hx) (y & Hy); simpl.
    unfold mb_equiv, mem; simpl; split.
    2: { intros []; tauto. }
    rewrite mem_equiv_Y; auto; apply hfs_mem_ext.
  Qed.

  Local Fact mem_ext_Y x y : x ∈ p -> y ∈ p -> (forall a, π1 a ∈ x <-> π1 a ∈ y) <-> x = y.
  Proof.
    intros H1 H2; split.
    + intros H; apply hfs_mem_ext.
      rewrite mem_fa_Y; auto.
      intros z Hz; apply (Hp1 Hz); auto.
    + intros ->; tauto.
  Qed.

  Hint Resolve mem_ext_Y : core.

  Local Fact is_pair : forall x y k, mb_is_pair mem k x y
                                 <-> π1 k = hfs_pair (π1 x) (π1 y).
  Proof.
    intros (x & Hx) (y & Hy) (k & Hk); simpl.
    unfold mb_is_pair; simpl.
    unfold mb_equiv, mem; simpl.
    rewrite hfs_pair_spec'.
    rewrite mem_fa_Y; auto.
    2: intros ? [ -> | -> ]; auto.
    fol equiv; intros (a & Ha); simpl.
    fol equiv; try tauto.
    fol equiv; auto.
  Qed.

  Local Fact is_opair : forall x y k, mb_is_opair mem k x y
                                  <-> π1 k = ⟬π1 x,π1 y⟭.
  Proof.
    intros (x & Hx) (y & Hy) (k & Hk); simpl.
    unfold mb_is_opair; simpl.
    split.
    + intros ((a & Ha) & (b & Hb) & H); revert H.
      repeat rewrite is_pair; simpl.
      intros (-> & -> & ->); auto.
    + intros ->.
      generalize Hx Hy Hk; revert Hx Hy Hk.
      do 3 rewrite <- p_bool_spec at 1.
      intros Hx' Hy' Hk' Hx Hy Hk.
      apply hfs_trans_opair_inv in Hk'; auto.
      do 2 rewrite p_bool_spec in Hk'.
      destruct Hk' as (H1 & H2).
      exists (exist _ (hfs_pair x x) H1).
      exists (exist _ (hfs_pair x y) H2).
      repeat rewrite is_pair; simpl; auto.
  Qed.

  Local Fact is_tuple n : forall v t, @mb_is_tuple _ mem t n v
                                  <-> π1 t = hfs_tuple (vec_map π1 v).
  Proof.
    induction n as [ | n IHn ]; intros v (t & Ht).
    + vec nil v; clear v; simpl; split.
      * intros H; apply hfs_mem_ext.
        intros z; split.
        - intros Hz.
          assert (Hz' : p_bool z = true).
          { apply p_bool_spec.
            apply Hp1 with (1 := Hz), p_bool_spec; auto. }
          destruct (H (exist _ z Hz')); auto.
        - rewrite hfs_empty_spec; tauto.
      * intros -> (z & ?); unfold mem; simpl.
        rewrite hfs_empty_spec; tauto.
    + vec split v with x; simpl; split.
      * intros (t' & H1 & H2).
        rewrite IHn in H2; try lia.
        rewrite <- H2.
        apply is_opair with (k := exist _ t Ht); auto.
      * intros ->.
        assert (H1 : p_bool (hfs_tuple (vec_map π1 v)) = true).
        { apply p_bool_spec.
          apply p_bool_spec in Ht.
          apply hfs_trans_opair_inv, proj2, hfs_trans_pair_inv in Ht; auto; tauto. }
        exists (exist _ (hfs_tuple (vec_map π1 v)) H1); split.
        - rewrite is_opair; simpl; auto.
        - rewrite IHn; simpl; auto.
  Qed.

  Local Fact has_tuples : mb_has_tuples mem yd nt.
  Proof.
    intros v Hv.
    set (t := hfs_tuple (vec_map (proj1_sig (P:=fun x : hfs => p_bool x = true)) v)).
    assert (H1 : p_bool t = true).
    { apply p_bool_spec, Hp6; auto; intro; rew vec; apply Hv. }
    exists (exist _ t H1).
    apply is_tuple; simpl; reflexivity.
  Qed.

  Local Definition i' x : Y := exist _ _ (p_bool_spec1 (Hp1 (Hi x) Hp2)).

  Local Fact Hi'' x : mem (i' x) yd.
  Proof. unfold i', yd, mem; simpl; auto. Qed.

  Hint Resolve Hi'' : core.

  Local Definition s' (y : Y) : X := s (π1 y).


  Theorem reln_hfs : { Y : Type &
                     { _ : finite_t Y &
                     { mem : Y -> Y -> Prop &
                     { _ : forall u v, { mem u v } + { ~ mem u v } &
                     { yd : Y &
                     { yr : Y &
                     { i : X -> Y &
                     { s : Y -> X &
                             (forall x, mem (i x) yd)
                          /\ (forall y, mem y yd -> exists x, y = i x)
                          /\ (forall v, R v <-> mb_is_tuple_in mem yr (vec_map i v))
                      }}}}}}}}.
  Proof using x0 Xfin Xdiscr HR.
    exists Y, HY, mem, mem_dec, yd, yr, i', s'.
    msplit 2; auto.
    + intros y Hy; unfold i'.
      destruct (Hi' Hy) as (x & Hx).
      exists x; apply eqY; simpl; auto.
    + intros v; rewrite Hr3; split.
      * intros Hv.
        red.
        assert (H1 : p_bool (hfs_tuple (vec_map i v)) = true).
        { apply p_bool_spec, Hp1 with (1 := Hv); auto. }
        exists (exist _ (hfs_tuple (vec_map i v)) H1); split.
        - apply is_tuple; simpl; rewrite vec_map_map; auto.
        - unfold yr; red; simpl; auto.
      * intros ((t & Ht) & H1 & H2).
        rewrite is_tuple in H1.
        simpl in H1, H2.
        rewrite vec_map_map in H1; subst t; auto.
  Qed.

End bt_model_n.