Stream: Coq users

Topic: Modeling reachability


view this post on Zulip Julin Shaji (Apr 01 2024 at 13:39):

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

view this post on Zulip Julin Shaji (Apr 01 2024 at 13:40):

Given that we can enumerate all possible A values.
Like enum: list A.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2024 at 16:58):

Hi @Julin Shaji , I suggest you have a look at math-comp's fingraph.v

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2024 at 16:58):

there reachability is defined (for graphs with finite number of nodes)

view this post on Zulip Julin Shaji (Apr 03 2024 at 05:01):

Thanks! connect of fingraph seems useful.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2024 at 14:21):

@Julin Shaji indeed, the dfs_pathP lemma is actually very deep!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2024 at 14:22):

[And hard to prove from scratch actually]

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2024 at 14:22):

But that's a very general technique to side-step termination issues

view this post on Zulip Julin Shaji (Apr 21 2024 at 12:41):

What could be a way to make a 'computation-oriented' form of connect? Does that mean starting from scratch?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 22 2024 at 11:55):

in other graph libraries

view this post on Zulip Julin Shaji (Apr 22 2024 at 12:12):

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 26 2024 at 13:17):

I see, thanks for the writeup.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 26 2024 at 13:18):

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!

view this post on Zulip Julin Shaji (Apr 27 2024 at 16:02):

Yeah, I was thinking like that too.

view this post on Zulip Julin Shaji (Apr 27 2024 at 16:04):

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.

view this post on Zulip Julin Shaji (Apr 27 2024 at 16:04):

I guess the problem is by nature non-trivial to prove from scratch like you said.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2024 at 17:33):

Yup, it follows the general pattern:


Last updated: Jun 23 2024 at 05:02 UTC