Hi everyone ! I'm looking for a piece of advice on the simplest way to get a decidable version of an inductive predicate. (which is, in my special case, possible)

I have notion of *reachability* in a store (a list of objects), defined as so : (objects have a decidable, finite number of fields)

```
Parameter Obj: Type.
Definition Loc: Type := nat.
Definition Store: Type := list Obj.
Parameter isField: Store -> Loc -> Loc -> bool.
Inductive reachability : Store -> Loc -> Loc -> Prop :=
| rch_heap: (* we can access the current location *)
forall l σ,
l < length σ ->
reachability σ l l
| rch_step: (* we can access a field of the object at l0 *)
forall l0 l1 σ,
isField σ l0 l1 = true ->
reachability σ l0 l1
| rch_trans: (* transitive case *)
forall l0 l1 l2 σ,
reachability σ l0 l1 ->
reachability σ l1 l2 ->
reachability σ l0 l2.
```

And I'm trying to build a boolean version, such that I have something like :

```
Fixpoint reachabilityb (σ:Store) (l1 l2: Loc) : bool. ?
Lemma reachability_reflect: forall σ l0 l1, reflect (reachability σ l0 l1) (reachabilityb σ l0 l1).
```

The mathematical result in itself is pretty obvious: Just recursively look up every fields, starting from `l0`

. You'll either find the target in less than `length σ`

steps or never will. Such a function is easy to write, with a starting fuel of `length σ`

. However, expressing its equivalence with the inductive predicate in Coq is tricky.

I've started to try with lists, finite sets and invariants about the presence of duplicates, but I've kind of got lost in the details. This seemed to me like a problem classic enough so that someone else have dealt with it before. Would you have any ideas on efficient (proof-work wise - the function does not have to be *actually* efficient) to approach this ?

Thanks you for any help!

rch_trans and rch_step can be replaced by an rch_cons constructor that checks isField and recurses.

Then isField could be replaced by a function Store -> Loc -> list Loc giving you the list of fields of the given object.

Those two steps could simplify a bit the result (maybe only the boring parts) by making your inductive/judgment somewhat closer to the call graph of the other function...

For the bigger task, it might help to index the reachability proof by its trace, which is just the list of nodes, and prove that (1) any reachability proof implies one where the trace has no duplicates (by cutting cycles) (2) any duplicate-free proof has length < length sigma. Both should be consequences of the pigeonhole principle.

Once you have this short-enough derivation of reachability, you should prove that the reachability function actually finds a derivation. But it need not find the same! So you might want to reason about a function that finds *all* proofs of reachability and show that its output includes your derivation.

(and then relate that to your boolean function).

I'm far from sure this is the simplest road, but the pieces of this proof strategy should be easier.

[a mathematical paper will call this obvious, but an actual proof isn’t — we just have great intuition here]

for bonus points, the above proof strategy should be doable entirely without finite sets and with just lists (and a couple uses of `NoDup`

), and lists are easier to reason about.

Paolo Giarrusso said:

for bonus points, the above proof strategy should be doable entirely without finite sets and with just lists (and a couple uses of

`NoDup`

), and lists are easier to reason about.

I had to write accessibility lemmas, and traces were the right tool.

Libraries `List`

, `Relation_Operators`

and `Operators_Properties`

are used to decompose an accessibility hypothesis in smaller parts (applying lemmas relating transitive closures and `List.app`

for instance).

Unfortunately, these lemmas were proven as ad-hoc helpers in a bigger library.

It may be useful to write a generic library on traces and accessibility (if it doesn't exist yet).

https://github.com/coq-community/hydra-battles/blob/master/theories/ordinals/Epsilon0/Paths.v

Thank you for your answers ! I followed your advice.

If someone stumbles upon this thread in the future, here is the scheme:

- Make a sibling predicate
`reachability_trace`

that also state the list of points used for the transitive case (the base cases have no trace) - Prove it equivalent to the normal version (easy)
- State that every location in the trace is actually reachable from the starting point with the trace split at the location
- State that every reachable location is reachable with a trace that has no duplicates
- Show the pigeonhole principle.
- Make a boolean function (with fuel) that tests the base case and recursively calls itself on all possible midpoints (using
`existsb`

for instance) - Show that its monotonic with respect to its fuel
- Show that the predicate extended with a trace implies the boolean version with a fuel of
`length trace`

- Show the equivalence between the normal predicate and the boolean version with a fuel of
`length store`

It would be nice to have an accessibility library, but it seems hard to build something that fits every needs...

Thank you again !

Clément Blaudeau has marked this topic as resolved.

Last updated: Jun 16 2024 at 01:42 UTC