(**************************************************************)
(*   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 utils decidable fol_ops fo_sig fo_terms fo_logic fo_sat.

Set Implicit Arguments.

Local Reserved Notation "⟪ A ⟫'" (at level 1, format "⟪ A ⟫'").

Local Notation ø := vec_nil.

Section remove_constants.

  Variable (Σ : fo_signature) (HΣ : forall s, ar_syms Σ s = 0)
           (ls : list (syms Σ)).

  Definition Σrem_cst : fo_signature.
  Proof.
    exists Empty_set (rels Σ).
    + intros [].
    + apply ar_rels.
  Defined.

  Notation Σ' := Σrem_cst.

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

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

  Implicit Type σ : syms Σ -> nat.

  Let convert_t σ (t : 𝕋) : 𝕋' :=
    match t with
      | in_var n => in_var n
      | in_fot s _ => in_var (σ s)
    end.

  Local Fixpoint encode σ (A : 𝔽) : 𝔽' :=
    match A with
      | ⊥ => ⊥
      | fol_atom r v => @fol_atom Σ' r (vec_map (convert_t σ) v)
      | fol_bin b A B => fol_bin b (encode σ A) (encode σ B)
      | fol_quant q A => fol_quant q (encode (fun s => S (σ s)) A)
    end.

  Section soundness.

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

    Definition Σrem_cst_model : fo_model Σ' X.
    Proof.
      split.
      + intros [].
      + apply (fom_rels M).
    Defined.

    Notation M' := Σrem_cst_model.

    Notation "⟪ A ⟫" := (fun φ => fol_sem M φ A).
    Notation "⟪ A ⟫'" := (fun ψ => fol_sem M' ψ A).

    Local Fact soundness σ (A : 𝔽) φ ψ :
            (forall s, In s ls -> In (σ s) (fol_vars A) -> False)
         -> (forall n, In n (fol_vars A) -> φ n = ψ n)
         -> (forall s, In s ls -> ψ (σ s) = fom_syms M s (cast ø (eq_sym (HΣ s))))
         -> incl (fol_syms A) ls
         -> ⟪A⟫ φ <-> ⟪encode σ A⟫' ψ.
    Proof.
      induction A as [ | r v | b A HA B HB | q A HA ] in σ, φ, ψ |- *;
        intros H1 H2 H3 H4; simpl; try tauto.
      + rewrite vec_map_map.
        apply fol_equiv_ext; f_equal.
        apply vec_pos_ext; intro p; rew vec.
        cut (incl (fo_term_syms (vec_pos v p)) ls).
        2:{ intros s Hs; apply H4; simpl; apply in_flat_map.
            exists (vec_pos v p); split; auto.
            apply in_vec_list, in_vec_pos. }
        cut (forall n, In n (fo_term_vars (vec_pos v p)) -> φ n = ψ n).
        2:{ intros n Hn; apply H2, in_flat_map.
            exists (vec_pos v p); split; auto.
            apply in_vec_list, in_vec_pos. }
        generalize (vec_pos v p); intros [ n | s w ] H5 H6; simpl.
        - apply H5; simpl; auto.
        - rewrite H3; f_equal; auto.
          2: apply H6; rew fot; simpl; auto.
          clear H5 H6.
          revert w; rewrite HΣ; intros w.
          vec nil w; auto.
      + apply fol_bin_sem_ext.
        * apply HA; auto.
          - intros s G1 G2; apply (H1 _ G1), in_app_iff; auto.
          - intros; apply H2, in_app_iff; auto.
          - intros ? ?; apply H4, in_app_iff; auto.
        * apply HB; auto.
          - intros s G1 G2; apply (H1 _ G1), in_app_iff; auto.
          - intros; apply H2, in_app_iff; auto.
          - intros ? ?; apply H4, in_app_iff; auto.
      + apply fol_quant_sem_ext; intros x.
        apply HA; auto.
        * intros s G1 G2; apply (H1 _ G1).
          simpl; apply in_flat_map.
          exists (S (σ s)); simpl; auto.
        * intros [|n] Hn; simpl; auto.
          apply H2; simpl; apply in_flat_map.
          exists (S n); simpl; auto.
    Qed.

  End soundness.

  Section completeness.

    Variable (X : Type) (M' : fo_model Σ' X).

    Definition Σadd_cst_model σ (ψ : nat -> X) : fo_model Σ X.
    Proof.
      split.
      + intros s _; exact (ψ (σ s)).
      + apply (fom_rels M').
    Defined.

    Notation M := Σadd_cst_model.

    Local Fact completeness σ (A : 𝔽) φ ψ :
            (forall s, In s ls -> In (σ s) (fol_vars A) -> False)
         -> (forall n, In n (fol_vars A) -> φ n = ψ n)
         -> incl (fol_syms A) ls
         -> fol_sem (Σadd_cst_model σ ψ) φ A
        <-> fol_sem M' ψ (encode σ A).
    Proof.
      induction A as [ | r v | b A HA B HB | q A HA ] in σ, φ, ψ |- *;
      intros H1 H2 H3; simpl; try tauto.
      + rewrite vec_map_map.
        apply fol_equiv_ext; f_equal.
        apply vec_pos_ext; intro p; rew vec.
        cut (incl (fo_term_syms (vec_pos v p)) ls).
        2:{ intros s Hs; apply H3; simpl; apply in_flat_map.
            exists (vec_pos v p); split; auto.
            apply in_vec_list, in_vec_pos. }
        cut (forall n, In n (fo_term_vars (vec_pos v p)) -> φ n = ψ n).
        2:{ intros n Hn; apply H2, in_flat_map.
            exists (vec_pos v p); split; auto.
            apply in_vec_list, in_vec_pos. }
        generalize (vec_pos v p); intros [ n | s w ] H5 H6; simpl; auto.
        apply H5; simpl; auto.
      + apply fol_bin_sem_ext.
        * apply HA; auto.
          - intros s G1 G2; apply (H1 _ G1), in_app_iff; auto.
          - intros; apply H2, in_app_iff; auto.
          - intros ? ?; apply H3, in_app_iff; auto.
        * apply HB; auto.
          - intros s G1 G2; apply (H1 _ G1), in_app_iff; auto.
          - intros; apply H2, in_app_iff; auto.
          - intros ? ?; apply H3, in_app_iff; auto.
      + apply fol_quant_sem_ext; intros x.
        rewrite <- HA with (φ := x·φ); unfold M; simpl; try tauto.
        * intros s G1 G2; apply (H1 _ G1).
          simpl; apply in_flat_map.
          exists (S (σ s)); simpl; auto.
        * intros [|n] Hn; simpl; auto.
          apply H2; simpl; apply in_flat_map.
          exists (S n); simpl; auto.
    Qed.

  End completeness.

End remove_constants.

Section reduction.

  Variable (Σ : fo_signature)
           (Σ0 : forall s, ar_syms Σ s = 0)
           (Σd : discrete (syms Σ)).

  Section syms_map.

    Variable A : fol_form Σ.

    Let ls := fol_syms A.
    Let K := list_discr_pos_n Σd ls.

    Let n := projT1 K.
    Let v : vec _ n := projT1 (projT2 K).
    Let g : _ -> option (pos n) := proj1_sig (projT2 (projT2 K)).

    Let HK := proj2_sig (projT2 (projT2 K)).

    Let H1 x : in_vec x v <-> In x ls.
    Proof. apply (proj1 HK). Qed.

    Let H2 x : In x ls <-> g x <> None.
    Proof. apply (proj1 (proj2 HK)). Qed.

    Let H3 p : g (vec_pos v p) = Some p.
    Proof. apply (proj1 (proj2 (proj2 HK))). Qed.

    Let H4 x p : g x = Some p -> vec_pos v p = x.
    Proof. apply (proj2 (proj2 (proj2 HK))). Qed.

    Let σ s :=
      match g s with
        | Some p => pos2nat p
        | None => 0
      end.

    Let f x : option (syms Σ) :=
      match le_lt_dec n x with
        | left _ => None
        | right H => Some (vec_pos v (nat2pos H))
      end.

    Let Hfσ s : In s ls -> f (σ s) = Some s.
    Proof.
      rewrite H2.
      unfold f, σ.
      generalize (H4 s).
      destruct (g s) as [ p | ].
      + intros E _.
        specialize (E _ eq_refl); subst.
        generalize (pos2nat_prop p).
        destruct (le_lt_dec n (pos2nat p)) as [ | H ].
        * intros; exfalso; lia.
        * rewrite nat2pos_pos2nat; auto.
      + intros _ []; auto.
    Qed.

    Local Fact syms_map : { σ : syms Σ -> nat &
                          { f : nat -> option (syms Σ) |
                            forall s, In s ls -> f (σ s) = Some s } }.
    Proof. exists σ, f; auto. Qed.

  End syms_map.

  Hint Resolve incl_refl : core.

  Theorem Sig_rem_cst_dep_red A : { B | @fo_form_fin_dec_SAT Σ A <-> @fo_form_fin_dec_SAT (Σrem_cst Σ) B }.
  Proof.
    generalize (fol_vars_max_spec A).
    set (m := fol_vars_max A); intros Hm.
    destruct (syms_map A) as (g & f & Hfg).
    set (σ s := g s + S m).
    exists (encode σ A).
    split.
    + intros (X & M & G1 & G2 & phi & G3).
      exists X, (Σrem_cst_model M), G1.
      exists. { intros r; simpl; apply G2. }
      set (psi n :=
        match le_lt_dec (S m) n with
          | left _ =>
          match f (n - S m) with
            | Some s => fom_syms M s (cast ø (eq_sym (Σ0 _)))
            | None => phi 0
          end
          | right _ => phi n
        end).
      exists psi.
      revert G3; apply soundness with (HΣ := Σ0) (ls := fol_syms A); auto.
      * intros s Hs; unfold σ; intros H.
        apply Hm in H; lia.
      * intros n Hn; apply Hm in Hn.
        unfold psi.
        destruct (le_lt_dec (S m) n); try lia; auto.
      * intros s Hs.
        unfold psi, σ.
        apply Hfg in Hs.
        replace (g s + S m - S m) with (g s) by lia.
        rewrite Hs.
        destruct (le_lt_dec (S m) (g s + S m)); auto; lia.
    + intros (X & M' & G1 & G2 & psi & G3).
      exists X, (Σadd_cst_model M' σ psi), G1.
      exists. { intros r; simpl; apply G2. }
      exists psi.
      revert G3; apply completeness with (ls := fol_syms A); auto.
      intros s Hs; unfold σ; intros H.
      apply Hm in H; lia.
  Qed.

End reduction.