Require Import List Arith Bool Lia Eqdep_dec.

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

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

From Undecidability.Shared.Libs.DLW.Wf
  Require Import wf_finite.

From Undecidability.TRAKHTENBROT
  Require Import notations decidable fol_ops fo_sig fo_terms fo_logic fo_sat
                 membership hfs reln_hfs.

Import fol_notations.

Set Implicit Arguments.

Local Infix "∊" := In (at level 70, no associativity).
Local Infix "⊑" := incl (at level 70, no associativity).


Local Notation ø := vec_nil.

Section Sign_Sig2_encoding.

  Variable (n : nat).

  Notation Σ2 := (Σrel 2).
  Notation Σn := (Σrel n).

  Infix "∈" := Σ2_mem.
  Infix "≈" := Σ2_equiv.
  Infix "⊆" := Σ2_incl.

  Notation "t ∋ ⦉ v ⦊" := (Σ2_is_tuple_in t v) (at level 70, format "t ∋ ⦉ v ⦊").


  Arguments Σrel_var {k}.

  Fixpoint Σn_Σ2 (d r : nat) (A : fol_form Σn) : fol_form Σ2 :=
    match A with
      | ⊥ => ⊥
      | fol_atom _ v => r ∋ ⦉vec_map Σrel_var v⦊
      | fol_bin b A B => fol_bin b (Σn_Σ2 d r A) (Σn_Σ2 d r B)
      | fol_quant fol_fa A => ∀ 0 ∈ (S d) ⤑ Σn_Σ2 (S d) (S r) A
      | fol_quant fol_ex A => ∃ 0 ∈ (S d) ⟑ Σn_Σ2 (S d) (S r) A
     end.

  Variable (X : Type) (M2 : fo_model Σ2 X).
  Variable (Y : Type) (Mn : fo_model Σn Y).

  Notation "a ∈ₘ b" := (fom_rels M2 tt (a##b##ø)) (at level 59, no associativity).
  Notation P := (fun v => fom_rels Mn tt v).

  Variable R : Y -> X -> Prop.


  Let HR1 (d r : X) := forall y, exists x, x ∈ₘ d /\ R y x.
  Let HR2 (d r : X) := forall x, x ∈ₘ d -> exists y, R y x.
  Let HR3 (d r : X) := forall v w,
            (forall p, R (vec_pos v p) (vec_pos w p))
         -> P v <-> mb_is_tuple_in (fun a b => a ∈ₘ b) r w.

  Notation "⟪ A ⟫" := (fun ψ => fol_sem M2 ψ A).
  Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'").


  Lemma Σn_Σ2_correct (A : fol_form Σn) d r φ ψ :
            HR1 (ψ d) (ψ r)
         -> HR2 (ψ d) (ψ r)
         -> HR3 (ψ d) (ψ r)
        -> (forall x, x ∊ fol_vars A -> R (φ x) (ψ x))
        -> ⟪ A ⟫' φ <-> ⟪Σn_Σ2 d r A⟫ ψ.
  Proof.
    revert d r φ ψ.
    induction A as [ | [] v | b A HA B HB | [] A HA ]; intros l r phi psy H1 H2 H3 H.
    + simpl; tauto.
    + simpl; red in H3.
      rewrite H3 with (w := vec_map (fun x => psy (Σrel_var x)) v).
      * apply (fol_quant_sem_ext fol_ex); intros x.
        apply (fol_bin_sem_ext fol_conj); try tauto.
        rewrite Σ2_is_tuple_spec; simpl.
        rewrite !vec_map_map; simpl; tauto.
      * intros p; rewrite !vec_pos_map.
        case_eq (vec_pos v p).
        2: intros [].
        simpl; intros x Hx; rewrite Hx; simpl.
        apply H; simpl; apply in_flat_map.
        exists (vec_pos v p); split.
        - apply in_vec_list, in_vec_pos.
        - simpl; rewrite Hx; simpl; auto.
    + simpl; apply fol_bin_sem_ext; [ apply HA | apply HB ];
        intros; auto; apply H, in_or_app; simpl; auto.
    + simpl; split.
      * intros (x & Hx).
        destruct (H1 x) as (y & G1 & G2).
        exists y; split.
        - rew fot; simpl; auto.
        - revert Hx; apply HA; auto.
          intros [ | n' ]; simpl; auto.
          intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto.
      * intros (y & G1 & G2); revert G1 G2; rew fot; simpl; intros G1 G2.
        destruct (H2 _ G1) as (x & G3).
        exists x; revert G2; apply HA; auto.
        intros [ | n' ]; simpl; auto.
        intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto.
    + simpl; split.
      * intros G1 y; rew fot; simpl; intros G2.
        destruct (H2 _ G2) as (x & G3).
        generalize (G1 x); apply HA; auto.
        intros [ | n' ]; simpl; auto.
        intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto.
      * intros G1 x.
        destruct (H1 x) as (y & G2 & G3).
        generalize (G1 _ G2); apply HA; auto.
        intros [ | n' ]; simpl; auto.
        intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto.
  Qed.

  Variable A : fol_form Σn.


  Let B := fol_subst (fun v => £ (2+v)) A.
  Let d := 0.
  Let r := 1.



  Definition Σn_Σ2_enc := Σ2_non_empty d ⟑ Σ2_list_in d (fol_vars B) ⟑ Σn_Σ2 d r B.

End Sign_Sig2_encoding.

Section SAT2_SATn.

  Variable n : nat.


  Section nested.

    Variables (A : fol_form (Σrel n))
              (X : Type)
              (M2 : fo_model (Σrel 2) X)
              (M2fin : finite_t X)
              (M2dec : fo_model_dec M2)
              (ψ : nat -> X)
              (HA : fol_sem M2 ψ (Σn_Σ2_enc A)).

    Let mem a b := fom_rels M2 tt (a##b##ø).

    Let mem_dec : forall x y, { mem x y } + { ~ mem x y }.
    Proof. intros x y; apply (@M2dec tt). Qed.


    Let P x := (if mem_dec x (ψ 0) then true else false) = true.

    Let HP0 x : P x <-> mem x (ψ 0).
    Proof.
      unfold P.
      destruct (mem_dec x (ψ 0)); split; try tauto; discriminate.
    Qed.

    Let HP1 : finite_t (sig P).
    Proof.
      apply fin_t_finite_t.
      + intros; apply UIP_dec, bool_dec.
      + apply finite_t_fin_t_dec; auto.
        intro; apply bool_dec.
    Qed.

    Notation π1 := (@proj1_sig _ _).

    Let Mn : fo_model (Σrel n) (sig P).
    Proof.
      exists.
      + intros [].
      + intros [] v.
        exact (mb_is_tuple_in mem (ψ 1) (vec_map π1 v)).
    Defined.

    Let Mn_dec : fo_model_dec Mn.
    Proof. intros [] v; apply mb_is_tuple_in_dec; auto. Qed.

    Let R (x : sig P) (y : X) := π1 x = y.

    Local Lemma SAT2_to_SATn : exists Y, fo_form_fin_dec_SAT_in A Y.
    Proof.
      exists (sig P).
      simpl in HA. destruct HA as (H2 & H3 & H4).
      change (fol_sem M2 ψ (Σ2_non_empty 0)) in H2.
      rewrite Σ2_non_empty_spec in H2.
      rewrite Σ2_list_in_spec in H3.
      revert H3 H4; set (B := A⦃fun v : nat => in_var (2 + v)⦄); intros H3 H4.
      assert (H5 : forall n, n ∊ fol_vars B -> P (ψ n))
        by (intros; apply HP0, H3; auto).
      destruct H2 as (x0 & H0).
      generalize H0; intros H2.
      apply HP0 in H0.
      set (phi := fun n : nat =>
        match in_dec eq_nat_dec n (fol_vars B) with
          | left H => exist _ (ψ n) (H5 _ H)
          | right _ => exist _ x0 H0
        end : sig P).
      exists Mn, HP1, Mn_dec, (fun n => phi (2+n)).
      unfold B in *; clear B.
      rewrite <- Σn_Σ2_correct with (Mn := Mn) (φ := phi) (R := R) in H4.
      + rewrite fol_sem_subst in H4.
        revert H4; apply fol_sem_ext; intro; rew fot; auto.
      + intros (x & Hx); exists x; unfold R; simpl; split; auto.
        apply HP0 in Hx; auto.
      + intros x Hx; apply HP0 in Hx.
        exists (exist _ x Hx); red; simpl; auto.
      + intros v w Hvw. simpl.
        apply fol_equiv_ext; f_equal.
        apply vec_pos_ext; intros p.
        rewrite vec_pos_map; apply Hvw.
      + intros j Hj; red.
        unfold phi.
        destruct (in_dec eq_nat_dec j (fol_vars A⦃fun v : nat => in_var (2 + v)⦄))
          as [ H | [] ]; auto; simpl.
    Qed.

  End nested.

  Theorem SAT2_SATn A : fo_form_fin_dec_SAT (@Σn_Σ2_enc n A)
                     -> fo_form_fin_dec_SAT A.
  Proof.
    intros (X & M2 & H1 & H2 & psy & H3).
    apply SAT2_to_SATn with X M2 psy; auto.
  Qed.

End SAT2_SATn.

Section SATn_SAT2.

  Variable n : nat.


  Section The_HFS_model.

    Variables (A : fol_form (Σrel n))
              (X : Type) (Mn : fo_model (Σrel n) X)
              (X_fin : finite_t X)
              (X_discr : discrete X)
              (Mn_dec : fo_model_dec Mn)
              (φ : nat -> X)
              (HA : fol_sem Mn φ A).

    Notation P := (fom_rels Mn tt).

    Local Lemma SATn_to_SAT2 : exists Y, fo_form_fin_dec_SAT_in (@Σn_Σ2_enc n A) Y.
    Proof.
      destruct reln_hfs with (R := P)
        as (Y & H1 & mem & H3 & d & r & i & s & H6 & H7 & H9); auto.
      exists Y, (bin_rel_Σ2 mem), H1, (bin_rel_Σ2_dec _ H3), d·r·(fun n => i (φ n)).
      unfold Σn_Σ2_enc; msplit 2; auto.
      + exists (i (φ 0)); simpl; rew fot; simpl; auto.
      + apply Σ2_list_in_spec.
        intros ?; simpl.
        rewrite fol_vars_map, in_map_iff.
        intros (? & <- & ?); simpl; auto.
      + rewrite <- Σn_Σ2_correct
          with (Mn := Mn)
               (R := fun x y => y = i x)
               (φ := (φ 0)·(φ 1)·φ); auto.
        * rewrite fol_sem_subst.
          revert HA; apply fol_sem_ext.
          intros; simpl; rew fot; auto.
        * intros x; exists (i x); split; auto; apply H6.
        * intros ? ? ?; rewrite H9.
          apply fol_equiv_ext; f_equal.
          apply vec_pos_ext; intro; rew vec.
        * intros ?; rewrite fol_vars_map, in_map_iff.
          intros (? & <- & ?); simpl; auto.
    Qed.

  End The_HFS_model.

  Theorem SATn_SAT2 A : fo_form_fin_discr_dec_SAT A
                     -> fo_form_fin_dec_SAT (@Σn_Σ2_enc n A).
  Proof.
    intros (X & ? & Mn & ? & ? & psy & ?).
    apply SATn_to_SAT2 with X Mn psy; auto.
  Qed.

End SATn_SAT2.