Require Import List Arith Lia.

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

From Undecidability.TRAKHTENBROT
  Require Import notations.

Set Default Proof Using "Type".

Set Implicit Arguments.


Record fo_signature := Mk_fo_signature {
  syms : Type;
  rels : Type;
  ar_syms : syms -> nat;
  ar_rels : rels -> nat
}.


Definition Σrel (n : nat) : fo_signature.
Proof.
  exists Empty_set
         unit
         .
  + intros [].   + exact (fun _ => n). Defined.


Definition Σrel_eq (n : nat) : fo_signature.
Proof.
  exists Empty_set
         bool
         .
  + intros [].   + exact (fun b => if b then n else 2).
Defined.



Inductive Σbpcp_syms :=
  | Σbpcp_bool : bool -> Σbpcp_syms
  | Σbpcp_unit : Σbpcp_syms
  | Σbpcp_undef : Σbpcp_syms
  .


Inductive Σbpcp_rels :=
  | Σbpcp_hand : Σbpcp_rels
  | Σbpcp_ssfx : Σbpcp_rels
  | Σbpcp_eq : Σbpcp_rels
  .

Definition Σbpcp : fo_signature.
Proof.
  exists Σbpcp_syms Σbpcp_rels.
  + exact (fun s =>
      match s with
        | Σbpcp_bool _ => 1
        | _ => 0
      end).
  + exact (fun _ => 2).
Defined.


Record fo_model Σ (X : Type) := Mk_fo_model {
  fom_syms : forall s, vec X (ar_syms Σ s) -> X;
  fom_rels : forall r, vec X (ar_rels Σ r) -> Prop }.


Definition fo_model_dec Σ X (M : fo_model Σ X) :=
  forall r (v : vec _ (ar_rels _ r)), { fom_rels M r v } + { ~ fom_rels M r v }.


Definition rel2_on_vec X (R : X -> X -> Prop) (v : vec X 2) : Prop :=
  R (vec_head v) (vec_head (vec_tail v)).

Arguments rel2_on_vec {X} R v /.

Section bin_rel_Σ2.

  Variable (X : Type) (R : X -> X -> Prop).

  Definition bin_rel_Σ2 : fo_model (Σrel 2) X.
  Proof using R.
    exists; intros [].
    exact (rel2_on_vec R).
  Defined.

  Hypothesis HR : forall x y, { R x y } + { ~ R x y }.

  Fact bin_rel_Σ2_dec : fo_model_dec bin_rel_Σ2.
  Proof using HR. intros [] v; apply HR. Qed.

End bin_rel_Σ2.