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

From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list finite.

From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.

From Undecidability.TRAKHTENBROT
Require Import notations fol_ops fo_sig fo_terms fo_logic fo_sat discrete.

Set Implicit Arguments.

(* * FSAT and FSAT over discrete model are equivalent *)

(* This equivalence and hence reduction most probably cannot
be proved for infinite models, or at least the way it is
proved in here *)

(* Satisfiability of A in a finite and decidable model implies satisfiability
of A in a finite, decidable and discrete model, in fact in a model based on
the finite type (pos n) *)

Theorem fo_discrete_removal Σ (A : fol_form Σ) :
fo_form_fin_dec_SAT A
-> exists n, fo_form_fin_discr_dec_SAT_in A (pos n).
Proof.
intros (X & M & Hfin & Hdec & phi & HA).
set (ls := fol_syms A).
set (lr := fol_rels A).
destruct (fo_fin_model_discretize ls lr Hfin Hdec)
as (n & Md & Mdec & f & E).
set (psy n := f (phi n)).
exists n, (@pos_eq_dec _), Md, (finite_t_pos _) , Mdec, psy.
revert HA.
apply fo_model_projection with (p := f);
unfold lr, ls; auto; apply incl_refl.
Qed.

Theorem fo_form_fin_dec_SAT_fin_discr_dec Σ (A : fol_form Σ) :
fo_form_fin_dec_SAT A
-> fo_form_fin_discr_dec_SAT A.
Proof.
intros H.
destruct fo_discrete_removal with (1 := H) (A := A)
as (n & Hn); auto.
exists (pos n); auto.
Qed.