strengthen the AVL tree's insertWith-just

[mikedelorimier]

This PR adds insertWith-just-update to strengthen the existing insertWith-just in Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert.

The subject of this property is the op insertWith k f t l<k<u, where k is the key inserted, and f : Maybe (Val k) → Val k is applied to just v when (k , v) is already in t.

So insertWith-just is the "insertWith⁺" for the case where k is already in t.
But the preexisting insertWith-just ignores which v was already in t and requires P to hold for any v.

One of the main tests for insertWith-just is whether it can be used to prove the simple membership property:

(k , v) ∈ t → (k , f v) ∈ insertWith k f t l<k<u

insertWith-just-update strengthens insertWith-just so it can be used to prove this property.

Compare this to insert-just, which can be used to prove the analogous property:

(k , v) ∈ t → (k , v′) ∈ insert k v′ t l<k<u

The exact comparision of the new and old properties:

insertWith-just-update : (t : Tree V l u h) (l<k<u : l < k < u) →
                         (∀ k′ v → (eq : k ≈ k′) → P (k′ , v) →
                                   Q (k′ , respects eq (f (just (respects (sym eq) v))))) →
                         (p : Any P t) → k ≈ lookupKey p →
                         Any Q (proj₂ (insertWith k f t l<k<u))
insertWith-just : (t : Tree V l u h) (l<k<u : l < k < u) →
                  (pr : ∀ k′ v → (eq : k ≈ k′) →
                                 P (k′ , respects eq (f (just (respects (sym eq) v))))) →
                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t l<k<u))

You can see here that the old pr has to hold for arbitrary v.
The new pr is weakened with the assumption P (k′ , v).
The one place where insertWith-just was used was for insert-just, which happens to replace and ignore the old v.

Note that the changing insertWith-just to insertWith-just-update mostly preserved the proof, simplifying it slightly.

The following are some design decisions I took for the initial attempt at this PR:

My reason for the -update suffix is the new property is relevant when f actually updates the old v.

insertWith-just is deprecated.
At some point another deprecation phase would replace the name insertWith-just-update with insertWith-just.
For reference, Data.Vec.Properties.∷.ʳ++-eqFree is another deprecated name that nontrivially depends on its replacement.
I kept the new insertWith-just in its module nest so the order of implicit variables wouldn't change.

Now insertWith-just calls insertWith-just-update and insert-just calls insertWith-just-update instead of insertWith-just.

Note that the Q variable I added has level q, which is different than P's level.
This seems right, but it is different from Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup's Q, which has level p.

[jamesmckinna]

Two quick comments ahead of any proper review:

Note that the Q variable I added has level q, which is different than P's level. This seems right, but it is different from Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup's Q, which has level p.

1. So, in fact, the semantics of variable generalisation would nevertheless independently assign levels to variables P, Q declared by P Q : Pred A p when mentioned in a type. That is, we shouldn't think of a variable block as somehow defining a
   whole telescope of bindings-with-fixed-dependencies, rather that each dependency mentioned eg P : Pred A p, will trigger a generalisation over A and p as well. It's not perhaps the most immediately graspable idiom, but nevertheless 'works'. See https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html for details.

Simpler, perhaps: if we bind A B : Set a as variables, then when binding a function f : A → B in a type, A and B will in fact receive independent level assignments... as if we had instead written A : Set a; B : Set b...

2. In an earlier PR of yours, I had speculated whether the strengthening obtained here could in fact be reduced to a combination of the now-deprecated insertWith-just and lookup-rebuild. Are you now saying that this is, in fact, not possible?

[mikedelorimier]

2. In an earlier PR of yours, I had speculated whether the strengthening obtained here could in fact be reduced to a combination of the now-deprecated `insertWith-just` and `lookup-rebuild`. Are you now saying that this is, in fact, _not_ possible?

Oh right, here's the thread where you suggested lookup-rebuild with insertWith-just. I'm saying it's not possible.

I'll give an example data structure where lookup-rebuild and insertWith-just hold, but insertWith-just-update doesn't hold.
TLDR; Assume there's a bug where repeated insertWith k f gets stuck on v = f (just (f nothing)). insertWith-just doesn't see this bug because its pr argument doesn't depend on the v in f (just v).

This is a dictionary that's implemented by logging to a list (i.e. assoc-list with repeats).
So the representation of the dictionary is List and insert k v t = (k , v) ∷ t.
lookup and all the various read ops find the first pair that matches the queried k.
But insertWith has a bug where it finds the last matching pair instead of the first: insertWith k v t = (k , f (find-last k t)) ∷ t.
That is, all the library's ops behave as expected, except for insertWith.

The following example shows repeated insertWith k f stuck at f (just (f nothing)), instead of the expected (f ∘ just)^n (f nothing).

var	representation	denotation	op
t0	[]	{}	empty
t1	(k , f nothing) ∷ []	{k ↦ f nothing}	insertWith k f t0
t2	(k , f (just (f nothing))) ∷ (k , f nothing) ∷ []	{k ↦ f (just (f nothing))}	insertWith k f t1
t3	(k , f (just (f nothing))) ∷ (k , f (just (f nothing))) ∷ (k , f nothing) ∷ []	{k ↦ f (just (f nothing))}	insertWith k f t2

lookup-rebuild : (p : Any P t) → Q (lookup p) → Any Q t

Here, Any's path is an index starting from the head.
Because we're logging, the path also witnesses that no earlier index has the same key.
I think it's clear that lookup-rebuild holds.

insertWith-just : ... →
                  (pr : ∀ k′ v → (eq : k ≈ k′) →
                                 P (k′ , respects eq (f (just (respects (sym eq) v))))) →
                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t ...))

Because of Any ((k ≈_) ∘′ key) t, we know that the path to k exists, so we also know that t has (k , f nothing) last.
So insertWith k f t ... has (k , f (just (f nothing))) first so the returned path will index this first pair.
We'll have to provide a P (k , f (just (f nothing))) for this path's contents, which is given by pr k (f nothing) refl.
So we can implement insertWith-just.

insertWith-just-update : ... →
                         (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , v) →
                                   Q (k′ , respects eq (f (just (respects (sym eq) v))))) →
                         (p : Any P t) → k ≈ lookupKey p →
                         Any Q (proj₂ (insertWith k f t l<k<u))

Consider V = ℕ and f = maybe′ suc 0 and P (_ , v) = n ≡ v and Q (_ , v) = suc n ≡ v.
Then pr holds, but insertWith-just-update is clearly false.

[mikedelorimier]

rather that each dependency mentioned eg P : Pred A p, will trigger a generalisation over A and p as well

Thanks for point this out. I learned this at one point but forgot.

[jamesmckinna]

Thanks for the very detailed explanation.

I think on this basis we could argue that the earlier implementation of insertWith-just is in fact a bug, and so we could/should make the breaking change for v3.0 (rather than the more elaborate phased deprecation you outline) of giving it the type of insertWith-just-update. The earlier v2.4 deprecations concerned renamings only, so v2.4-compatible client code will need to change to reflect the new type you give, but that's part of the philosophy of moving to v3.0... to change things that are broken without having to make the change backwards-compatible.