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.
PreFos
does not ensure that the arity and the interpretation fit together (because you are usinglist
instead of a tuple of the given arity). It looks like the whole thing would benefit from more dependent types and less first-order-logic thinking. $\endgroup$nat
and asked how to express anatural number greater than zero
. I don't want to change the example now because your answer is great. $\endgroup$FOS
out ofPreFOS
andIsFOS
) was intended to be more important than the specific example, which is just a translation of the first-order logic concept as it's normally presented written in very naive Coq. $\endgroup$sig
type, written as{ x : A | p x }
? Sorry, I did read your question as it being about how to define relational structures, which is why I changed the title. Feel free to change it back, but before that, also please look at thesig
type to see if that answers your question. $\endgroup$sig
type tag is exactly what I am looking for. Thank you. Your answer is extremely helpful though (although a lot of it is beyond my level of understanding). I'm going to edit my question with an update explaining what the question originally was and what it is now. $\endgroup$