How to implement first-order relational structures in Coq?

Question

I'm trying to define a first-order relational structure in Coq.

I have a way to define a pre-first-order-relational-structure, which is not a standard notion, but seems simple enough.

I also have a way to insist that a pre-first-order-relational-structure is actually a relational structure.

These things can be stitched together with a sig type, but this does not make idiomatic use of Coq features. What's a better way to do it?

See Appendix B for a brief history of this question.

---

The approach that I've taken so far is to define a pre first-order structure as a thing that takes a type of symbols S and then wraps a type U denoting the universe/domain/carrier.

Every symbol has an arity, which is None if the symbol is not defined in this particular structure.

Also, every list of items taken from U is potentially inside the interpretation of any relation symbol (i.e. symbols don't a priori respect arity).

This approach keeps the type signature of a PreFOS simple.

Defining IsFOS, which takes a PreFOS and insists that it actually does respect arity is not that difficult.

Appendix A: Original Implementation

Require Import List.

(* A pre-[Relational First-order Structure] 

S is the set of all symbols, a symbol may or may not be defined
in a given relational structure.

 *)
Record PreFOS (S : Type) (U : Type) : Type :=
  { arity : S -> option nat
  ; interpretation : S -> (list U) -> Prop
  }.

(*
IsFOSImpl defines what it means to be a relational first-order structure.

If a symbol is undefined, it must be false everywhere.

If a symbol is defined, but called with the wrong number of arguments,
it must also return false.
 *)
Definition IsFOS (S : Type) (U : Type) (M : PreFOS S U) : Prop :=
  (
    (* Undefined symbols always interpret to false. *)
    (forall s : S,
        arity S U M s = None ->
        (forall args : list U, interpretation S U M s args -> False))
  ) /\
    (
      (* Defined symbols interpret to false outside their arity. *)
      (forall s : S,
          (exists n : nat, arity S U M s = Some n ->
                           (forall args : list U,
                               length args <> n ->
                               (interpretation S U M s args -> False))))
    ).

Appendix B: History of Question

This question was originally about how to take an existing type X and produce a type referring to the Xs that satisfy P. This is a sig type as pointed out by Andrej Bauer in the comments.

However, the original question was ambiguous how do you make a type constrained by a predicate could be referring to sig types. It is also a description of a first-order relational structure is.

Andrej's answer very thoroughly addresses everything that's non-idiomatic with Appendix A. I think this has a lot of value, especially for novice Coq users like me.

I'm retroactively changing this question to make the answer on topic.

Answer 1

Supplemental: It looks like I misunderstood the point of the question and the OP might have simply been looking for the sig type, usually written as {x : A | P A}. Apologies for showing below some irrelevant code.

Here is the idomatic approach to defining relational signatures and relational structures. It uses dependent types the way they're supposed to be used.

(* A relational signature is given by a type of relational symbols, and for each
   symbol an arity. While it is customary to think of the arity as a number, it
   is more principled to think of it as a set of indices (indexing the
   arguments).

   Thus, instead of saying that S has arity 2, we say that S har arity bool (or any other
   two-element type).
*)

Record RelationalSignature : Type :=
  { symbols :> Type
  ; arity : symbols -> Type
  }.

Arguments arity {_} _.

(* A relational structure is given by a carrier type U and an interpetation function
   which, for each relational symbol S of arity n, gives a predicate on U^n.

   Notice how taking arities to be types allows us to write just "arity S -> carrier".
*)

Record RelationalStructure (Sig : RelationalSignature) : Type :=
  { carrier :> Type
  ; interpretation : forall S : Sig, (arity S -> carrier) -> Prop
  }.

(* Example: a signature with a binary symbol Cow and a unary symbol Rabbit. *)

(* The type of symbols. *)
Inductive MySymbols : Type := Cow | Rabbit.

(* The arity of a unary symbol. *)
Inductive Unary : Type := the_arg.

(* The arity of a binary symbol. *)
Inductive Binary : Type := arg1 | arg2.

Definition MySignature :=
  {| symbols := MySymbols
   ; arity := fun S => match S with
                         | Cow => Binary
                         | Rabbit => Unary
                       end
  |}.

(* An example of a relational structure on natural numbers in which we interpret
   Cow as "less than or equal" and Rabbit as "not zero". *)

Definition MyStructure : RelationalStructure MySignature :=
  {| carrier := nat
   ; interpretation :=
       fun (S : MySignature) =>
         match S with
           | Cow => (fun xs => xs arg1 <= xs arg2)
           | Rabbit => fun xs => xs the_arg <> 0
         end
  |}.

You do not need any predicates explaining that the signature or the relational structure is valid. It is all taken care of by the dependent types.