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 fol_ops fo_sig fo_terms fo_logic fo_sat Sig_no_syms.

Set Implicit Arguments.


Fixpoint find_non_empty_word X (l : list (list X)) : { s & { w | In (s::w) l } } + { concat l = nil }.
Proof.
  destruct l as [ | [ | s w ] l ].
  + right; auto.
  + destruct (find_non_empty_word X l) as [ (s & w & H) | H ].
    * left; exists s, w; right; auto.
    * right; simpl; auto.
  + left; exists s, w; left; auto.
Qed.

Local Notation ø := vec_nil.

Section fot_word_var.


  Variable (X : Type).

  Implicit Type t : fo_term (fun _ : X => 1).

  Fixpoint fot_var t :=
    match t with
      | in_var i => i
      | in_fot s v => fot_var (vec_pos v pos0)
    end.

  Fixpoint fot_word t :=
    match t with
      | in_var i => nil
      | in_fot s v => s::fot_word (vec_pos v pos0)
    end.

  Fixpoint fot_word_var w i : fo_term (fun _ : X => 1) :=
    match w with
      | nil => in_var i
      | s::w => in_fot s (fot_word_var w i##ø)
    end.

  Fact fot_word_var_eq t : t = fot_word_var (fot_word t) (fot_var t).
  Proof.
    induction t as [ | s v IH ]; simpl in *; auto; f_equal.
    generalize (IH pos0); clear IH; vec split v with t; vec nil v; clear v; simpl.
    intro; f_equal; auto.
  Qed.

  Fact fot_word_eq w i : fot_word (fot_word_var w i) = w.
  Proof. induction w; simpl; f_equal; auto. Qed.

  Fact fot_var_eq w i : fot_var (fot_word_var w i) = i.
  Proof. induction w; simpl; f_equal; auto. Qed.

End fot_word_var.

Section Σ11_words.

  Variable (X Y : Type).


  Definition Σ11 : fo_signature.
  Proof.
    exists X Y; intros _.
    + exact 1.
    + exact 1.
  Defined.

  Fixpoint Σ11_words (A : fol_form Σ11) : list (list X) :=
    match A with
      | ⊥ => nil
      | fol_atom r v => (fot_word (vec_pos v pos0))::nil
      | fol_bin _ A B => Σ11_words A++Σ11_words B
      | fol_quant _ A => Σ11_words A
    end.

End Σ11_words.

Section Σfull_mon_rem.



  Variable (Y : Type) (HY : finite_t Y)
           (n m : nat).

  Notation X := (pos n).

  Let Yw := { w : list X | length w < S m }.

  Let YwY_fin : finite_t (Yw*Y).
  Proof.
    apply finite_t_prod; auto.
    apply finite_t_list, finite_t_pos.
  Qed.

  Let lwY := proj1_sig YwY_fin.
  Let HlwY p : In p lwY.
  Proof. apply (proj2_sig YwY_fin). Qed.


  Notation Σ := (Σ11 X Y).
  Notation Σ' := (Σ11 X (list X*Y + Y)).

  Fixpoint Σfull_mon_rec (A : fol_form Σ) : fol_form Σ' :=
    match A with
      | ⊥ => ⊥
      | fol_atom r v =>
        let w := fot_word (vec_head v) in
        let i := fot_var (vec_head v)
        in @fol_atom Σ' (inl (rev w,r)) (£i##ø)
      | fol_bin b A B => fol_bin b (Σfull_mon_rec A) (Σfull_mon_rec B)
      | fol_quant q A => fol_quant q (Σfull_mon_rec A)
    end.

  Fact Σfull_mon_rec_syms A : fol_syms (Σfull_mon_rec A) = nil.
  Proof.
    induction A as [ | r v | b A HA B HB | q A HA ].
    1,2,4: simpl; tauto.
    simpl; rewrite HA, HB; auto.
  Qed.

  Variable (A : fol_form Σ) (HwA : forall w, In w (Σ11_words A) -> length w < S m).


  Let Eq (p : Yw * Y) :=
    let (w,r) := p in
    let (w,_) := w in
    match w with
      | nil => @fol_atom Σ' (inl (nil,r)) (£0##ø)
               ↔ @fol_atom Σ' (inr r) (£0##ø)
      | s::w' => @fol_atom Σ' (inl (w',r)) (@in_fot _ (ar_syms Σ') s (£0##ø)##ø)
               ↔ @fol_atom Σ' (inl (w,r)) (£0##ø)
    end.


  Let Eq' (p : Yw * Y) :=
    let (w,r) := p in
    let (w,_) := w in
    match w with
      | nil => @fol_atom Σ' (inl (nil,r)) (£n##ø)
               ↔ @fol_atom Σ' (inr r) (£n##ø)
      | s::w' => @fol_atom Σ' (inl (w',r)) (£(pos2nat s)##ø)
               ↔ @fol_atom Σ' (inl (w,r)) (£n##ø)
    end.


  Definition Σfull_mon_red : fol_form Σ' :=
    Σfull_mon_rec A ⟑ ∀ fol_lconj (map Eq lwY).

  Variable (K : Type).

  Let Fixpoint f (M : fo_model Σ K) w x :=
    match w with
      | nil => x
      | s::w => f M w (fom_syms M s (x##ø))
    end.

  Let f_app M w1 w2 x : f M (w1++w2) x = f M w2 (f M w1 x).
  Proof. revert x; induction w1; simpl; auto. Qed.

  Let f_snoc M w s x : f M (w++s::nil) x = fom_syms M s (f M w x##ø).
  Proof. rewrite f_app; auto. Qed.

  Section soundness.

    Variable (M : fo_model Σ K).

    Let M' : fo_model Σ' K.
    Proof.
      split.
      + exact (fom_syms M).
      + intros [ (w,r) | r ]; simpl in r |- *.
        * exact (fun v => fom_rels M r (f M w (vec_head v)##ø)).
        * exact (fom_rels M r).
    Defined.

    Fact Σfull_mon_rec_sound φ :
         fol_sem M' φ (Σfull_mon_rec A) <-> fol_sem M φ A.
    Proof.
      revert φ HwA; induction A as [ | r v | b B HB C HC | q B HB ]; intros φ HA.
      + simpl; tauto.
      + simpl in v; unfold Σfull_mon_rec.
        revert HA; vec split v with t; vec nil v; clear v; simpl vec_head; simpl syms; intros HA.
        specialize (HA _ (or_introl eq_refl)); simpl in HA |- *.
        replace (fo_term_sem M φ t)
        with (fo_term_sem M φ (fot_word_var (fot_word t) (fot_var t))).
        * simpl; apply fol_equiv_ext; do 2 f_equal.
          generalize (fot_word t) (fot_var t); clear t HA; intros w.
          induction w as [ | s w IHw ]; simpl; auto; intros i.
          rewrite f_snoc; simpl; do 2 f_equal; auto.
        * f_equal; symmetry; apply fot_word_var_eq.
      + simpl; apply fol_bin_sem_ext.
        * apply HB; intros ? ?; apply HA, in_app_iff; auto.
        * apply HC; intros ? ?; apply HA, in_app_iff; auto.
      + simpl; apply fol_quant_sem_ext; intro; apply HB; auto.
    Qed.

    Variable (Kfin : finite_t K)
             (Mdec : fo_model_dec M)
             (φ : nat -> K)
             (HA : fol_sem M φ A).

    Theorem Σfull_mon_rem_sound : fo_form_fin_dec_SAT_in Σfull_mon_red K.
    Proof.
      exists M', Kfin.
      exists.
      { intros [ (w,r) | r ]; simpl in r |- *; intro; apply Mdec. }
      exists φ; simpl; split.
      + apply Σfull_mon_rec_sound; auto.
      + intro x; rewrite fol_sem_lconj.
        intros ?; rewrite in_map_iff.
        intros ((([|s w]&Hw),r) & <- & Hr); unfold Eq.
        * simpl; auto.
        * simpl; auto.
    Qed.

  End soundness.

  Section completeness.

    Variable (M' : fo_model Σ' K).

    Let M : fo_model Σ K.
    Proof.
      split.
      + exact (fom_syms M').
      + exact (fun r => fom_rels M' (inr r)).
    Defined.

    Section Σfull_mon_rec_complete.

      Hypothesis HM1' : forall s w r x, length (s::w) < S m
                                 -> fom_rels M' (inl (s::w, r)) (x##ø)
                                <-> fom_rels M' (inl (w, r)) (fom_syms M s (x##ø)##ø).

      Hypothesis HM2' : forall r x, fom_rels M' (inr r) (x##ø)
                                <-> fom_rels M' (inl (nil,r)) (x##ø).

      Let Hf φ w i : f M (rev w) (φ i) = fo_term_sem M φ (fot_word_var w i).
      Proof.
        induction w; simpl; auto.
        rewrite f_snoc; simpl in *; rewrite IHw; auto.
      Qed.

      Fact Σfull_mon_rec_complete φ :
        fol_sem M' φ (Σfull_mon_rec A) <-> fol_sem M φ A.
      Proof.
        revert φ HwA; induction A as [ | r v | b B HB C HC | q B HB ]; intros φ HwA.
        + simpl; tauto.
        + simpl in v; unfold Σfull_mon_rec.
          revert HwA; vec split v with t; vec nil v; clear v; simpl vec_head; simpl syms; intros HwA.
          specialize (HwA _ (or_introl eq_refl)); simpl in HwA |- *.
          replace (fo_term_sem M φ t)
          with (fo_term_sem M φ (fot_word_var (fot_word t) (fot_var t))).
          * revert HwA; generalize (fot_word t) (fot_var t); intros w i.
            rewrite <- (rev_length w), <- Hf.
            simpl; generalize (rev w) (φ i); clear w; intros w.
            induction w as [ | s w IHw ]; simpl; auto; intros Hw x.
            - rewrite HM2'; tauto.
            - rewrite HM1', IHw; simpl; try tauto; lia.
          * f_equal; symmetry; apply fot_word_var_eq.
        + apply fol_bin_sem_ext.
          * apply HB; intros ? ?; apply HwA, in_app_iff; auto.
          * apply HC; intros ? ?; apply HwA, in_app_iff; auto.
        + simpl; apply fol_quant_sem_ext; intro; apply HB; auto.
      Qed.

    End Σfull_mon_rec_complete.

    Variable (Kfin : finite_t K)
             (M'dec : fo_model_dec M')
             (φ : nat -> K)
             (HA : fol_sem M' φ Σfull_mon_red).

    Theorem Σfull_mon_rem_complete : fo_form_fin_dec_SAT_in A K.
    Proof.
      exists M, Kfin.
      exists.
      { intros r'; simpl in r'; intros v; apply M'dec. }
      exists φ; simpl.
      destruct HA as [ H1 H2 ].
      revert H1; apply Σfull_mon_rec_complete.
      + intros s w r x Hw.
        simpl in H2; specialize (H2 x).
        rewrite fol_sem_lconj in H2.
        symmetry; apply (H2 (Eq (exist _ (s::w) Hw,r))), in_map_iff.
        exists (exist _ (s::w) Hw,r); split; auto.
      + intros r x.
        simpl in H2; specialize (H2 x).
        rewrite fol_sem_lconj in H2.
        symmetry; apply (H2 (Eq (exist _ nil (lt_0_Sn _),r))), in_map_iff.
        exists (exist _ nil (lt_0_Sn _),r); split; auto.
    Qed.

  End completeness.


  Theorem Σfull_mon_red_correct : fo_form_fin_dec_SAT_in A K
                              <-> fo_form_fin_dec_SAT_in Σfull_mon_red K.
  Proof.
    split.
    + intros (M & H1 & H2 & phi & H3).
      apply Σfull_mon_rem_sound with M phi; auto.
    + intros (M' & H1 & H2 & phi & H3).
      apply Σfull_mon_rem_complete with M' phi; auto.
  Qed.


  Definition Σfull_mon_red' : fol_form Σ' :=
    Σfull_mon_rec A ⟑ ∀ fol_mquant fol_ex n (fol_lconj (map Eq' lwY)).

  Local Lemma Σfull_mon_red'_sound :
          fo_form_fin_dec_SAT_in Σfull_mon_red K
       -> fo_form_fin_dec_SAT_in Σfull_mon_red' K.
  Proof.
    intros (M & Kfin & Mdec & φ & H1 & H2); simpl in H1, H2.
    exists M, Kfin, Mdec, φ; simpl; split; auto.
    intros x; specialize (H2 x).
    rewrite fol_sem_mexists.
    exists (vec_set_pos (fun p => fom_syms M p (x##ø))).
    rewrite fol_sem_lconj; intros g; rewrite in_map_iff.
    intros (c & <- & Hg).
    rewrite fol_sem_lconj in H2.
    specialize (H2 (Eq c) (in_map _ _ _ Hg)).
    clear Hg; revert H2.
    destruct c as (([ | s w ],?),r); simpl.
    + rewrite env_vlift_fix1 with (k := 0); simpl; auto.
    + rewrite env_vlift_fix1 with (k := 0).
      rewrite env_vlift_fix0; simpl; rew vec.
  Qed.

  Section Σfull_mon_red'_complete.

    Variable (M : fo_model Σ' K)
             (Kfin : finite_t K)
             (Mdec : fo_model_dec M)
             (φ : nat -> K)
             (HA : fol_sem M φ Σfull_mon_red').

    Let R x (v : vec _ n) := fol_sem M (env_vlift x·φ v) (fol_lconj (map Eq' lwY)).

    Let Rreif : { f : K -> vec K n | forall x, R x (f x) }.
    Proof.
      apply finite_t_dec_choice.
      + apply finite_t_vec; auto.
      + intros x v; apply fol_sem_dec; auto.
      + simpl in HA; apply proj2 in HA.
        intros x; generalize (HA x).
        rewrite fol_sem_mexists; auto.
    Qed.

    Let g := proj1_sig Rreif.
    Let Hg x : fol_sem M (env_vlift x·φ (g x)) (fol_lconj (map Eq' lwY)).
    Proof. apply (proj2_sig Rreif). Qed.

    Let M' : fo_model Σ' K.
    Proof.
      split.
      + simpl; intros p v.
        exact (vec_pos (g (vec_head v)) p).
      + exact (fom_rels M).
    Defined.

    Local Lemma Σfull_mon_red'_complete : fo_form_fin_dec_SAT_in Σfull_mon_red K.
    Proof.
      exists M', Kfin, Mdec, φ.
      simpl; split.
      + simpl in HA; generalize (proj1 HA).
        apply fo_model_nosyms.
        * apply Σfull_mon_rec_syms.
        * intros; simpl; tauto.
      + intros x.
        specialize (Hg x).
        rewrite fol_sem_lconj in Hg.
        rewrite fol_sem_lconj.
        intros u; rewrite in_map_iff.
        intros (c & <- & Hc).
        specialize (Hg (Eq' c) (in_map _ _ _ Hc)).
        revert Hg.
        destruct c as (([|s w]&?),r); simpl.
        * rewrite env_vlift_fix1 with (k := 0); simpl; auto.
        * rewrite env_vlift_fix1 with (k := 0).
          rewrite env_vlift_fix0; simpl; rew vec.
    Qed.

  End Σfull_mon_red'_complete.


  Theorem Σfull_mon_red'_correct :
          fo_form_fin_dec_SAT_in A K
      <-> fo_form_fin_dec_SAT_in Σfull_mon_red' K.
  Proof.
    rewrite Σfull_mon_red_correct.
    split.
    + apply Σfull_mon_red'_sound.
    + intros (M & H1 & H2 & phi & H3).
      apply Σfull_mon_red'_complete with M phi; auto.
  Qed.


  Theorem Σfull_mon_red'_no_syms : fol_syms Σfull_mon_red' = nil.
  Proof.
    cut (incl (fol_syms Σfull_mon_red') nil).
    + generalize (fol_syms Σfull_mon_red').
      intros [ | x l ] H; auto.
      destruct (H x); simpl; auto.
    + simpl.
      rewrite Σfull_mon_rec_syms, fol_syms_mquant.
      rewrite fol_syms_bigop, <- app_nil_end; simpl.
      intros x; rewrite in_flat_map.
      intros (u & H & Hu); revert H.
      rewrite in_map_iff.
      intros (c & <- & Hc).
      revert Hu.
      destruct c as (([|s w]&?),r); simpl; auto.
  Qed.

End Σfull_mon_rem.

Section Σ11_reduction.


  Variable (n : nat) (Y : Type) (HY : finite_t Y) (A : fol_form (Σ11 (pos n) Y)) (K : Type).

  Let m := lmax (map (@length _) (Σ11_words A)).

  Let Hm w : In w (Σ11_words A) -> length w < S m.
  Proof.
    intros Hw; apply le_n_S, lmax_prop, in_map_iff.
    exists w; auto.
  Qed.

  Definition Σ11_red := Σfull_mon_red' HY m A.

  Theorem Σ11_red_correct : fo_form_fin_dec_SAT_in A K <-> fo_form_fin_dec_SAT_in Σ11_red K.
  Proof. apply Σfull_mon_red'_correct; auto. Qed.

  Theorem Σ11_red_no_syms : fol_syms Σ11_red = nil.
  Proof. apply Σfull_mon_red'_no_syms. Qed.

End Σ11_reduction.


Section Σ11_Σ1.

  Variable (n : nat) (Y : Type) (HY : finite_t Y) (A : fol_form (Σ11 (pos n) Y)).

  Theorem Σ11_Σ1_reduction : { B : fol_form (Σ11 Empty_set (list (pos n)*Y + Y))
                                 | fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT B }.
  Proof.
    destruct Σ_no_sym_correct with (A := Σ11_red HY A) as (B & HB).
    { rewrite Σ11_red_no_syms; apply incl_refl. }
    exists B; rewrite <- HB; split; intros (X & H); exists X; revert H; apply Σ11_red_correct.
  Qed.

End Σ11_Σ1.