(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

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.

(* * From binary singleton to n-ary singleton with n >= 2 *)

Local Notation ø := vec_nil.

(* The reduction could be made to work for (infinite) SAT only *)

Section Sig2_Sig_n_encoding.

  Variable (n : ).

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

  (* The encoding is trivial here : replace R2(x,y) with Rn(x,y,...,y) *)

  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 ( _ £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) ( : fo_model Σ2 X) (Mn : fo_model Σn X).

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

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

    Hypothesis HP : x y, 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 .
      + 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)
              ( : fo_model Σ2 X)
              ( : finite_t X)
              ( : fo_model_dec )
              ( : X)
              ( : fol_sem A).

    Let Mn : fo_model Σn X.
    Proof.
      exists.
      + intros [].
      + intros []; simpl.
        intros v.
        exact (fom_rels 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, .
      exists. { intros [] ?; apply . }
      exists .
      revert .
      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 & & & & & ).
    apply Σ2_Σn_sound_loc with ( := ) ( := ); auto.
  Qed.


  Section completeness.

    Variables (X : Type)
              (Mn : fo_model Σn X)
              ( : finite_t X)
              ( : fo_model_dec Mn)
              ( : X)
              ( : fol_sem Mn (Σ2_Σn A)).

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


    Local Lemma Σ2_Σn_complete_loc : fo_form_fin_dec_SAT A.
    Proof.
      exists X, , .
      exists. { intros [] ?; apply . }
      exists .
      revert .
      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 & & & & ).
    apply Σ2_Σn_complete_loc with (Mn := Mn) ( := ); auto.
  Qed.


End Sig2_Sig_n_encoding.