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 fol_ops fo_sig fo_terms fo_logic fo_sat.

Import fol_notations.

Set Implicit Arguments.


Local Notation ø := vec_nil.


Section Sig2_Sig_n_encoding.

  Variable (n : nat).

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


  Fixpoint Σ2_Σn (A : fol_form Σ2) : fol_form Σn :=
    match A with
      | ⊥ => ⊥
      | fol_atom _ v => let x := Σrel_var (vec_head v) in
                          let y := Σrel_var (vec_head (vec_tail v))
                          in @fol_atom Σn tt (£x##vec_set_pos (fun _ => £y))
      | fol_bin b A B => fol_bin b (Σ2_Σn A) (Σ2_Σn B)
      | fol_quant q A => fol_quant q (Σ2_Σn A)
     end.

  Section correctness.

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

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

    Let P2 a b := fom_rels M2 tt (a##b##ø).
    Let Pn a b := fom_rels Mn tt (a##vec_set_pos (fun _ => b)).

    Hypothesis HP : forall x y, P2 x y <-> Pn x y.

    Lemma Σ2_Σn_correct (A : fol_form Σ2) φ : ⟪ A ⟫ φ <-> ⟪Σ2_Σn A⟫' φ.
    Proof.
      revert φ.
      induction A as [ | [] v | b A HA B HB | q A HA ]; intros phi.
      + simpl; tauto.
      + vec split v with a; vec split v with b; vec nil v; clear v; revert a b.
        intros [ a | [] ] [ b | [] ]; unfold Σ2_Σn; simpl; rew fot.
        rewrite vec_map_set_pos; apply HP.
      + simpl; apply fol_bin_sem_ext; auto.
      + simpl; apply fol_quant_sem_ext; intro; auto.
    Qed.

  End correctness.

  Variable (A : fol_form Σ2).

  Section soundness.

    Variables (X : Type)
              (M2 : fo_model Σ2 X)
              (H1 : finite_t X)
              (H2 : fo_model_dec M2)
              (phi : nat -> X)
              (H3 : fol_sem M2 phi A).

    Let Mn : fo_model Σn X.
    Proof.
      exists.
      + intros [].
      + intros []; simpl.
        intros v.
        exact (fom_rels M2 tt (vec_head v##vec_head (vec_tail v)##ø)).
    Defined.

    Local Lemma Σ2_Σn_sound_loc : fo_form_fin_dec_SAT (Σ2_Σn A).
    Proof.
      exists X, Mn, H1.
      exists. { intros [] ?; apply H2. }
      exists phi.
      revert H3.
      apply Σ2_Σn_correct; simpl; tauto.
    Qed.

  End soundness.

  Lemma Σ2_Σn_soundness :
        fo_form_fin_dec_SAT A
     -> fo_form_fin_dec_SAT (Σ2_Σn A).
  Proof.
    intros (X & M2 & H1 & H2 & phi & H3).
    apply Σ2_Σn_sound_loc with (M2 := M2) (phi := phi); auto.
  Qed.

  Section completeness.

    Variables (X : Type)
              (Mn : fo_model Σn X)
              (H1 : finite_t X)
              (H2 : fo_model_dec Mn)
              (phi : nat -> X)
              (H3 : fol_sem Mn phi (Σ2_Σn A)).

    Let M2 : fo_model Σ2 X.
    Proof.
      exists.
      + intros [].
      + intros []; simpl.
        intros v.
        exact (fom_rels Mn tt (vec_head v##vec_set_pos (fun _ => vec_head (vec_tail v)))).
    Defined.

    Local Lemma Σ2_Σn_complete_loc : fo_form_fin_dec_SAT A.
    Proof.
      exists X, M2, H1.
      exists. { intros [] ?; apply H2. }
      exists phi.
      revert H3.
      apply Σ2_Σn_correct; simpl; tauto.
    Qed.

  End completeness.

  Lemma Σ2_Σn_completeness :
        fo_form_fin_dec_SAT (Σ2_Σn A)
     -> fo_form_fin_dec_SAT A.
  Proof.
    intros (X & Mn & H1 & H2 & phi & H3).
    apply Σ2_Σn_complete_loc with (Mn := Mn) (phi := phi); auto.
  Qed.

End Sig2_Sig_n_encoding.