## Stream: Coq users

### Topic: Modeling reachability

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

#### Julin Shaji (Apr 01 2024 at 13:40):

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

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

#### Emilio Jesús Gallego Arias (Apr 02 2024 at 16:58):

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

#### Julin Shaji (Apr 03 2024 at 05:01):

Thanks! `connect` of fingraph seems useful.

#### Emilio Jesús Gallego Arias (Apr 03 2024 at 14:21):

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

#### Emilio Jesús Gallego Arias (Apr 03 2024 at 14:22):

[And hard to prove from scratch actually]

#### Emilio Jesús Gallego Arias (Apr 03 2024 at 14:22):

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

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

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

#### Emilio Jesús Gallego Arias (Apr 22 2024 at 11:55):

in other graph libraries

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

#### Emilio Jesús Gallego Arias (Apr 26 2024 at 13:17):

I see, thanks for the writeup.

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

#### Julin Shaji (Apr 27 2024 at 16:02):

Yeah, I was thinking like that too.

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

#### Julin Shaji (Apr 27 2024 at 16:04):

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

#### Emilio Jesús Gallego Arias (Apr 28 2024 at 17:33):

Yup, it follows the general pattern:

• prove some function good up to N steps, where N ensures termination
• find a N big enough so that your function will always reach a "done" state
• eliminate the N

Last updated: Jun 23 2024 at 05:02 UTC