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.

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 remove_interpreted_symbol.

  Variables (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
            (e : rels Σ) (H_ae : ar_rels _ e = 2) (He : 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.


    Hint Resolve finite_t_pos : core.

    Variable (A : 𝔽)
             (HA1 : fol_syms A ⊑ ls)
             (HA2 : 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
        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.