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.TRAKHTENBROT
  Require Import notations utils fol_ops fo_sig fo_terms fo_logic fo_sat.

Import fol_notations.

Set Implicit Arguments.


Tactic Notation "iff" "equal" := apply fol_equiv_ext.

Local Notation ø := vec_nil.

Section Sig_n_Sig.

  Variable (Σ : fo_signature) (r : rels Σ).

  Notation Σn := (Σrel (ar_rels _ r)).

  Local Fixpoint enc (A : fol_form Σn) : fol_form Σ :=
    match A with
      |
      | fol_atom _ v fol_atom r (vec_map ( x £(Σrel_var x)) v)
      | fol_bin b A B fol_bin b (enc A) (enc B)
      | fol_quant q A fol_quant q (enc A)
     end.

  Section M_enc_n.

    Variables (X : Type) (M : fo_model Σ X).

    Local Definition M_enc_n : fo_model Σn X.
    Proof.
      exists; intros [] v.
      exact (fom_rels M r v).
    Defined.


    Notation "⟪ A ⟫" := ( ψ fol_sem M ψ A).
    Notation "⟪ A ⟫'" := ( φ fol_sem M_enc_n φ A) (at level 1, format "⟪ A ⟫'").

    Local Fact enc_correct_1 A φ : A ⟫' φ enc A φ.
    Proof.
      revert φ.
      induction A as [ | [] v | b A HA B HB | q A HA ]; intros .
      + simpl; tauto.
      + unfold M_enc_n; simpl; rewrite vec_map_map.
        iff equal; f_equal; apply vec_pos_ext.
        intros p; do 2 rewrite vec_pos_map; rew fot.
        simpl in v; generalize (vec_pos v p); intros [ i | [] ].
        rew fot; simpl; auto.
      + simpl; apply fol_bin_sem_ext; auto.
      + simpl; apply fol_quant_sem_ext; intro; auto.
    Qed.


  End M_enc_n.

  Local Lemma SAT_SATn A : fo_form_fin_dec_SAT (enc A)
                         fo_form_fin_dec_SAT A.
  Proof.
    intros (X & M & & & & ).
    exists X, (M_enc_n M), .
    exists. { intros [] v; apply . }
    exists .
    revert ; apply enc_correct_1.
  Qed.


  Section Mn_enc.

    Variables (X : Type) (Mn : fo_model Σn X) ( : X).

    Local Definition Mn_enc : fo_model Σ X.
    Proof.
      exists.
      + intros s v; apply .
      + intros r' v.
        destruct (eq_nat_dec (ar_rels _ r) (ar_rels _ r')) as [ H | H ].
        * exact (fom_rels Mn tt (eq_rect_r _ v H)).
        * exact False.
    Defined.


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

    Local Fact enc_correct_2 A φ : A ⟫' φ enc A φ.
    Proof.
      revert φ.
      induction A as [ | [] v | b A HA B HB | q A HA ]; intros .
      + simpl; tauto.
      + unfold Mn_enc; simpl; rewrite vec_map_map.
        destruct (eq_nat_dec (ar_rels Σ r) (ar_rels Σ r)) as [ H | [] ]; auto.
        rewrite eq_nat_uniq with (H := H); unfold eq_rect_r; simpl.
        iff equal; f_equal; apply vec_pos_ext.
        intros p; do 2 rewrite vec_pos_map; rew fot.
        simpl in v; generalize (vec_pos v p); intros [ i | [] ].
        rew fot; simpl; auto.
      + simpl; apply fol_bin_sem_ext; auto.
      + simpl; apply fol_quant_sem_ext; intro; auto.
    Qed.


  End Mn_enc.

  Local Lemma SATn_SAT A : fo_form_fin_dec_SAT A
                         fo_form_fin_dec_SAT (enc A).
  Proof.
    intros (X & Mn & & & & ).
    exists X, (Mn_enc Mn ( 0)), .
    exists.
    { intros r' v; simpl.
      destruct (eq_nat_dec (ar_rels Σ r) (ar_rels Σ r')) as [ H | H ].
      + revert v; rewrite H; unfold eq_rect_r; simpl; intro; apply .
      + right; tauto. }
    exists .
    revert ; apply enc_correct_2.
  Qed.


  Hint Resolve SATn_SAT SAT_SATn : core.

  Local Theorem SATn_SAT_red :
       { f : fol_form Σn fol_form Σ
           | A, fo_form_fin_dec_SAT A fo_form_fin_dec_SAT (f A) }.
  Proof. exists enc; split; auto. Qed.

End Sig_n_Sig.

Theorem SATn_SAT_reduction (Σ : fo_signature) (n : ) (r : rels Σ) (Hr : ar_rels _ r = n) :
      { f : fol_form (Σrel n) fol_form Σ
          | A, fo_form_fin_dec_SAT A fo_form_fin_dec_SAT (f A) }.
Proof. subst n; apply SATn_SAT_red. Qed.