Require Import Undecidability.FOL.Util.Syntax Undecidability.FOL.Util.Syntax_facts.
Export FragmentSyntax.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Require Import Vector.

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Local Notation vec := Vector.t.

Section fixb.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.

  Fixpoint impl (A : list form) phi :=
    match A with
    | []
    | :: A bin Impl (impl A )
    end.

End fixb.

Notation "A phi" := (impl A ) (right associativity, at level 55).

Tarski Semantics

Section Tarski.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.


  Section Semantics.

    Variable domain : Type.

    Class interp := B_I
      {
        i_func : f : syms, vec domain (ar_syms f) domain ;
        i_atom : P : preds, vec domain (ar_preds P) Prop ;
      }.

    Definition env := domain.

    Context {I : interp}.

    Fixpoint eval (rho : env) (t : term) : domain :=
      match t with
      | var s s
      | func f v i_func (Vector.map (eval ) v)
      end.

    Fixpoint sat {ff : falsity_flag} (rho : env) (phi : form) : Prop :=
      match with
      | atom P v i_atom (Vector.map (eval ) v)
      | falsity False
      | bin Impl sat sat
      | quant All d : domain, sat (d .: )
      end.

  End Semantics.

  Notation "rho ⊨ phi" := (sat ) (at level 20).

  Section Substs.

    Variable D : Type.
    Variable I : interp D.

    Lemma eval_ext rho xi t :
      ( x, x = x) eval t = eval t.
    Proof.
      intros H. induction t; cbn.
      - now apply H.
      - f_equal. apply map_ext_in. now apply IH.
    Qed.


    Lemma eval_comp rho xi t :
      eval (subst_term t) = eval ( >> eval ) t.
    Proof.
      induction t; cbn.
      - reflexivity.
      - f_equal. rewrite map_map. apply map_ext_in, IH.
    Qed.


    Lemma sat_ext {ff : falsity_flag} rho xi phi :
      ( x, x = x) .
    Proof.
      induction as [ | b P v | | ] in , |- *; cbn; intros H.
      - reflexivity.
      - erewrite map_ext; try reflexivity. intros t. now apply eval_ext.
      - specialize ( ). specialize ( ). destruct ; intuition.
      - destruct q.
        + split; intros H' d; eapply IHphi; try apply (H' d). 1,2: intros []; cbn; intuition.
    Qed.


    Lemma sat_ext' {ff : falsity_flag} rho xi phi :
      ( x, x = x) .
    Proof.
      intros Hext H. rewrite sat_ext. exact H.
      intros x. now rewrite (Hext x).
    Qed.


    Lemma sat_comp {ff : falsity_flag} rho xi phi :
       (subst_form ) ( >> eval ) .
    Proof.
      induction as [ | b P v | | ] in , |- *; cbn.
      - reflexivity.
      - erewrite map_map, map_ext; try reflexivity. intros t. apply eval_comp.
      - specialize ( ). specialize ( ). destruct ; intuition.
      - destruct q.
        + setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d).
          all: intros []; cbn; trivial; now setoid_rewrite eval_comp.
    Qed.


    Lemma sat_subst {ff : falsity_flag} rho sigma phi :
      ( x, eval ( x) = x) (subst_form ).
    Proof.
      intros H. rewrite sat_comp. apply sat_ext. intros x. now rewrite H.
    Qed.


    Lemma sat_single {ff : falsity_flag} (rho : D) (Phi : form) (t : term) :
      (eval t .: ) Phi subst_form (t..) Phi.
    Proof.
      rewrite sat_comp. apply sat_ext. now intros [].
    Qed.


    Lemma impl_sat {ff : falsity_flag} A rho phi :
      sat (A ) (( psi, A sat ) sat ).
    Proof.
      induction A; cbn; firstorder congruence.
    Qed.


    Lemma impl_sat' {ff : falsity_flag} A rho phi :
      sat (A ) (( psi, A sat ) sat ).
    Proof.
      eapply impl_sat.
    Qed.


  End Substs.

End Tarski.

Arguments sat {_ _ _ _ _} _ _, {_ _ _} _ {_} _ _.
Arguments interp {_ _} _, _ _ _.

Notation "p ⊨ phi" := (sat _ p ) (at level 20).
Notation "p ⊫ A" := ( psi, A sat _ p ) (at level 20).

Section Defs.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.

  Definition valid_ctx A phi := D (I : interp D) rho, ( psi, A ) .
  Definition valid phi := D (I : interp D) rho, .
  Definition valid_L A := D (I : interp D) rho, A.
  Definition satis phi := D (I : interp D) rho, .
  Definition fullsatis A := D (I : interp D) rho, A.

End Defs.


Section TM.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Instance TM : interp unit :=
    {| i_func := _ _ tt; i_atom := _ _ True; |}.

  Fact TM_sat (rho : unit) (phi : form falsity_off) :
     .
  Proof.
    revert . remember falsity_off as ff. induction ; cbn; trivial.
    - discriminate.
    - destruct ; auto.
    - destruct q; firstorder.
  Qed.


End TM.