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

Import fol_notations.

Require Import Undecidability.Shared.ListAutomation.

Set Implicit Arguments.


Local Notation ø := vec_nil.

Section Sig_remove_symbols.

  Variable (Σ : fo_signature).


  Definition Σnosyms : fo_signature.
  Proof.
    exists Empty_set (unit + (syms Σ + rels Σ))%type.
    + intros [].
    + intros [ | [ s | r ] ].
      * exact 2.
      * exact (S (ar_syms _ s)).
      * exact (ar_rels _ r).
  Defined.

  Notation Σ' := Σnosyms.

  Let e : rels Σ' := inl tt.

  Local Definition fom_nosyms X : fo_model Σ X -> fo_model Σ' X.
  Proof.
    intros (F,R); split.
    + intros [].
    + intros [|[s|r]].
      * exact (rel2_on_vec eq).
      * exact (fun v => vec_head v = F _ (vec_tail v)).
      * exact (R r).
  Defined.

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

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

  Section removing_symbols_from_terms.

    Let f k (p : pos k) n : 𝕋' := match n with 0 => £ (pos2nat p) | S n => £ (n+1+k) end.

    Local Fixpoint fot_rem_syms (t : 𝕋) : 𝔽' :=
      match t with
        | in_var n => @fol_atom Σ' e (£0##£(S n)##ø)
        | in_fot s v =>
            let A := @fol_atom Σ' (inr (inl s)) (£(ar_syms _ s)##vec_set_pos (fun p => £ (pos2nat p))) in
            let wB := vec_set_pos (fun p => (fot_rem_syms (vec_pos v p))⦃f p⦄)
            in fol_mquant fol_ex (ar_syms _ s) (A ⟑ fol_vec_fa wB)
      end.

    Local Fact fot_rem_syms_fix0 n : fot_rem_syms (in_var n) = fol_atom e (£0##£(S n)##ø).
    Proof. trivial. Qed.

    Local Fact fot_rem_syms_fix1 s v :
                 fot_rem_syms (in_fot s v)
               = let A := @fol_atom Σ' (inr (inl s)) (£(ar_syms _ s)##vec_set_pos (fun p => £ (pos2nat p))) in
                 let wB := vec_set_pos (fun p => (fot_rem_syms (vec_pos v p))⦃f p⦄)
                 in fol_mquant fol_ex (ar_syms _ s) (A ⟑ fol_vec_fa wB).
    Proof. trivial. Qed.

    Opaque fo_term_syms.

    Local Fact fot_rem_syms_rels t : incl (fol_rels (fot_rem_syms t)) (e::map (fun x => inr (inl x)) (fo_term_syms t)).
    Proof.
      induction t as [ n | s v IHv ].
      + rewrite fot_rem_syms_fix0; cbv; tauto.
      + rewrite fot_rem_syms_fix1; simpl.
        rewrite fol_rels_mquant; simpl.
        unfold fol_vec_fa.
        rewrite fol_rels_bigop.
        intros r; simpl.
        rewrite in_app_iff, in_map_iff, in_flat_map.
        intros [ <- | [ H | [] ] ]; auto.
        { right; exists s; auto; rew fot; simpl; auto. }
        revert H; intros (A & H1 & H2); revert H2.
        apply vec_list_inv in H1.
        destruct H1 as (p & ->); rew vec.
        rewrite fol_rels_subst.
        intros H; apply IHv in H; revert H.
        simpl; rewrite in_map_iff.
        intros [ <- | (s' & <- & Hs') ]; auto.
        right; exists s'; split; auto; rew fot.
        right; rewrite in_flat_map.
        exists (vec_pos v p); split; auto.
        apply in_vec_list, in_vec_pos.
    Qed.

    Local Fact fot_rem_syms_spec t X M φ ψ :
            (forall n, φ n = ψ (S n))
         -> ψ 0 = fo_term_sem M φ t
        <-> fol_sem (@fom_nosyms X M) ψ (fot_rem_syms t).
    Proof.
      revert X M φ ψ.
      induction t as [ n | s v IHv ]; intros X M phi psi H2.
      + destruct M as (re,sy); simpl; rewrite <- H2; tauto.
      + specialize (fun p => IHv p X M).
        rewrite fot_rem_syms_fix1.
        rewrite fol_sem_mexists.
        split.
        * intros H3.
          exists (vec_set_pos (fun p => fo_term_sem M phi (vec_pos v p))).
          destruct M as (sy,re); simpl; split.
          - simpl.
            replace (ar_syms _ s) with (0+ar_syms _ s) at 3 by lia.
            rewrite env_vlift_fix1; simpl; f_equal; rewrite H3; simpl; f_equal.
            apply vec_pos_ext; intros p; rew vec; rew fot.
            rewrite env_vlift_fix0; rew vec.
          - simpl.
            rewrite fol_sem_vec_fa; intros p.
            rew vec.
            rewrite fol_sem_subst.
            rewrite <- IHv; auto.
            2: reflexivity.
            simpl; rew fot.
            rewrite env_vlift_fix0; rew vec.
            apply fo_term_sem_ext; intros n Hn.
            replace (n+1+ar_syms _ s) with ((S n)+ar_syms _ s) by lia.
            rewrite env_vlift_fix1; auto.
        * intros (w & Hw1 & Hw2).
          destruct M as (sy,re); simpl.
          simpl in Hw1.
          replace (ar_syms _ s) with (0+ar_syms _ s) in Hw1 at 2 by lia.
          rewrite env_vlift_fix1 in Hw1.
          rewrite Hw1; clear Hw1.
          simpl; f_equal.
          apply vec_pos_ext; intros p; rew vec.
          rew fot.
          rewrite fol_sem_vec_fa in Hw2.
          specialize (Hw2 p); revert Hw2; rew vec; intros Hw2.
          rewrite fol_sem_subst in Hw2.
          rewrite <- IHv with (φ := phi) in Hw2; auto.
          intros n; simpl.
          replace (n+1+ar_syms _ s) with ((S n)+ar_syms _ s) by lia.
          rewrite env_vlift_fix1; auto.
    Qed.

  End removing_symbols_from_terms.

  Section and_now_from_formulas.

    Let f k (p : pos k) n : 𝕋' := match n with 0 => £ (pos2nat p) | S n => £ (n+k) end.

    Local Fixpoint fol_rem_syms A : 𝔽' :=
      match A with
        | ⊥ => ⊥
        | fol_atom r v => let A := @fol_atom Σ' (inr (inr r)) (vec_set_pos (fun p => £ (pos2nat p))) in
                             let wB := vec_set_pos (fun p => (fot_rem_syms (vec_pos v p))⦃f p⦄)
                             in fol_mquant fol_ex (ar_rels _ r) (A ⟑ fol_vec_fa wB)
        | fol_bin c A B => fol_bin c (fol_rem_syms A) (fol_rem_syms B)
        | fol_quant q A => fol_quant q (fol_rem_syms A)
      end.

    Local Fact fol_rem_syms_rels A :
         incl (fol_rels (fol_rem_syms A))
              (e :: map (fun r => inr (inl r)) (fol_syms A)
                 ++ map (fun r => inr (inr r)) (fol_rels A)).
    Proof.
      induction A as [ | r v | b A IHA B IHB | q A IHA ].
      + cbv; tauto.
      + simpl.
        rewrite fol_rels_mquant; simpl.
        unfold fol_vec_fa.
        rewrite fol_rels_bigop.
        intros s; simpl; rewrite in_app_iff, in_flat_map, in_app_iff.
        intros [ <- | [ (A & H1 & H2) | [] ] ]; simpl; auto; revert H2.
        apply vec_list_inv in H1; destruct H1 as (p & ->); rew vec; intros H1.
        rewrite fol_rels_subst in H1.
        apply fot_rem_syms_rels in H1; simpl in H1.
        rewrite in_map_iff in H1.
        destruct H1 as [ | (s' & <- & H1) ]; auto.
        right; left; apply in_map_iff.
        exists s'; split; auto.
        apply in_flat_map.
        exists (vec_pos v p); split; auto.
        apply in_vec_list, in_vec_pos.
      + intros r; simpl.
        repeat rewrite map_app.
        repeat rewrite in_app_iff.
        intros [ H | H ].
        * apply IHA in H; revert H; simpl.
          rewrite in_app_iff; tauto.
        * apply IHB in H; revert H; simpl.
          rewrite in_app_iff; tauto.
      + intros r; simpl.
        repeat rewrite map_app.
        repeat rewrite in_app_iff.
        intros H; apply IHA in H; revert H.
        simpl; rewrite in_app_iff; tauto.
    Qed.

    Local Fact fol_rem_syms_spec A X M φ :
           fol_sem M φ A
       <-> fol_sem (@fom_nosyms X M) φ (fol_rem_syms A).
    Proof.
      revert φ.
      induction A as [ | r v | b A IHA B IHB | q A IHA ]; intros phi.
      + simpl; tauto.
      + simpl; rewrite fol_sem_mexists; split.
        * intros H; simpl in H |- *.
          exists (vec_map (fo_term_sem M phi) v); split.
          - revert H; apply fol_equiv_ext.
            unfold fom_nosyms; destruct M as (re,sy); simpl; f_equal.
            apply vec_pos_ext; intros p; rew vec; rew fot.
            rewrite env_vlift_fix0; rew vec.
          - rewrite fol_sem_vec_fa; intros p; rew vec.
            rewrite fol_sem_subst; simpl.
            rewrite <- fot_rem_syms_spec; auto.
            2: intro; reflexivity.
            simpl.
            rewrite env_vlift_fix0; rew vec.
            apply fo_term_sem_ext.
            intros; rewrite env_vlift_fix1; auto.
        * intros (w & Hw1 & Hw2); revert Hw1.
          simpl; apply fol_equiv_ext.
          unfold fom_nosyms; destruct M as (re,sy); simpl; f_equal.
          apply vec_pos_ext; intros p; rew vec; rew fot.
          rewrite env_vlift_fix0.
          rewrite fol_sem_vec_fa in Hw2.
          specialize (Hw2 p); revert Hw2; rew vec.
          rewrite fol_sem_subst, <- fot_rem_syms_spec; auto.
          2: intro; reflexivity.
          simpl; rewrite env_vlift_fix0.
          intros ->; apply fo_term_sem_ext.
          intros; rewrite env_vlift_fix1; auto.
      + simpl; apply fol_bin_sem_ext; auto.
      + simpl; apply fol_quant_sem_ext.
        intro; auto.
    Qed.

  End and_now_from_formulas.

  Variable (X : Type) (M : fo_model Σ' X)
           (HM : forall x y, fom_rels M e (x##y##ø) <-> x = y)
           .

  Local Definition fol_rel_fun (s : syms Σ) : 𝔽' :=
       let n := ar_syms _ s
       in ∀∀ fol_mquant fol_fa n (
             @fol_atom Σ' (inr (inl s)) (£(S n)##vec_set_pos (fun p => £(pos2nat p)))
                     ⤑ @fol_atom Σ' (inr (inl s)) (£n##vec_set_pos (fun p => £(pos2nat p)))
                     ⤑ @fol_atom Σ' e (£(S n)##£n##ø) ).

  Local Fact fol_rel_fun_spec s φ :
             fol_sem M φ (fol_rel_fun s)
         <-> graph_fun (fun v x => fom_rels M (inr (inl s)) (x##v)).
  Proof.
    unfold fol_rel_fun; simpl; split.
    + intros H v x y H1 H2.
      specialize (H x y).
      rewrite fol_sem_mforall in H.
      specialize (H v); simpl fol_sem in H.
      rewrite env_vlift_fix1 with (k := 1) in H.
      rewrite env_vlift_fix1 with (k := 0) in H.
      rewrite HM in H; simpl in H.
      apply H.
      * revert H1; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
      * revert H2; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
    + intros H x y.
      rewrite fol_sem_mforall; intros v.
      specialize (H v x y); simpl in H.
      simpl.
      rewrite env_vlift_fix1 with (k := 1).
      rewrite env_vlift_fix1 with (k := 0).
      rewrite HM; simpl.
      intros H1 H2; apply H.
      * revert H1; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
      * revert H2; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
  Qed.

  Local Definition fol_rel_tot (s : syms Σ) : 𝔽' :=
        let n := ar_syms _ s
        in fol_mquant fol_fa n (∃ @fol_atom Σ' (inr (inl s)) (£0##vec_set_pos (fun p => £(1+pos2nat p)))).

  Local Fact fol_rel_tot_spec s φ :
             fol_sem M φ (fol_rel_tot s)
         <-> graph_tot (fun v x => fom_rels M (inr (inl s)) (x##v)).
  Proof.
    unfold fol_rel_tot.
    rewrite fol_sem_mforall.
    apply forall_equiv; intros v; simpl.
    apply exists_equiv; intros x.
    apply fol_equiv_ext; do 2 f_equal.
    apply vec_pos_ext; intros p; rew vec; rew fot.
    simpl; rewrite env_vlift_fix0; auto.
  Qed.

  Local Definition fol_rels_are_functions ls :=
        fol_lconj (map (fun s => fol_rel_fun s ⟑ fol_rel_tot s) ls).

  Local Fact fol_rels_are_functions_spec ls φ :
             fol_sem M φ (fol_rels_are_functions ls)
         <-> forall s, In s ls -> is_graph_function (fun v x => fom_rels M (inr (inl s)) (x##v)).
  Proof.
    unfold fol_rels_are_functions.
    rewrite fol_sem_lconj; split.
    + intros H s Hs; red.
      rewrite <- fol_rel_tot_spec with (φ := φ).
      rewrite <- fol_rel_fun_spec with (φ := φ).
      apply (H (fol_rel_fun s ⟑ fol_rel_tot s)), in_map_iff.
      exists s; auto.
    + intros H B; rewrite in_map_iff.
      intros (s & <- & Hs); split.
      * apply fol_rel_fun_spec, H; auto.
      * apply fol_rel_tot_spec, H; auto.
  Qed.

  Definition Σsyms_Σnosyms ls A := fol_rels_are_functions ls ⟑ fol_rem_syms A.

End Sig_remove_symbols.



Theorem Σsyms_Σnosyms_sound Σ ls A X :
             fo_form_fin_discr_dec_SAT_in A X
          -> @fo_form_fin_dec_eq_SAT_in (Σnosyms Σ) (inl tt) eq_refl (Σsyms_Σnosyms ls A) X.
Proof.
  intros (H0 & M & H1 & H2 & phi & H3).
  exists (fom_nosyms M), H1; destruct M as (sy,re).
  exists.
  { intros [[]|[s|r]]; simpl.
    + intros; apply H0.
    + intros; apply H0.
    + intros; apply H2. }
  exists.
  { intros x y; cbv; tauto. }
  exists phi.
  unfold Σsyms_Σnosyms; split.
  + apply fol_rels_are_functions_spec; auto; simpl; try tauto.
    intros s Hs; split.
    * intros v x y; simpl; intros; subst; auto.
    * intros v; exists (sy s v); simpl; auto.
  + revert H3; apply fol_rem_syms_spec.
Qed.


Section completeness.

  Variable (Σ : fo_signature) (ls : list (syms Σ)) (A : fol_form Σ)
           (Hls : forall s, { In s ls } + { ~ In s ls })
           (HAls : incl (fol_syms A) ls).

  Notation Σ' := (Σnosyms Σ).

  Let e : rels Σ' := inl tt.

  Variable (X : Type).

  Section nested.

    Variable (M : fo_model Σ' X)
             (Xfin : finite_t X)
             (Mdec : fo_model_dec M)
             (He : forall x y, fom_rels M e (x##y##ø) <-> x = y)
             (φ : nat -> X)
             (HM : fol_sem M φ (Σsyms_Σnosyms ls A)).

    Let HF : forall s, In s ls -> is_graph_function (fun v x => fom_rels M (inr (inl s)) (x##v)).
    Proof.
      simpl in HM; apply proj1 in HM.
      rewrite fol_rels_are_functions_spec in HM; auto.
    Qed.

    Let HA : fol_sem M φ (fol_rem_syms A).
    Proof. simpl in HM; apply proj2 in HM; auto. Qed.

    Let F (s : syms Σ) : In s ls -> { f | forall v x, fom_rels M (inr (inl s)) (x##v) <-> x = f v }.
    Proof. intro; apply graph_tot_reif; auto. Qed.

    Local Definition Σsyms_Σnosyms_rev_model : fo_model Σ X.
    Proof.
      split.
      + intros s.
        destruct (Hls s) as [ H | H ].
        * exact (proj1_sig (F s H)).
        * exact (fun _ => φ 0).
      + intros r.
        exact (fom_rels M (inr (inr r))).
    Defined.

    Local Fact Σsyms_Σnosyms_complete_nested : fol_sem Σsyms_Σnosyms_rev_model φ A.
    Proof.
      apply fol_rem_syms_spec.
      revert HA.
      apply fo_model_projection' with (i := fun x => x) (j := fun x => x) (ls := nil)
             (lr := e :: map (fun r => inr (inl r)) (fol_syms A)
                      ++ map (fun r => inr (inr r)) (fol_rels A)); auto.
      + intros r v; simpl In; rewrite in_app_iff, in_map_iff, in_map_iff.
        intros [ <- | [ (s & <- & Hs) | (r' & <- & Hr') ] ]; simpl.
        * vec split v with x; vec split v with y; vec nil v; simpl.
          fold e; rewrite He; tauto.
        * destruct (Hls s) as [ H | H ]; try tauto.
          vec split v with x; simpl.
          rewrite <- (proj2_sig (F s H) v x).
          apply fol_equiv_ext; f_equal; f_equal.
          apply vec_pos_ext; intro; rew vec.
          destruct H; revert Hs; apply HAls.
        * apply fol_equiv_ext; f_equal; f_equal.
          apply vec_pos_ext; simpl; intros; rew vec.
          rewrite vec_pos_map; auto.
      + intros [].
      + apply fol_rem_syms_rels.
    Qed.

  End nested.

  Theorem Σsyms_Σnosyms_complete :
          @fo_form_fin_dec_eq_SAT_in (Σnosyms Σ) e eq_refl (Σsyms_Σnosyms ls A) X
       -> fo_form_fin_discr_dec_SAT_in A X.
  Proof.
    intros (M & H1 & H2 & H3 & phi & H5).
    cbn in H3.
    exists.
    { intros x y.
      generalize (H2 e (x##y##ø)).
      intros []; [ left | right ]; try red;
        rewrite <- H3; auto. }
    exists (Σsyms_Σnosyms_rev_model H1 H2 H3 H5).
    exists H1.
    exists. { intros r v; simpl; apply H2. }
    exists phi.
    apply Σsyms_Σnosyms_complete_nested.
  Qed.

End completeness.