(**************************************************************)
(*   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 Lia Relations.

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_congruence fo_sat.

Set Implicit Arguments.

FSATEQ reduces to FSAT

1/ A is satisfiable in a fin/dec/interpreted model iff f(A) if satisfiable in a fin/dec model

2/ A is satisfiable in a fin/dec iff f(A) if satisfiable in a fin/dec/interpreted model

for 2/ simply add an equality symbol that is not in A and do not use it and interpret it as =. f(A) is same as A but in an upgraded signature

for 1/ A over Σ may contain an identity symbol e the idea ... given ls and lr containing the syms and rels belongs of A, and also e,

Of course if A is satisfiable interpreted that A is satisfiable (uninterpreted). No suppose A is satisfiable uninterpreted, how can we ensure that e is interpreted by equality in the compressed model.

For this we add formulas stating that e is a congruence for any on the symbols and rels in ls/lr so that in the compressed model, e will ensure bisimilarity and thus equality.

Section remove_interpreted_symbol.

  Variables (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
            (e : rels Σ) (H_ae : ar_rels _ e = 2) (He : In e lr).

  Notation 𝕋 := (fol_term Σ).
  Notation 𝔽 := (fol_form Σ).

  Notation "x ≡ y" := (@fol_atom Σ e (cast (x##y##ø) (eq_sym H_ae))) (at level 59).

  Definition Σ_noeq A := fol_congruence H_ae ls lr ⟑ A.

  Section soundness.

    Variable (A : 𝔽) (X : Type).

    Theorem Σ_noeq_sound :
               fo_form_fin_dec_eq_SAT_in _ H_ae A X
            -> fo_form_fin_dec_SAT_in (Σ_noeq A) X.
    Proof.
      intros (M & H1 & H2 & HE & phi & H5).
      exists M, H1, H2, phi; unfold Σ_noeq.
      rewrite fol_sem_bin_fix; split; auto.
      rewrite fol_sem_congruence.
      split; [ | msplit 2 ].
      + split.
        * intros s _ v w H; rewrite HE.
          f_equal; apply vec_pos_ext; intros p.
          apply HE, H.
        * intros r _ v w H.
          apply fol_equiv_ext; f_equal.
          apply vec_pos_ext; intros p.
          apply HE, H.
      + intros ?; rewrite HE; auto.
      + intros ? ? ?; rewrite !HE; intros; subst; auto.
      + intros ? ?; rewrite !HE; intros; subst; auto.
    Qed.

  End soundness.

  Section completeness.

    (* Not sure how to make this one work over infinite models
       Need some replacement for the quotient below *)

    Hint Resolve finite_t_pos : core.

    Variable (A : 𝔽)
             (HA1 : incl (fol_syms A) ls)
             (HA2 : incl (fol_rels A) lr).

    Theorem Σ_noeq_complete :
               fo_form_fin_dec_SAT (Σ_noeq A)
            -> fo_form_fin_dec_eq_SAT e H_ae A.
    Proof.
      intros (X & M & H1 & H2 & phi & H5 & H3).
      apply fol_sem_congruence in H5.
      destruct H5 as ((H4 & H5) & (H6 & H8 & H7)).
      set (R x y := fom_rels M e (cast (x ## y ## ø) (eq_sym H_ae))).
      destruct H1 as (lX & HlX).
      destruct decidable_EQUIV_fin_quotient with (l := lX) (R := R)
        as [ n cls repr G1 G2 ]; auto.
      + intros; apply H2.
      + intros x; exists x; split; auto; apply H6.
      + exists (pos n).
        set (Mn := Mk_fo_model Σ
               (fun s v => cls (fom_syms M s (vec_map repr v)))
               (fun r v => fom_rels M r (vec_map repr v))).
        exists Mn.
        exists; auto.
        exists. { intros r v; apply H2. }
        exists.
        { intros p q.
          unfold Mn; simpl.
          rewrite cast_fun; simpl.
          unfold R in G2; rewrite G2, !G1; tauto. }
        exists (fun n => cls (phi n)).
        revert H3.
        apply fo_model_projection' with (i := cls) (j := repr) (ls := ls) (lr := lr); auto.
        * intros s v Hs; simpl; apply G2.
          rewrite vec_map_map; red.
          apply H4; auto.
          intros p; rew vec; apply G2.
          rewrite G1; auto.
        * intros r v Hr; simpl.
          rewrite vec_map_map.
          apply H5; auto.
          intros p; rew vec; apply G2.
          rewrite G1; auto.
    Qed.

  End completeness.

End remove_interpreted_symbol.