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.
Set Implicit Arguments.
Tactic Notation "iff" "equal" := apply fol_equiv_ext.
Local Notation ø := vec_nil.
Section Sig_n_Sig.
Variable (Σ : fo_signature) (r : rels Σ).
Notation Σn := (Σrel (ar_rels _ r)).
Local Fixpoint enc (A : fol_form Σn) : fol_form Σ :=
match A with
| ⊥ => ⊥
| fol_atom _ v => fol_atom r (vec_map (fun x => £(Σrel_var x)) v)
| fol_bin b A B => fol_bin b (enc A) (enc B)
| fol_quant q A => fol_quant q (enc A)
end.
Section M_enc_n.
Variables (X : Type) (M : fo_model Σ X).
Local Definition M_enc_n : fo_model Σn X.
Proof.
exists; intros [] v.
exact (fom_rels M r v).
Defined.
Notation "⟪ A ⟫" := (fun ψ => fol_sem M ψ A).
Notation "⟪ A ⟫'" := (fun φ => fol_sem M_enc_n φ A) (at level 1, format "⟪ A ⟫'").
Local Fact enc_correct_1 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ.
Proof.
revert φ.
induction A as [ | [] v | b A HA B HB | q A HA ]; intros phi.
+ simpl; tauto.
+ unfold M_enc_n; simpl; rewrite vec_map_map.
iff equal; f_equal; apply vec_pos_ext.
intros p; do 2 rewrite vec_pos_map; rew fot.
simpl in v; generalize (vec_pos v p); intros [ i | [] ].
rew fot; simpl; auto.
+ simpl; apply fol_bin_sem_ext; auto.
+ simpl; apply fol_quant_sem_ext; intro; auto.
Qed.
End M_enc_n.
Local Lemma SAT_SATn A : fo_form_fin_dec_SAT (enc A)
-> fo_form_fin_dec_SAT A.
Proof.
intros (X & M & H1 & H2 & phi & H3).
exists X, (M_enc_n M), H1.
exists. { intros [] v; apply H2. }
exists phi.
revert H3; apply enc_correct_1.
Qed.
Section Mn_enc.
Variables (X : Type) (Mn : fo_model Σn X) (x0 : X).
Local Definition Mn_enc : fo_model Σ X.
Proof.
exists.
+ intros s v; apply x0.
+ intros r' v.
destruct (eq_nat_dec (ar_rels _ r) (ar_rels _ r')) as [ H | H ].
* exact (fom_rels Mn tt (eq_rect_r _ v H)).
* exact False.
Defined.
Notation "⟪ A ⟫" := (fun ψ => fol_sem Mn_enc ψ A).
Notation "⟪ A ⟫'" := (fun φ => fol_sem Mn φ A) (at level 1, format "⟪ A ⟫'").
Local Fact enc_correct_2 A φ : ⟪ A ⟫' φ <-> ⟪ enc A ⟫ φ.
Proof.
revert φ.
induction A as [ | [] v | b A HA B HB | q A HA ]; intros phi.
+ simpl; tauto.
+ unfold Mn_enc; simpl; rewrite vec_map_map.
destruct (eq_nat_dec (ar_rels Σ r) (ar_rels Σ r)) as [ H | [] ]; auto.
rewrite eq_nat_uniq with (H := H); unfold eq_rect_r; simpl.
iff equal; f_equal; apply vec_pos_ext.
intros p; do 2 rewrite vec_pos_map; rew fot.
simpl in v; generalize (vec_pos v p); intros [ i | [] ].
rew fot; simpl; auto.
+ simpl; apply fol_bin_sem_ext; auto.
+ simpl; apply fol_quant_sem_ext; intro; auto.
Qed.
End Mn_enc.
Local Lemma SATn_SAT A : fo_form_fin_dec_SAT A
-> fo_form_fin_dec_SAT (enc A).
Proof.
intros (X & Mn & H1 & H2 & phi & H3).
exists X, (Mn_enc Mn (phi 0)), H1.
exists.
{ intros r' v; simpl.
destruct (eq_nat_dec (ar_rels Σ r) (ar_rels Σ r')) as [ H | H ].
+ revert v; rewrite <- H; unfold eq_rect_r; simpl; intro; apply H2.
+ right; tauto. }
exists phi.
revert H3; apply enc_correct_2.
Qed.
Hint Resolve SATn_SAT SAT_SATn : core.
Local Theorem SATn_SAT_red :
{ f : fol_form Σn -> fol_form Σ
| forall A, fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (f A) }.
Proof. exists enc; split; auto. Qed.
End Sig_n_Sig.
Theorem SATn_SAT_reduction (Σ : fo_signature) (n : nat) (r : rels Σ) (Hr : ar_rels _ r = n) :
{ f : fol_form (Σrel n) -> fol_form Σ
| forall A, fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (f A) }.
Proof. subst n; apply SATn_SAT_red. Qed.