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

Model Discreteness and Interpreted Equality

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.