(**************************************************************)
(*   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 Lia Max.

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.

Import fol_notations.

Set Implicit Arguments.

(* * Removal of function symbols from propositional signatures *)

Section Σ_Σ0.

  Variable (Σ : fo_signature)
           (HΣ : forall r, ar_rels Σ r = 0).

  Definition Σ0 : fo_signature.
  Proof.
    exists Empty_set (rels Σ); exact (fun _ => 0).
  Defined.

  Fixpoint Σ_Σ0 (A : fol_form Σ) :=
    match A with
      | ⊥ => ⊥
      | fol_atom r _ => @fol_atom Σ0 r vec_nil
      | fol_bin b A B => fol_bin b (Σ_Σ0 A) (Σ_Σ0 B)
      | fol_quant q A => fol_quant q (Σ_Σ0 A)
     end.

  Section soundness.

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

    Let M' : fo_model Σ0 unit.
    Proof.
      split.
      + intros [].
      + intros r _; apply (fom_rels M r).
        rewrite HΣ; exact vec_nil.
    Defined.

    Local Fact Σ_Σ0_sound A φ ψ : fol_sem M φ A <-> fol_sem M' ψ (Σ_Σ0 A).
    Proof.
      revert φ ψ; induction A as [ | r v | b A HA B HB | [] A HA ]; intros φ ψ.
      + simpl; tauto.
      + simpl; fol equiv.
        revert v; rewrite (HΣ r); unfold eq_rect_r; simpl.
        intros v; vec nil v; auto.
      + apply fol_bin_sem_ext; auto.
      + simpl; split.
        * intros (? & H); exists tt; revert H; apply HA.
        * intros (? & H); exists (φ 0); revert H; apply HA.
      + simpl; split.
        * intros H x; generalize (H (φ 0)); apply HA.
        * intros H x; generalize (H tt); apply HA.
    Qed.

    Hypothesis (Mdec : fo_model_dec M)
               (phi : nat -> X)
               (A : fol_form Σ)
               (HA : fol_sem M phi A).

    Local Lemma Σ_Σ0_soundness : fo_form_fin_dec_SAT (Σ_Σ0 A).
    Proof.
      exists unit, M', finite_t_unit.
      exists. { intros r v; simpl; apply Mdec. }
      exists (fun _ => tt).
      revert HA; apply Σ_Σ0_sound.
    Qed.

  End soundness.

  Section completeness.

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

    Let M : fo_model Σ unit.
    Proof.
      split.
      + intros; exact tt.
      + intros r _; apply (fom_rels M' r vec_nil).
    Defined.

    Local Fact Σ_Σ0_complete A φ ψ : fol_sem M φ A <-> fol_sem M' ψ (Σ_Σ0 A).
    Proof.
      revert φ ψ; induction A as [ | r v | b A HA B HB | [] A HA ]; intros φ ψ.
      + simpl; tauto.
      + simpl; tauto.
      + apply fol_bin_sem_ext; auto.
      + simpl; split.
        * intros (? & H); exists (ψ 0); revert H; apply HA.
        * intros (? & H); exists (φ 0); revert H; apply HA.
      + simpl; split.
        * intros H x; generalize (H (φ 0)); apply HA.
        * intros H x; generalize (H (ψ 0)); apply HA.
    Qed.

    Hypothesis (M'dec : fo_model_dec M')
               (psi : nat -> X)
               (A : fol_form Σ)
               (HA : fol_sem M' psi (Σ_Σ0 A)).

    Local Lemma Σ_Σ0_completeness : fo_form_fin_dec_SAT A.
    Proof.
      exists unit, M, finite_t_unit.
      exists. { intros r v; simpl; apply M'dec. }
      exists (fun _ => tt).
      revert HA; apply Σ_Σ0_complete.
    Qed.

  End completeness.

  Theorem Σ_Σ0_correct A : fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (Σ_Σ0 A).
  Proof.
    split.
    + intros (X & M & _ & G2 & phi & G3).
      apply Σ_Σ0_soundness with X M phi; auto.
    + intros (X & M & _ & G2 & phi & G3).
      apply Σ_Σ0_completeness with X M phi; auto.
  Qed.

End Σ_Σ0.

Section Σ0_Σ.

  Variable (Σ : fo_signature)
           (HΣ : forall r, ar_rels Σ r = 0).

  Fixpoint Σ0_Σ (A : fol_form (Σ0 Σ)) :=
    match A with
      | ⊥ => ⊥
      | fol_atom r _ => @fol_atom Σ r (cast vec_nil (eq_sym (HΣ r)))
      | fol_bin b A B => fol_bin b (Σ0_Σ A) (Σ0_Σ B)
      | fol_quant q A => fol_quant q (Σ0_Σ A)
     end.

  Section soundness.

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

    Let M' : fo_model Σ unit.
    Proof.
      split.
      + intros; exact tt.
      + intros r _; apply (fom_rels M r vec_nil).
    Defined.

    Local Fact Σ0_Σ_sound A φ ψ : fol_sem M' ψ (Σ0_Σ A) <-> fol_sem M φ A.
    Proof.
      revert φ ψ; induction A as [ | r v | b A HA B HB | [] A HA ]; intros φ ψ.
      + simpl; tauto.
      + simpl in *; vec nil v; simpl; tauto.
      + apply fol_bin_sem_ext; auto.
      + simpl; split.
        * intros (? & H); exists (φ 0); revert H; apply HA.
        * intros (? & H); exists (ψ 0); revert H; apply HA.
      + simpl; split.
        * intros H x; generalize (H (ψ 0)); apply HA.
        * intros H x; generalize (H (φ 0)); apply HA.
    Qed.

    Hypothesis (Mdec : fo_model_dec M)
               (φ : nat -> X)
               (A : fol_form (Σ0 Σ))
               (HA : fol_sem M φ A).

    Local Lemma Σ0_Σ_soundness : fo_form_fin_dec_SAT (Σ0_Σ A).
    Proof.
      exists unit, M', finite_t_unit.
      exists. { intros r v; simpl; apply Mdec. }
      exists (fun _ => tt).
      revert HA; apply Σ0_Σ_sound.
    Qed.

  End soundness.

  Section completeness.

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

    Let M' : fo_model (Σ0 Σ) unit.
    Proof.
      split.
      + intros [].
      + intros r _; apply (fom_rels M r).
        rewrite HΣ; exact vec_nil.
    Defined.

    Local Fact Σ0_Σ_complete A φ ψ : fol_sem M ψ (Σ0_Σ A) <-> fol_sem M' φ A.
    Proof.
      revert φ ψ; induction A as [ | r v | b A HA B HB | [] A HA ]; intros φ ψ.
      + simpl; tauto.
      + simpl; fol equiv.
        revert v; rewrite (HΣ r); unfold eq_rect_r; simpl; auto.
      + apply fol_bin_sem_ext; auto.
      + simpl; split.
        * intros (? & H); exists tt; revert H; apply HA.
        * intros (? & H); exists (ψ 0); revert H; apply HA.
      + simpl; split.
        * intros H x; generalize (H (ψ 0)); apply HA.
        * intros H x; generalize (H tt); apply HA.
    Qed.

    Hypothesis (Mdec : fo_model_dec M)
               (phi : nat -> X)
               (A : fol_form (Σ0 Σ))
               (HA : fol_sem M phi (Σ0_Σ A)).

    Local Lemma Σ0_Σ_completeness : fo_form_fin_dec_SAT A.
    Proof.
      exists unit, M', finite_t_unit.
      exists. { intros r v; simpl; apply Mdec. }
      exists (fun _ => tt).
      revert HA; apply Σ0_Σ_complete.
    Qed.

  End completeness.

  Theorem Σ0_Σ_correct A : fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (Σ0_Σ A).
  Proof.
    split.
    + intros (X & M & _ & G2 & phi & G3).
      apply Σ0_Σ_soundness with X M phi; auto.
    + intros (X & M & _ & G2 & phi & G3).
      apply Σ0_Σ_completeness with X M phi; auto.
  Qed.

End Σ0_Σ.