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.

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 ( 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 ( p £ (pos2nat p))) in
            let wB := vec_set_pos ( 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 ( p £ (pos2nat p))) in
                 let wB := vec_set_pos ( 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 ( 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 & & ); revert .
        apply vec_list_inv in .
        destruct 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 φ ψ :
            ( 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 .
      + destruct M as (re,sy); simpl; rewrite ; tauto.
      + specialize ( p IHv p X M).
        rewrite fot_rem_syms_fix1.
        rewrite fol_sem_mexists.
        split.
        * intros .
          exists (vec_set_pos ( p fo_term_sem M (vec_pos v p))).
          destruct M as (sy,re); simpl; split.
          - simpl.
            replace (ar_syms _ s) with (0+ar_syms _ s) at 3 by .
            rewrite env_vlift_fix1; simpl; f_equal; rewrite ; 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 .
            rewrite env_vlift_fix1; auto.
        * intros (w & & ).
          destruct M as (sy,re); simpl.
          simpl in .
          replace (ar_syms _ s) with (0+ar_syms _ s) in at 2 by .
          rewrite env_vlift_fix1 in .
          rewrite ; clear .
          simpl; f_equal.
          apply vec_pos_ext; intros p; rew vec.
          rew fot.
          rewrite fol_sem_vec_fa in .
          specialize ( p); revert ; rew vec; intros .
          rewrite fol_sem_subst in .
          rewrite IHv with:= ) in ; auto.
          intros n; simpl.
          replace (n+1+ar_syms _ s) with ((S n)+ar_syms _ s) by .
          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 ( p £ (pos2nat p))) in
                             let wB := vec_set_pos ( 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 ( r inr (inl r)) (fol_syms A)
                  map ( 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 & & ) | [] ] ]; simpl; auto; revert .
        apply vec_list_inv in ; destruct as (p & ); rew vec; intros .
        rewrite fol_rels_subst in .
        apply fot_rem_syms_rels in ; simpl in .
        rewrite in_map_iff in .
        destruct as [ | (s' & & ) ]; 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 .
      + simpl; tauto.
      + simpl; rewrite fol_sem_mexists; split.
        * intros H; simpl in H |- *.
          exists (vec_map (fo_term_sem M ) 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 & & ); revert .
          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 .
          specialize ( p); revert ; 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 : 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 ( p £(pos2nat p)))
                      @fol_atom Σ' (inr (inl s)) (£n##vec_set_pos ( 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 ( v x fom_rels M (inr (inl s)) (x##v)).
  Proof.
    unfold fol_rel_fun; simpl; split.
    + intros H v x y .
      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 ; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
      * revert ; 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 ; apply H.
      * revert ; apply fol_equiv_ext; do 2 f_equal.
        apply vec_pos_ext; intros p; rew vec; rew fot.
        rewrite env_vlift_fix0; auto.
      * revert ; 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 ( p £(1+pos2nat p)))).

  Local Fact fol_rel_tot_spec s φ :
             fol_sem M φ (fol_rel_tot s)
          graph_tot ( 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 ( 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)
          s, In s ls is_graph_function ( 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 ( & M & & & & ).
  exists (fom_nosyms M), ; destruct M as (sy,re).
  exists.
  { intros [[]|[s|r]]; simpl.
    + intros; apply .
    + intros; apply .
    + intros; apply . }
  exists.
  { intros x y; cbv; tauto. }
  exists .
  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 ; apply fol_rem_syms_spec.
Qed.



Section completeness.

  Variable (Σ : fo_signature) (ls : list (syms Σ)) (A : fol_form Σ)
           (Hls : 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 : x y, fom_rels M e (x##y##ø) x = y)
             (φ : X)
             (HM : fol_sem M φ (Σsyms_Σnosyms ls A)).

    Let HF : s, In s ls is_graph_function ( 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 | 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 ( _ φ 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 := x x) (j := x x) (ls := nil)
             (lr := e :: map ( r inr (inl r)) (fol_syms A)
                       map ( 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 & & & & & ).
    cbn in .
    exists.
    { intros x y.
      generalize ( e (x##y##ø)).
      intros []; [ left | right ]; try red;
        rewrite ; auto. }
    exists (Σsyms_Σnosyms_rev_model ).
    exists .
    exists. { intros r v; simpl; apply . }
    exists .
    apply Σsyms_Σnosyms_complete_nested.
  Qed.


End completeness.