Vec.Properties: introduce `≈-cong′`

[mildsunrise]

Additions

This PR introduces the ≈-cong′ lemma:

≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n))
          {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys →
          f xs ≈[ cong f-len eq ] f ys
≈-cong′ f {xs = []}     {ys = []}     refl = cast-is-id refl (f [])
≈-cong′ f {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl

This lemma does for ≈[_] what cong does for ≡: given f and xs ≈[ _ ] ys it proves f xs ≈[ _ ] f ys. More specifically, it proves that any Vec A n → Vec B m function that is polymorphic in n must preserve ≈[_].

Current status

Compare this with the existing ≈-cong lemma (introduced by @shhyou with #2067 along with the reasoning system):

≈-cong : ∀ .{l≡o : l ≡ o} .{m≡n : m ≡ n} {xs : Vec A m} {ys zs} (f : Vec A o → Vec A n) →
         xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs
≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs)

This lemma works for a non-polymorphic f, but it requires the user to supply proof that f preserves ≈[_]. We already have a handful of these proofs written for some functions:

map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) →
           map f (cast eq xs) ≡ cast eq (map f xs)
map-cast {n = zero}  f eq []       = refl
map-cast {n = suc _} f eq (x ∷ xs)
  = cong (f x ∷_) (map-cast f (suc-injective eq) xs)

cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} →
           cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys
cast-++ˡ {o = zero}  eq []       {ys} = cast-is-id refl (cast eq [] ++ ys)
cast-++ˡ {o = suc o} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ˡ (cong pred eq) xs)

cast-++ʳ : ∀ .(eq : n ≡ o) (xs : Vec A m) {ys : Vec A n} →
           cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys
cast-++ʳ {m = zero}  eq []       {ys} = refl
cast-++ʳ {m = suc m} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq xs)

cast-∷ʳ : ∀ .(eq : suc n ≡ suc m) x (xs : Vec A n) →
          cast eq (xs ∷ʳ x) ≡ (cast (cong pred eq) xs) ∷ʳ x
cast-∷ʳ {m = zero}  eq x []       = refl
cast-∷ʳ {m = suc m} eq x (y ∷ xs) = cong (y ∷_) (cast-∷ʳ (cong pred eq) x xs)
cast-∷ʳ _ x _ = ≈-cong′ (_∷ʳ x) refl

cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
cast-reverse {n = zero}  eq []       = refl
cast-reverse {n = suc n} eq (x ∷ xs) = begin
  reverse (x ∷ xs)           ≂⟨ reverse-∷ x xs ⟩
  reverse xs ∷ʳ x            ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ eq x (reverse xs))
                                       (cast-reverse (cong pred eq) xs) ⟩
  reverse (cast _ xs) ∷ʳ x   ≂⟨ reverse-∷ x (cast (cong pred eq) xs) ⟨
  reverse (x ∷ cast _ xs)    ≈⟨⟩
  reverse (cast eq (x ∷ xs)) ∎
  where open CastReasoning

Simplifications

≈-cong′ is used in a similar way, except that it doesn't require manually proving preservation of cast for f. So, most uses of ≈-cong (including all current ones) can be migrated to ≈-cong′ just by removing the 2nd argument:

-≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _) (fromList-reverse xs)
+≈-cong′ (_∷ʳ x) (fromList-reverse xs)

An extreme example is example4-cong², where we show chaining ≈-cong. This can also be done with ≈-cong′, but there we can further express it as a single ≈-cong′ of the composition, as we tend to do with cong:

-≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
-        (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
-                (unfold-∷ʳ _ a xs))
+≈-cong′ (reverse ∘ (_++ ys)) (unfold-∷ʳ _ a xs)

And the 'cast preservation' proofs above, should you still need them, are just special cases of ≈-cong′:

map-cast f _ _ = sym (≈-cong′ (map f) refl)
cast-++ˡ _ _ {ys} = ≈-cong′ (_++ ys) refl
cast-++ʳ _ xs = ≈-cong′ (xs ++_) refl
cast-∷ʳ _ x _ = ≈-cong′ (_∷ʳ x) refl
cast-reverse _ _ = ≈-cong′ reverse refl

[mildsunrise]

(draft because we still need to figure out a good name for this lemma, and also update the documentation at doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda)

[shhyou]

This improvement is awesome! In the long term, it'd be great if it's possible to prioritize this new lemma over the existing ≈-cong, perhaps taking up its name and giving the old one a different name.

[jamesmckinna]

This seems like a great contribution... but I'm not across what's needed to get this over the line for v2.2 @mildsunrise how would you like to proceed? Is there something (further) that the other (approving) maintainers could contribute here?

[MatthewDaggitt]

Remaining to do?

1. Both of @shhyou's comment should be implemented I think
2. We should then implement the old ≈-cong in terms of ≈-cong′ for sanity
3. We should deprecate ≈-cong?

[mildsunrise]

(rebased to fix conflicts, mostly caused by #2430)

[mildsunrise]

Hi! Sorry for the absence, I'll try to unblock this as much as possible.

Both of @shhyou's comment should be implemented I think

Done!

We should then implement the old ≈-cong in terms of ≈-cong′ for sanity

I don't think we can, because the old ≈-cong is more general than the new one: the new one only works for functions that are polymorphic in the input length, and where the output length depends only on the input length.

We should deprecate ≈-cong?

I am indifferent. I guess it could be argued that the new ≈-cong′ is the one that actually shows congruence, and the old one is merely an adapter from a sort of congruence proof given for cast to a congruence proof for ≈[_].

[MatthewDaggitt]

I don't think we can, because the old ≈-cong is more general than the new one: the new one only works for functions that are polymorphic in the input length, and where the output length depends only on the input length.

Ah okay, that makes sense!

I am indifferent. I guess it could be argued that the new ≈-cong′ is the one that actually shows congruence, and the old one is merely an adapter from a sort of congruence proof given for cast to a congruence proof for ≈[_].

Yup. I was advocating for deprecation based on the misconception that the new definition was more general.

Okay great, I think that tidies everything up. I'll merge this in and squeeze it into v2.2