The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,


I am not sur I get it, but what happens if you construct your DAG  
inductively ?
Something like :

Inductive CFG : Type :=
cfg_i : nat -> (list (formula * CFG)) -> CFG.

Here you actually have a tree (thus no sharing in your DAG). But since
dfg : DFG is of a concrete type, you can build programs over it.

Actually, if you avoid lists and define CFG and list of formula * CFG  
simultaneously, you get :


Inductive CFG : Type :=
cfg_i : nat -> forest -> CFG
with forest : Type :=
| nnil : forest
| ccons : formula -> CFG -> forest -> forest.

Fixpoint val (d:CFG) : formula :=
match d with
| cfg_i _ l => (l_val l)
end
with l_val (l : forest) : formula :=
match l with
| nnil => f_false
| ccons f d' l' =>
     (f_or (f_and f (val d'))
          (l_val l'))
end.

which may be close to what you are looking for ?

Note that the nat in the nodes are not really useful anymore.

Going back to your original question: this is indeed related to
set comprehension, since the idea is what is used in the (inductive)
encoding of sets in type theory. The idea of the encoding is due
to P. Aczel. There should be a contrib ZF coming with the Coq contribs.

You can look at Peter's papers, or my "Sets in Types, Types in Sets"  
paper
on  benjamin.werner.name


Hope this helps,

Benjamin


Le 4 mars 07 à 04:06, Peter Hawkins a écrit :

> 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
>
> --------------------------------------------------------
> 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