Conversion from Vec equality to heterogeneous equality

[Blaisorblade]

to-≡ from Data.Vec.Equality converts from vector equality to homogeneous equality, but only once you've done the work of casting the arguments so that they have the same length. That seems enough work that it'd be worth it having it in the stdlib, together with to-≡.
I certainly want to-≅. Part of the problem shows up also for ≅-to-≡ — see ≅-to-subst-≡ for an alternative.

Here's an example of the functions I'd like to have and some example:

-- Let's try to use the result of xs++[]=xs as an equality.
-- This problem was posted by Fuuzetsu on the #agda IRC channel.

module VectorEqualityExtras (A : Set) where

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; ≡-to-≅)

open import Function

open import Data.Vec
open import Data.Vec.Properties
open import Data.Vec.Equality
open UsingVectorEquality (setoid A)
open PropositionalEquality

{-
-- Does not work. The problem is that vector equality is semi-heterogeneous, in
-- that the two compared vectors do not need to have, a priori, the same length.
-- So you can't convert it to a homogeneous equality.
xs++[]=xs-propEq : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≡ xs
xs++[]=xs-propEq xs = to-≡ (xs++[]=xs xs)
-}

to-≅ : ∀ {a} {A : Set a} {m n} {xs : Vec A m} {ys : Vec A n} → xs ≈ ys → xs ≅ ys
to-≅ p with length-equal p
to-≅ p | P.refl = ≡-to-≅ (to-≡ p)

≅-to-t-≡ : ∀ {a} {A B : Set a} {xs : A} {ys : B} → (p : xs ≅ ys) → A ≡ B
≅-to-t-≡ H.refl = P.refl

-- If you need a propositional equality, you'll have to use subst on one side.
-- However, we can do that for you, in different ways.

-- A generic way to convert heterogeneous to homogeneous equality.
≅-to-subst-≡ : ∀ {a} {A B : Set a} {xs : A} {ys : B} → (p : xs ≅ ys) → subst (λ x → x) (≅-to-t-≡ p) xs ≡ ys
≅-to-subst-≡ H.refl = P.refl

-- We can use it to build the following:
to-subst-≡′ : ∀ {a} {A : Set a} {m n} {xs : Vec A m} {ys : Vec A n} → (p : xs ≈ ys) → subst (λ x → x) (≅-to-t-≡ (to-≅ p)) xs ≡ ys
to-subst-≡′ = ≅-to-subst-≡ ∘ to-≅

-- A more specific one, with a more precise type for you.
to-subst-≡ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → (p : xs ≈ ys) → subst (Vec A) (length-equal p) xs ≡ ys
to-subst-≡ {xs = xs} p = H.≅-to-≡
  (H.trans
    (H.≡-subst-removable (Vec A) (length-equal p) xs)
    (to-≅ p))

-- Working variants of xs++[]=xs-propEq:
xs++[]=xs-hEq : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≅ xs
xs++[]=xs-hEq xs = to-≅ (xs++[]=xs xs)

xs++[]=xs-subst-propEq : ∀ {n} → (xs : Vec A n) → subst (Vec A) (length-equal (xs++[]=xs xs)) (xs ++ []) ≡ xs

-- Without to-subst-≡, we need an inlined version of it:
{-
xs++[]=xs-subst-propEq xs = H.≅-to-≡
  (H.trans
    (H.≡-subst-removable (Vec A) (length-equal (xs++[]=xs xs)) (xs ++ []))
    (xs++[]=xs-hEq xs))
-}

xs++[]=xs-subst-propEq xs = to-subst-≡ (xs++[]=xs xs)

This code also lives at
https://gist.github.com/Blaisorblade/87d7d50167704603e682

[Blaisorblade]

So, do you think the library functions (e.g. not examples with xs++[]=xs) in the code above could be merged?

[andreasabel]

On 20.09.2014 04:15, Paolo G. Giarrusso wrote:

So, do you think the library functions (e.g. not examples with
|xs++[]=xs|) in the code above could be merged?

A very general "yes, if they follow the reasoning and naming style of
the standard library".

• Lemma ≅-to-t-≡ is going to Relation.Binary.HeterogeneousEquality,
  right? I'd prefer a more telling name, like ≅-to-type-≡. Unless "t" is
  the accepted abbreviation for "type" in the std-lib (which I doubt).

The other stuff is going to Data.Vec.Equality, or?

Please make a pull request (and take special care to pick identifiers
that harmonize with the style of the remaining lib).

Thanks!
Andreas

Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel@gu.se
http://www2.tcs.ifi.lmu.de/~abel/

[Blaisorblade]

Thank you! Your guesses are mostly right — except for ≅-to-subst-≡ which I'd also place in Relation.Binary.HeterogeneousEquality.

[MatthewDaggitt]

A little late, but I've just added these into the library with commit 13a0620