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 Implicit Arguments.


Section bt_model_n.



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

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

  Let X_surj_hfs : { l : hfs & { f : hfs -> X &
                    { g : X -> hfs |
                      hfs_transitive l
                   /\ hfs_empty ∈ l
                   /\ (forall p, g p ∈ l)
                   /\ (forall x, x ∈ l -> exists p, x = g p)
                   /\ (forall p, f (g p) = p) } } }.
  Proof.
    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.


  Let l := projT1 X_surj_hfs.
  Let s := projT1 (projT2 X_surj_hfs).
  Let i := proj1_sig (projT2 (projT2 (X_surj_hfs))).

  Let Hl : hfs_transitive l.
  Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.
  Let Hempty : hfs_empty ∈ l.
  Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.
  Let Hs : forall x, s (i x) = x.
  Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.
  Let Hi : forall x, i x ∈ l.
  Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.
  Let Hi' : forall s, s ∈ l -> exists x, s = i x.
  Proof. apply (proj2_sig (projT2 (projT2 (X_surj_hfs)))). Qed.


  Let p := iter hfs_pow l (1+(2*nt)).

  Let Hp1 : hfs_transitive p.
  Proof. apply hfs_iter_pow_trans; auto. Qed.

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

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

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

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

  Hint Resolve finite_t_prod hfs_mem_fin_t : core.


  Let encode_R : { r | r ∈ p
                      /\ (forall v, @hfs_tuple nt v ∈ r -> forall q, vec_pos v q ∈ l)
                      /\ 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 ∈ l).
    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 ∈ l).
        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.

  Let r := proj1_sig encode_R.

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

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

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


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

  Let 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.

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

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

  Let 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.

  Let 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.

  Let mem (x y : Y) := proj1_sig x ∈ proj1_sig y.

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

  Let yl : Y. Proof. exists l; apply p_bool_spec, Hp2. Defined.
  Let yr : Y. Proof. exists r; apply p_bool_spec, Hr1. Defined.


  Let is_equiv : forall x y, mb_equiv mem x y <-> proj1_sig x = proj1_sig y.
  Proof.
    intros (x & Hx) (y & Hy); simpl.
    unfold mb_equiv, mem; simpl; split.
    2: intros []; tauto.
    intros H.
    apply hfs_mem_ext.
    intros z; split; intros Hz.
    * apply p_bool_spec in Hx.
      generalize (Hp1 Hz Hx).
      rewrite p_bool_spec; intros H'.
      apply (H (exist _ z H')); auto.
    * apply p_bool_spec in Hy.
      generalize (Hp1 Hz Hy).
      rewrite p_bool_spec; intros H'.
      apply (H (exist _ z H')); auto.
  Qed.

  Let is_pair : forall x y k, mb_is_pair mem k x y
                          <-> proj1_sig k = hfs_pair (proj1_sig x) (proj1_sig y).
  Proof.
    intros (x & Hx) (y & Hy) (k & Hk); simpl.
    unfold mb_is_pair; simpl; rewrite hfs_mem_ext.
    generalize Hx Hy Hk; revert Hx Hy Hk.
    do 3 rewrite <- p_bool_spec at 1.
    intros Hx' Hy' Hk' Hx Hy Hk.
    split.
    + intros H a; split; rewrite hfs_pair_spec; [ intros Ha | intros [ Ha | Ha ] ].
      * generalize (Hp1 Ha Hk'); rewrite p_bool_spec; intros Ha'.
        specialize (H (exist _ a Ha')); simpl in H.
        repeat rewrite is_equiv in H; apply H; auto.
      * subst; apply (H (exist _ x Hx)); repeat rewrite is_equiv; simpl; auto.
      * subst; apply (H (exist _ y Hy)); repeat rewrite is_equiv; simpl; auto.
    + intros H (a & Ha); repeat rewrite is_equiv; simpl; rewrite <- hfs_pair_spec.
      apply H.
  Qed.

  Let is_opair : forall x y k, mb_is_opair mem k x y
                           <-> proj1_sig k = ⟬proj1_sig x,proj1_sig y⟭.
  Proof.
    intros (x & Hx) (y & Hy) (k & Hk); simpl.
    unfold mb_is_opair; 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.

  Let is_tuple n : forall v t, @mb_is_tuple _ mem t n v
                           <-> proj1_sig t = hfs_tuple (vec_map (@proj1_sig _ _) 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 (@proj1_sig _ _) v)) = true).
        { apply p_bool_spec.
          apply p_bool_spec in Ht.
          apply hfs_trans_opair_inv, proj2, hfs_trans_pair_inv in Ht; tauto. }
        exists (exist _ (hfs_tuple (vec_map (@proj1_sig _ _) v)) H1); split.
        - rewrite is_opair; simpl; auto.
        - rewrite IHn; simpl; auto.
  Qed.

  Let has_tuples : mb_has_tuples mem yl 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.

  Let i' : X -> Y.
  Proof.
    intros x.
    exists (i x).
    apply p_bool_spec.
    generalize (Hi x) Hp2; apply Hp1.
  Defined.

  Let Hi'' x : mem (i' x) yl.
  Proof. unfold i', yl, mem; simpl; auto. Qed.

  Let s' (y : Y) : X := s (proj1_sig y).


  Theorem reln_hfs : { Y : Type &
                     { _ : finite_t Y &
                     { _ : discrete Y &
                     { mem : Y -> Y -> Prop &
                     { _ : forall u v, { mem u v } + { ~ mem u v } &
                     { yl : Y &
                     { yr : Y &
                     { i : X -> Y &
                     { s : Y -> X &
                             mb_member_ext mem
                          /\ mb_has_tuples mem yl nt
                          /\ (forall x, mem (i x) yl)
                          /\ (forall y, mem y yl -> exists x, y = i x)
                          /\ (forall x, s (i x) = x)
                          /\ (forall v, R v <-> mb_is_tuple_in mem yr (vec_map i v))
                          /\ (forall x y, mb_equiv mem x y <-> x = y)
                      }}}}}}}}}.
  Proof.
    exists Y, HY, discrY, mem, mem_dec, yl, yr, i', s'.
    msplit 6; auto.
    + intros (u & Hu) (v & Hv) (w & Hw); unfold mem; simpl.
      unfold mb_equiv; simpl; intros H.
      cut (u = v); [ intros []; auto | ].
      apply hfs_mem_ext.
      apply p_bool_spec in Hu.
      apply p_bool_spec in Hv.
      clear w Hw.
      intros x; split; intros Hx.
      * generalize (Hp1 Hx Hu); rewrite p_bool_spec; intros H'.
        apply (H (exist _ x H')); auto.
      * generalize (Hp1 Hx Hv); rewrite p_bool_spec; intros H'.
        apply (H (exist _ x H')); 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.
        apply H2.
    + intros x y; rewrite is_equiv; split; auto.
      intros; subst; auto.
  Qed.

End bt_model_n.