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.

Import fol_notations.

Require Import Undecidability.Shared.ListAutomation.

Set Default Proof Using "Type".

Set Implicit Arguments.

Local Infix "∊" := In (at level 70, no associativity).
Local Infix "⊑" := incl (at level 70, no associativity).
Local Notation ø := vec_nil.


Section congruence.

  Variables (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
            (X : Type) (M : fo_model Σ X)
            (R : X -> X -> Prop).

  Infix "≈" := R.

  Definition Σ_congruence_wrt :=
          (forall s, s ls -> forall v w, (forall p, vec_pos v p vec_pos w p)
                                          -> fom_syms M s v fom_syms M s w)
       /\ (forall r, r lr -> forall v w, (forall p, vec_pos v p vec_pos w p)
                                          -> fom_rels M r v <-> fom_rels M r w).

End congruence.

Section fol_congruence.

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

  Section encode_congruence.

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

    Notation "x ≈ y" := (fom_rels M e (cast (x##y##ø) (eq_sym H_ae))).

    Local Fact fol_sem_e x y φ : fol_sem M φ (x y) = fo_term_sem M φ x fo_term_sem M φ y.
    Proof. simpl; f_equal; rewrite H_ae; simpl; auto. Qed.

    Let fol_syms_e x y : fol_syms (x y) = fo_term_syms x ++ fo_term_syms y.
    Proof. simpl; rewrite H_ae; simpl; auto; rewrite <- app_nil_end; auto. Qed.

    Let fol_rels_e x y : fol_rels (x y) = e::nil.
    Proof. auto. Qed.

    Local Definition fol_vec_equiv n := fol_vec_fa (vec_set_pos (fun p : pos n => £(pos2nat p+n) £(pos2nat p))).

    Local Fact fol_vec_equiv_syms n : fol_syms (fol_vec_equiv n) nil.
    Proof.
      unfold fol_vec_equiv.
      rewrite fol_syms_vec_fa.
      intros x; rewrite in_flat_map.
      intros (D & HD & H); revert H.
      apply vec_list_inv in HD.
      destruct HD as (p & ->).
      rew vec; rewrite fol_syms_e; simpl; tauto.
    Qed.

    Local Fact fol_vec_equiv_rels n : fol_rels (fol_vec_equiv n) e::nil.
    Proof.
      unfold fol_vec_equiv.
      rewrite fol_rels_vec_fa.
      intros x; rewrite in_flat_map.
      intros (D & HD & H); revert H.
      apply vec_list_inv in HD.
      destruct HD as (p & ->); rew vec.
    Qed.

    Local Fact fol_vec_equiv_sem n φ :
                fol_sem M φ (fol_vec_equiv n)
            <-> (forall p : pos n, φ (pos2nat p+n) φ (pos2nat p)).
    Proof.
      unfold fol_vec_equiv.
      rewrite fol_sem_vec_fa.
      fol equiv; intros p; rew vec.
      rewrite fol_sem_e; simpl; tauto.
    Qed.

    Section congr_syms.

      Variable (s : syms Σ).

      Let n := ar_syms _ s.

      Let A := fol_vec_equiv n.
      Let f : 𝕋 := in_fot s (vec_set_pos (fun p => £(pos2nat p))).
      Let g : 𝕋 := in_fot s (vec_set_pos (fun p => £(pos2nat p+n))).
      Let B := g f.

      Let HrA : fol_syms A nil. Proof. apply fol_vec_equiv_syms. Qed.
      Let HsA : fol_rels A e::nil. Proof. apply fol_vec_equiv_rels. Qed.

      Let HrB : fol_syms B s::nil.
      Proof.
        unfold B; simpl.
        rewrite H_ae; unfold eq_rect_r.
        intros x; do 2 (simpl; rewrite in_app_iff).
        do 2 rewrite in_concat_iff.
        intros [ | [ (l & Hx & H) | [ | [ (l & Hx & H) | [] ] ] ] ]; try tauto; revert Hx;
          apply vec_list_inv in H; destruct H as (p & ->); rew vec.
      Qed.

      Let HsB : fol_rels B e::nil.
      Proof. simpl; cbv; tauto. Qed.

      Local Definition congr_syms : 𝔽 := fol_mquant fol_fa n (fol_mquant fol_fa n (A B)).

      Local Fact congr_syms_syms : fol_syms congr_syms s::nil.
      Proof.
        unfold congr_syms.
        do 2 rewrite fol_syms_mquant.
        rewrite fol_syms_bin.
        apply incl_app; auto.
      Qed.

      Local Fact congr_syms_rels : fol_rels congr_syms e::nil.
      Proof.
        unfold congr_syms.
        do 2 rewrite fol_rels_mquant.
        rewrite fol_rels_bin.
        apply incl_app; auto.
      Qed.

      Local Definition congr_syms_spec φ :
               fol_sem M φ congr_syms
           <-> forall v w, (forall p, vec_pos v p vec_pos w p) -> fom_syms M s v fom_syms M s w.
      Proof.
        unfold congr_syms.
        rewrite fol_sem_mforall.
        fol equiv; intros v.
        rewrite fol_sem_mforall.
        fol equiv; intros w.
        rewrite fol_sem_bin_fix.
        fol equiv imp.
        + unfold A; rewrite fol_vec_equiv_sem.
          fol equiv; intros p; rew vec; simpl.
          fol equiv; repeat f_equal.
          * rewrite env_vlift_fix1, env_vlift_fix0; auto.
          * rewrite env_vlift_fix0; auto.
        + unfold B.
          rewrite fol_sem_e; simpl.
          apply fol_equiv_ext; repeat f_equal;
            apply vec_pos_ext; intros p; rew vec; rew fot.
          * rewrite env_vlift_fix1, env_vlift_fix0; auto.
          * rewrite env_vlift_fix0; auto.
      Qed.

    End congr_syms.

    Section congr_rels.

      Variable (r : rels Σ).

      Let n := ar_rels _ r.

      Let A := fol_vec_equiv n.
      Let B := @fol_atom Σ r (vec_set_pos (fun p => £(pos2nat p))).
      Let C := @fol_atom Σ r (vec_set_pos (fun p => £(pos2nat p+n))).

      Let HsA : fol_syms A nil. Proof. apply fol_vec_equiv_syms. Qed.
      Let HrA : fol_rels A e::nil. Proof. apply fol_vec_equiv_rels. Qed.

      Let HsB : fol_syms B nil.
      Proof.
        unfold B; simpl.
        intros x; rewrite in_flat_map.
        intros (t & H & Ht); revert Ht.
        apply vec_list_inv in H; destruct H as (p & ->); rew vec.
      Qed.

      Let HrB : fol_rels B r::nil.
      Proof. simpl; cbv; tauto. Qed.

      Let HsC : fol_syms C nil.
      Proof.
        unfold C; simpl.
        intros x; rewrite in_flat_map.
        intros (t & Ht & H); revert H.
        apply vec_list_inv in Ht.
        destruct Ht as (p & ->); rew vec; simpl; tauto.
      Qed.

      Let HrC : fol_rels C e::r::nil.
      Proof. simpl; cbv; tauto. Qed.

      Local Definition congr_rels : 𝔽 := fol_mquant fol_fa n (fol_mquant fol_fa n (A (C B))).

      Local Fact congr_rels_syms : fol_syms congr_rels nil.
      Proof.
        unfold congr_rels.
        do 2 rewrite fol_syms_mquant.
        repeat rewrite fol_syms_bin.
        repeat (apply incl_app; auto).
      Qed.

      Local Fact congr_rels_rels : fol_rels congr_rels e::r::nil.
      Proof.
        unfold congr_rels.
        do 2 rewrite fol_rels_mquant.
        repeat rewrite fol_rels_bin.
        repeat (apply incl_app; auto).
        intros x Hx; destruct (HrA _ Hx); try subst x; simpl; tauto.
      Qed.

      Local Definition congr_rels_spec φ :
             fol_sem M φ congr_rels
         <-> forall v w, (forall p, vec_pos v p vec_pos w p)
                      -> fom_rels M r v <-> fom_rels M r w.
      Proof.
        unfold congr_rels.
        rewrite fol_sem_mforall.
        fol equiv; intros v.
        rewrite fol_sem_mforall.
        fol equiv; intros w.
        simpl fol_sem at 1.
        fol equiv.
        + unfold A; rewrite fol_vec_equiv_sem.
          fol equiv; intros p; rew vec; simpl.
          fol equiv; repeat f_equal.
          * rewrite env_vlift_fix1, env_vlift_fix0; auto.
          * rewrite env_vlift_fix0; auto.
        + fol equiv iff; fol equiv; f_equal;
            apply vec_pos_ext; intros p; rew vec; rew fot.
          * rewrite env_vlift_fix1, env_vlift_fix0; auto.
          * rewrite env_vlift_fix0; auto.
      Qed.

    End congr_rels.

    Local Definition fol_congruent : 𝔽 :=
        fol_lconj (map congr_syms ls)
       fol_lconj (map congr_rels lr).

    Local Fact fol_congruent_syms : fol_syms fol_congruent ls.
    Proof.
      unfold fol_congruent.
      rewrite fol_syms_bin.
      repeat rewrite fol_syms_bigop; simpl.
      repeat apply incl_app; try (cbv; tauto).
      + intros s; rewrite in_flat_map.
        intros (A & HA & H); revert HA H.
        rewrite in_map_iff; intros (x & <- & Hx) H.
        apply congr_syms_syms in H; revert H.
        intros [ <- | [] ]; auto.
      + intros r; rewrite in_flat_map.
        intros (A & HA & H); revert HA H.
        rewrite in_map_iff; intros (x & <- & Hx) H.
        apply congr_rels_syms in H; revert H.
        intros [].
    Qed.

    Local Fact fol_congruent_rels : fol_rels fol_congruent lr.
    Proof using He.
      unfold fol_congruent.
      rewrite fol_rels_bin.
      repeat rewrite fol_rels_bigop; simpl.
      repeat apply incl_app; try (cbv; tauto).
      + intros s; rewrite in_flat_map.
        intros (A & HA & H); revert HA H.
        rewrite in_map_iff; intros (x & <- & Hx) H.
        apply congr_syms_rels in H; revert H.
        intros [ <- | [] ]; simpl; auto.
      + intros x; simpl.
        rewrite in_flat_map.
        intros (A & HA & H); revert HA H.
        rewrite in_map_iff; intros (y & <- & Hy) H.
        apply congr_rels_rels in H; revert H.
        intros [ | [ <- | [] ] ]; subst; auto.
    Qed.


    Local Fact fol_congruent_spec φ :
          fol_sem M φ fol_congruent
      <-> Σ_congruence_wrt ls lr M (fun x y => x y).
    Proof.
      unfold fol_congruent.
      rewrite fol_sem_bin_fix.
      do 2 rewrite fol_sem_lconj.
      fol equiv conj.
      + split.
        * intros H s Hs.
          apply (congr_syms_spec _ φ), H, in_map_iff.
          exists s; auto.
        * intros H f; rewrite in_map_iff.
          intros (s & <- & Hs).
          apply congr_syms_spec, H; auto.
      + split.
        * intros H r Hr.
          apply (congr_rels_spec _ φ), H, in_map_iff.
          exists r; auto.
        * intros H f; rewrite in_map_iff.
          intros (r & <- & Hr).
          apply congr_rels_spec, H; auto.
    Qed.

    Local Definition fol_equivalence :=
            ( £0 £0)
           (∀∀∀ £2 £1 £1 £0 £2 £0)
           (∀∀ £1 £0 £0 £1).

    Local Fact fol_equivalence_syms : fol_syms fol_equivalence = nil.
    Proof.
      unfold fol_equivalence.
      repeat (rewrite fol_syms_bin || rewrite fol_syms_quant).
      repeat rewrite fol_syms_e; auto.
    Qed.

    Local Fact fol_equivalence_rels : fol_rels fol_equivalence e::nil.
    Proof. simpl; cbv; tauto. Qed.

    Fact fol_equiv_spec φ :
           fol_sem M φ fol_equivalence <-> equiv _ (fun x y => x y).
    Proof.
      unfold fol_equivalence.
      repeat (rewrite fol_sem_bin_fix).
      repeat fol equiv conj.
      + rewrite fol_sem_quant_fix; apply forall_equiv; intro.
        rewrite fol_sem_e; simpl; tauto.
      + do 3 (rewrite fol_sem_quant_fix; apply forall_equiv; intro).
        do 2 rewrite fol_sem_bin_fix.
        do 3 rewrite fol_sem_e; simpl; tauto.
      + do 2 (rewrite fol_sem_quant_fix; apply forall_equiv; intro).
        rewrite fol_sem_bin_fix.
        do 2 rewrite fol_sem_e; simpl; tauto.
    Qed.


    Definition fol_congruence :=
          fol_congruent
         fol_equivalence.

    Fact fol_congruence_syms : fol_syms fol_congruence ls.
    Proof.
      unfold fol_congruence.
      rewrite fol_syms_bin, fol_equivalence_syms, <- app_nil_end.
      apply fol_congruent_syms.
    Qed.

    Fact fol_congruence_rels : fol_rels fol_congruence lr.
    Proof using He.
      unfold fol_congruence.
      rewrite fol_rels_bin.
      apply incl_app.
      + apply fol_congruent_rels.
      + intros x Hx.
        apply fol_equivalence_rels in Hx.
        destruct Hx as [ | [] ]; subst; auto.
    Qed.

    Fact fol_sem_congruence φ :
             fol_sem M φ fol_congruence
         <-> Σ_congruence_wrt ls lr M (fun x y => x y)
          /\ equiv _ (fun x y => x y).
    Proof.
      fol equiv conj.
      + apply fol_congruent_spec.
      + apply fol_equiv_spec.
    Qed.

  End encode_congruence.

End fol_congruence.

Arguments fol_congruence { _ _ }.