coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Werner <benjamin.werner AT inria.fr>
- To: Peter Hawkins <hawkinsp AT cs.stanford.edu>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club]Set comprehensions in Coq?
- Date: Tue, 6 Mar 2007 11:33:30 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:from:subject:date:to:x-mailer:sender; b=dEwtEEeV6WKQQe70CydRHdXtuoW3v5pr/flPbk6J+0l8wZG4Samtuq4pJ6PQjtc8PNI6Qa8b+QSwcRRCv2LfZytD7TpmL0x0EKWvD7Qrdpet4K/4GXnI83MVEr6EvmO9yvUQ8XmTvKNXor0gLwkE8ZC082tmdg/Fh/3TPRlOXdA=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club]Set comprehensions in Coq?, Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?, Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?, Benjamin Werner
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
- Re: [Coq-Club]Set comprehensions in Coq?,
Peter Hawkins
- Re: [Coq-Club]Set comprehensions in Coq?,
Adam Chlipala
Archive powered by MhonArc 2.6.16.