✔ Making a decidable version of an inductive predicate · Coq users

Stream: Coq users

Topic: ✔ Making a decidable version of an inductive predicate

Clément Blaudeau (Feb 01 2022 at 22:51):

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!

Paolo Giarrusso (Feb 02 2022 at 01:13):

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

Paolo Giarrusso (Feb 02 2022 at 01:14):

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

Paolo Giarrusso (Feb 02 2022 at 01:16):

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

Paolo Giarrusso (Feb 02 2022 at 01:20):

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.

Paolo Giarrusso (Feb 02 2022 at 01:26):

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.

Paolo Giarrusso (Feb 02 2022 at 01:26):

(and then relate that to your boolean function).

Paolo Giarrusso (Feb 02 2022 at 01:32):

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

Paolo Giarrusso (Feb 02 2022 at 01:34):

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

Paolo Giarrusso (Feb 02 2022 at 01:37):

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.

Pierre Castéran (Feb 02 2022 at 07:33):

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_Operatorsand Operators_Properties are used to decompose an accessibility hypothesis in smaller parts (applying lemmas relating transitive closures and List.appfor 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

Clément Blaudeau (Feb 04 2022 at 22:55):

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 !

Notification Bot (Feb 04 2022 at 22:55):

Clément Blaudeau has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC