The Coq mailing list

["Peter Hawkins" <hawkinsp AT cs.stanford.edu>]

Hi...

Ok, here's a more concrete example. First, we define boolean
propositional formulae:
Require Import Arith.
Inductive formula: Set :=
 | f_var: nat -> formula
 | f_true: formula
 | f_false: formula
 | f_and: formula -> formula -> formula
 | f_or: formula -> formula -> formula
 | f_not: formula -> formula.

Next, we assume the existence of a finite, connected, directed,
acyclic control flow graph with formulae on the edges, with a single
distinguished entry node n0. The formula on each edge represents the
conditions under which that transition may occur.

Parameter cfg : nat -> nat -> formula -> Prop.
Parameter n0 : nat.
(... statements of DAGness and so forth...)

Now, I want to define a relation representing a guard formula at each
node in the control flow graph. The guard represents the conditions
under which a program point may be reached.

To obtain the value of a node n, for each predecessor p of n I take
the conjunction of the value at the predecessor with the formula on
the edge p -> n, and take the disjunction for all predecessors of n.

NB. This is mathematically well-defined since the graph is a connected
DAG, so issues of fixpoints and so forth do not apply.

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.

(More background: that's actually the translation of a logic program
into an inductive definition, and by so doing I want to prove things
about the logic program. In logic programming terms, I need a way to
represent an all-solutions predicate)

Cheers,
Peter


On 3/3/07, Adam Chlipala 
<adamc AT cs.berkeley.edu>
 wrote:
> Peter Hawkins wrote:
> > No, I don't think that's what I want. If I understand things
> > correctly, that's a dependent type that lets me describe the type of
> > elements satisfying a predicate. I want _all_ elements satisfying a
> > predicate (as a concrete set), so I can, for example, write theorems
> > about properties of the set. Normally I'd want a value in Set, but I
> > don't think that's possible here.
>
> 'sig' does build Sets, and the resulting types have sets of values that
> are isomorphic to any other implementations of this idea that I can
> think of.  Maybe if you give a concrete example of something that is too
> much of a pain to do using 'sig', I could suggest something else; or
> maybe some other reader of this list understands your purpose better.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club