Agda-stdlib: AllNeighbours: Predicate on lists

[EdNutting]

I've been using the following data type to describe a property applied to all neighbouring pairs of elements. Not sure if it may be useful to others or if there's a better way of writing it?

data AllNeighbours {p} (P : A → A → Set p) : L.List A → Set (a Level.⊔ p) where
    empty : AllNeighbours P L.[]
    single : (x : A) → AllNeighbours P (x L.∷ L.[])
    pair : {x y : A} → {zs : L.List A} → P x y → AllNeighbours P (y L.∷ zs) → AllNeighbours P (x L.∷ y L.∷ zs)

[gallais]

In Haskell this type of thing is typically built like this:

AllNeighbours P xs = All (uncurry P) (zip xs (drop 1 xs))

Do you have interesting properties in mind that we can prove of AllNeighbours and
are not implied by a result on All?
For instance (P => Q) -> (AllNeighbours P => AllNeighbours Q) is a consequence
of All's map with this encoding.

[MatthewDaggitt]

I've experimented with the above definition as well. In practice I've only ever needed it for transitive relations and so I've found AllPairs (see #147) much easier to work with as it only has two constructors:

data AllPairs {a ℓ} {A : Set a} (_~_ : Rel A ℓ) : List A → Set (a ⊔ ℓ) where
  []  : AllPairs _~_ []
  _∷_ : ∀ {x xs} → All (x ~_) xs → AllPairs _~_ xs → AllPairs _~_ (x ∷ xs)

I'm planning on finally getting around to adding the above to the standard library after the next release. However they're obviously not equivalent in the non-transitive case so your's would be worth adding as well. I might be tempted to call it Linked though.

[MatthewDaggitt]

In response to @gallais's suggestion, Andreas suggested something similar for AllPairs. I feel there's a tension between reusability and readability here. For me personally, it takes quite a lot more effort to work out what's going on when they're defined using All. On the other hand it does make proving properties much easier, (if you do understand what's going on :smile:).

I'm on the fence about which encoding is better... Anyone else have any opinions?

[gallais]

I'm mostly curious about the type of results we would like to have on this and why we
may want to depart from the well-established Haskell approach.

I can already see one advantage of a first class AllNeighbours over an All-based
encoding: we can always pattern-match on a proof of AllNeighbours xs whereas an
All-based encoding will force us to split on xs first for unification to be happy.

Indeed inverting [] ?= zip xs (drop 1 xs) to get xs = [] or xs = [ x ],
and y :: y ?= zip xs (drop 1 xs) to get x = x :: x' :: xs' is hard!

[MatthewDaggitt]

I'm mostly curious about the type of results we would like to have on this

It's not quite the same but here's my AllPairs properties file. I haven't needed anything particularly fancy, just the standard set of lemmas about the way it interacts with list operations.

I can already see one advantage of a first class AllNeighbours over an All-based
encoding: we can always pattern-match on a proof of AllNeighbours xs whereas an
All-based encoding will force us to split on xs first for unification to be happy.

Good point.

[EdNutting]

So I had previously looked at Haskell's way of doing it, but as you've noted, it's tricky to show some things with and required other case splits for unification, which is awkward as an 'end user' though not a big deal. Working with all neighbours by this data has been fairly intuituve.

I've been using this to express properties over lists of edges. Where an edge is a pair of source and target. Given a path as a list of edges, I use AllNeighbours to enforce that the path is well formed I.e.target of one edge matches source of the next.

(I'm aware there are other ways to express paths, this happens to be the most handy for my use case)

[MatthewDaggitt]

I've been using this to express properties over lists of edges. Where an edge is a pair of source and target. Given a path as a list of edges, I use AllNeighbours to enforce that the path is well formed I.e.target of one edge matches source of the next.

Haha, I've been doing exactly the same thing. Out of interest do you have a link to your implementation? Mine is here, and I've always been disatisfied with it...

[EdNutting]

@MatthewDaggitt Unfortunately my proof isn't open source at the moment. It will be eventually when I am closer to completing. I'm attempting to do a proof by refinement that my team's hardware garbage collector works. My Graphs module is rather big by now but essentially handles 'reachability' in directed cyclic graphs. Perhaps this is a conversation for somewhere else though? This issue doesn't seem appropriate ;)

[HuStmpHrrr]

it's also related to https://github.com/agda/agda-stdlib/issues/467

[JacquesCarette]

Minor comment: just because it is possible to 'encode' something does not necessarily mean that it is a good idea to do so. If an isomorphic type lets you prove things much more conveniently, that might be worth it.

This is, in part, why my colleagues and I introduced the notion of "Realm" for mechanized mathematics systems, to make it easier to use equivalent definitions when it is beneficial to do so. And, of course, once HoTT is no longer cutting-edge research, transport can become a quite viable method.

Of course, one must still be wary of the cost. Naturals encoded in binary are great for computation, awful for proof; naturals encoded in unary are great for proof idiotic for computation. This generalizes (polynomials, matrices/vectors, etc) all have these representational choices that matter.