Reification fails when dealing with heterogeneous relation

[YaZko]

Hello,

I am encountering the following behaviour that looks like a bug: while I can take the greatest fixed-point of an endo over an heterogeneous relation, the coinduction tactic then fails during the process of reification.

Am I missing a good reason for this to happen?

The following minimal example reproduces this behavior.

From Coinduction Require Import
    coinduction rel tactics.

Section hetero.

  Variable X Y : Type.
  Variable sm : mon (X -> X -> Prop).
  Variable sh : mon (X -> Y -> Prop).

  Notation bisimm := (gfp sm).
  Notation bisimh := (gfp sh).

  (* Homogeneous case, no problem *)
  Goal forall x y, bisimm x y.
    coinduction ? ?.
  Abort.

  (* Heterogeneous case, reification fails *)
  Goal forall x y, bisimh x y.
    Fail coinduction ? ?.
  Abort.

End hetero.

[YaZko]

Actually taking a closer look, I realise that more generally the reification process seems to support only binary homogeneous relations at the moment, predicates or relations of higher arity are not supported either if I understand the tactics file correctly.

The Readme mentions that Hur's divergence example was covered, but examples have been cut from the main repo to avoid an unnecessary dependency and I can't seem to find the coq-coinduction-examples repo anywhere. Would it be accessible somewhere? Since it's a unary case, I'm curious if you had support for it at some point, or if you just by-passed the tactics all together.

More generally, I'd be strongly interested in a good support for at least predicates and binary (non-dependent) heterogeneous relations. I I understand correctly, this starts with alternatives to pT and rT, and alternate specialized reified reification.coinduction and reification.accumulate statements. But it also requires to expand the ml plugin accordingly.

I'm happy to give a shot at such an extension, but before I jump right in mindlessly, would you have any foresight as to how it should be done maybe?

Thanks!

[damien-pous]

Hi Yannick, Indeed, only homogeneous relations are supported for now. For the heterogeneous (+ arbitrary arity) case, I have already done the required generalisation of reification.coinduction et al., but I still need to extend the ocaml code - on my todo list... Concerning coq-coinduction-examples, I did move it out because they were quite slow to compile, and because I based some of the student homeworks on it this year... I'll publish the package soon - will send it to you privately.

[YaZko]

Ah wonderful, I didn't know it was already in the pipes.

Thanks a lot Damien!

[damien-pous]

Last commit on master should provide the feature! Please try it out, I'll make a new (opam) release if it works properly for you @YaZko.

[YaZko]

Wonderful, thanks a lot @damien-pous !

I just run a couple of tests locally, it's working flawlessly. I did not stress tested too much, but tried it on one case both on a toy example and to my real-life application without any issue, so I believe it is ready to be released!

Thanks again, Yannick

[damien-pous]

Hi again @YaZko, I've just added support for dependent arities (was fun how smooth this was...). Can you check I didn't break your use-case ? Best, Damien

[YaZko]

Hi Damien,

Hmm, this actually seems to have broken something, but why is not yet clear to me. I have a setoid rewrite that is now failing on my side exactly here: https://github.com/vellvm/ctrees/blob/master/theories/Bisim.v#L499 The exact rewrite that fails is the one by cnv_wbisim. But actually this mirrors closely your ccs development from the companion paper, and the same rewrite fails there: if you look at the lemma Equivalence_wbisim, when proving that weak bisimulation is transitive, you have the same issue.

Digging into a diff of the typeclass debug traces between f3161d0613d3cd782f1d9582ea96f932b633ccdb (where the rewrite worked) and the current head (on the ccs file for simplicity), it seems that things are now more complex when reaching this goal: Debug: 1.1-1: looking for (Proper (?R ==> RelationAlgebra.lattice.weq ==> ?r) body) with backtracking It used to be discharged via app_weq: Debug: 1.1-1.1: simple apply @app_weq on (Proper (?R ==> RelationAlgebra.lattice.weq ==> ?r) body), 0 subgoal(s) Now it gets more messy and if I read correctly the trace hits a conversion issue:

Debug: 1.1-1.1-2 : (Unconvertible (relation (mon (S -> S -> Prop) -> (S -> S -> Prop) -> S -> S -> Prop)) (?R ==> RelationAlgebra.lattice.weq ==> ?r)%signature (weq ==> weq ==> weq)%signature)

I have a vague feeling that it is not an issue with your extension of this library, but has to do with a conflict between the lattice constructs from the coinduction library and the ones from the RelationAlgebra library (you can see that there are two distinct weq in the conversion issues).

That's been a recurrent pain-point actually in these development manipulating both libraries, but it feels like having one side being dependent and not the other makes the interaction even more fragile.

[damien-pous]

Indeed, those interactions are painful, and getting some proper sharing here is next on my todo list... (doesn't look that easy, unfortunately)

The thing is that I need to define [dpointwise_relation], the obvious dependent generalisation of [pointwise_relation]. And to use it in [CompleteLattice_dfun], which generalises [CompleteLattice_fun] and which is now used even in the non-dependent case. Then Coq seems to be lost when it needs to recognise that [dpointwise_relation] in the non-dependent case is nothing but the [pointwise_relation] (which is still used in relation-algebra).

In coinduction-examples, I could solve it as follows: https://github.com/damien-pous/coinduction-examples/commit/f15957dd7ff85081eb9bd9dfeba01a0f0890733b

Is this an option for you?

[YaZko]

Ah yes your fix works on my side as well, thanks!

I can only confirm that the sharing would be great to have for sure, but it's definitely fine to live with the current situation.

On a different note, I would have a request: you are now leaking a notation REL. Could it be wrapped into a module (or I think 8.15 has fine grained options to avoid exporting notations with modules?). Because currently I have a bunch of scripts of the shape step in EQ; inv EQ; inv REL. that now break because Coq panics when it gets to the inv REL part because it parses it before the hypothesis exists and hence interpret it as your notation and crashes. step in EQ; inv EQ. inv REL is an easy fix, but that's a bit annoying. (arguably such scripts relying on generating names are terrible practice, I plead guilty, but still...)

[YaZko]

Actually you are only using it in tactics.v so just wrapping the file in a section to keep the notation local would be enough I think?

[YaZko]

The support for dependent relations definitely makes some typeclass resolution even harder than before, I have some setoid rewrites that don't terminate anymore and that I'm failing to fix so far. But I don't yet have a good argument as to why it happens, and whether it's not just on my side that I should manage better my set of instances for rewriting.

[YaZko]

Ok I did manage to pass all of my development against the latest version of the library. I did not end up managing to single out which inferences got harder, but instead systematically went through the development to:

• always provide a pair of instance of the shape Proper (rel ==> rel ==> impl) and Proper (rel ==> rel ==> flip impl) instead of an iff one
• provide explicit Proper instances to rewrite gfp b into t b R rather than let it figure out the monotonicity argument
• add a few other explicit rules that could be derived from some relations being subrelations of others.

That eventually ended up being sufficient to solve my issues, and speed up overall the rewritings, so as far as I'm concerned I'm happy with this latest version!

[damien-pous]

Thanks @YaZko, this feature is now released in v1.4