The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Peter Hawkins wrote:
> Inductive pointguard : nat -> formula -> Prop :=
>  | pg_base: pointguard n0 f_true.
>  | pointguard : ... what goes here to specify the conjunction of
> pgmerge for each n? ...
> with pgmerge : nat -> formula :=
>  | pgmerge_elem: forall p1 p2 f1 f2,
>      pointguard p1 f1 -> cfg p1 p2 f2 -> pgmerge p2 (f_and f1 f2).
>
> Now, I expect I can't actually write that in Coq since it doesn't know
> about the graph property in question and won't understand that the
> definition is sane. I'm guessing that at best I can define this
> axiomatically.

It looks to me like the central issue isn't the ability to use "set 
comprehensions"; what matters is that the sets you care about are 
finite, so that it makes sense to define the conjunctions of their 
images under a function.  (The meaning of "and" in the Coq standard 
library isn't such that infinite conjunctions are necessarily 
representable in Prop, or at least it isn't obvious to me how to prove 
otherwise.)

However you specify the finiteness of your graph, you should be able to 
prove that every node of the graph is below some specific natural 
number.  With that, it should be easy to define a relation that iterates 
through all natural numbers and merges for only those that are adjacent 
to the current node.

You could also define a general abstraction of finite sets of natural 
numbers, where you have a fold operation (generalization of your merge) 
that depends on knowing that a bound on the set size exists.