Suppose that we have a relation R: A -> A -> bool
.
What could be a good way to find all reachable A
values from a given
A
with respect to R
?
As in making a function like:
f: A -> list A
I needed this in the Type
world (as in, extractable).
Given that we can enumerate all possible A
values.
Like enum: list A
.
Hi @Julin Shaji , I suggest you have a look at math-comp's fingraph.v
there reachability is defined (for graphs with finite number of nodes)
Thanks! connect
of fingraph seems useful.
@Julin Shaji indeed, the dfs_pathP
lemma is actually very deep!
[And hard to prove from scratch actually]
But that's a very general technique to side-step termination issues
What could be a way to make a 'computation-oriented' form of connect
? Does that mean starting from scratch?
I think connect should work reasonably well for small examples, what kind of algorithm you have in mind? It is likely that better methods are already implemented
in other graph libraries
Actually, I was trying to have a proven-correct way of translation
regular expressions to a computation-friendly (ie, extractable) dfa
representation.
I attempted to learn from the way it's done for the proof-friendly
representation in
https://github.com/coq-community/reglang/blob/master/theories/dfa.v
There this conversion path is followed:
regex → nfa → dfa
using mathcomp sets as states.
To handle epsilon transitions, nfa
values are built from enfa
(nfas with epsilon transitions. nfa
type has no ε-transitions).
For the conversion from enfa to nfa, a way to collect all states
reachable from a given state is needed.
They use connect
for this:
-
https://github.com/coq-community/reglang/blob/master/theories/nfa.v#L59C44-L59C51
But connect
itself seems to use reflection lemmas and its extracted
form is quite large.
So, I figured the problem was its proof-oriented nature and set about
trying to find a computation-oriented counterpart.
(I'm not sure if that was the right path to go about.)
I see, thanks for the writeup.
I'd first check with experts (cc @Cyril Cohen ) about more efficient connect
versions.
I would develop the proofs using connect, and then, later, do a connect' that you can prove _extensionally_ equivalent to the other connect, then you can just replace it!
Yeah, I was thinking like that too.
So I was trying to see if it's possible to do refinement (a la CoqEAL) from a computation-friendly definition to connect
.
But for that, I needed a way to formulate that type friendly connect
.
I had been looking at how connect
itself is defined.
But that looked like a lot.
I guess the problem is by nature non-trivial to prove from scratch like you said.
Yup, it follows the general pattern:
Last updated: Oct 13 2024 at 01:02 UTC