[Agda] Converting All2 to All

[Dr. ERDI Gergo]

I've written the following function for Data.Vect.All (but it would apply
just the same for Data.List.All):

all₂₁ : ∀ {a b} {A : Set a} {B : Set b} {P : A → Set}
{n} {xs : Vec A n} {ys : Vec B n} →
All₂ (λ x y → P x) xs ys → All P xs
all₂₁ [] = []
all₂₁ (p ∷ ps) = p ∷ all₂₁ ps

My questions are:
1. What would be a good name for this function? (I am fairly certain all₂₁
is not one:))
2. Should I add it to the stdlib?

Thanks,
Gergo

[Dr. ERDI Gergo]

Post by Dr. ERDI Gergo
all₂₁ : ∀ {a b} {A : Set a} {B : Set b} {P : A → Set}
{n} {xs : Vec A n} {ys : Vec B n} →
All₂ (λ x y → P x) xs ys → All P xs
all₂₁ [] = []
all₂₁ (p ∷ ps) = p ∷ all₂₁ ps

Of course there's a symmetric all₂₂ with (λ x y → P y)as well.

[Matthew Daggitt]

Hi Gergo,
So the first thing to say is that due to an oversight, the functionality
of `All₂` in `Data.Vec.All` is actually a duplicate of the existing
datatype `Relation.Binary.Vec.Pointwise`. In the upcoming release of the
library at the end of January, we're deprecating `All₂` and moving
`Relation.Binary.Vec.Pointwise` to `Data.Vec.Relation.InductivePointwise`
and `Data.Vec.Relation.ExtensionalPointwise`. Feel free to have a look at
the CHANGELOG in standard library
<https://github.com/agda/agda-stdlib/tree/master/src> repository for a more
detailed explanation.

That's not to say your proofs wouldn't be a welcome contribution to the
library! The natural place for it in v0.15 will be in the new module
`Data.Vec.Relation.InductivePointwise`. I would probably name them
something like `pointwiseˡ⇒all` and `pointwiseʳ⇒all`, and possibly add
their counterparts `all⇒pointwiseˡ` and `all⇒pointwiseʳ` as well. If you'd
like to add them, feel free to submit a pull request to the library and
they can be added to the upcoming release.

Thanks,
Matthew

Post by Dr. ERDI Gergo
all₂₁ : ∀ {a b} {A : Set a} {B : Set b} {P : A → Set}

Post by Dr. ERDI Gergo
{n} {xs : Vec A n} {ys : Vec B n} →
All₂ (λ x y → P x) xs ys → All P xs
all₂₁ [] = []
all₂₁ (p ∷ ps) = p ∷ all₂₁ ps

Of course there's a symmetric all₂₂ with (λ x y → P y)as well.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Dr. ERDI Gergo]

Hi Gergo, So the first thing to say is that due to an oversight, the functionality of
`All₂` in `Data.Vec.All` is actually a duplicate of the existing datatype
`Relation.Binary.Vec.Pointwise`. In the upcoming release of the library at the end of
January, we're deprecating `All₂` and moving `Relation.Binary.Vec.Pointwise` to
`Data.Vec.Relation.InductivePointwise` and `Data.Vec.Relation.ExtensionalPointwise`.
Feel free to have a look at the CHANGELOG in standard library repository for a more
detailed explanation.

Thanks, that is a very useful heads-up. I've now migrated my code to
D.V.R.InductivePointwise in anticipation of this change.

That's not to say your proofs wouldn't be a welcome contribution to the library! The
natural place for it in v0.15 will be in the new module
`Data.Vec.Relation.InductivePointwise`. I would probably name them something
like `pointwiseˡ⇒all` and `pointwiseʳ⇒all`, and possibly add their counterparts
`all⇒pointwiseˡ` and `all⇒pointwiseʳ` as well. If you'd like to add them, feel free
to submit a pull request to the library and they can be added to the upcoming release.

One snag, though, is that the current upgrade path of the stdlib requires
D.V.All to import D.V.R.InductivePointwise, so I can't add these proofs to
D.V.R.InductivePointwise without causing a circular import... the only
place to add them currently is D.V.All. Would it still make sense for me
to add them to D.V.All?

[Matthew Daggitt]

Gergo, thanks for your PR to the library with the proofs. I've updated the
library so they shouldn't cause the cyclic dependency any more.

Hi Gergo, So the first thing to say is that due to an oversight, the

functionality of
`All₂` in `Data.Vec.All` is actually a duplicate of the existing datatype
`Relation.Binary.Vec.Pointwise`. In the upcoming release of the library at the end of
January, we're deprecating `All₂` and moving
`Relation.Binary.Vec.Pointwise` to
`Data.Vec.Relation.InductivePointwise` and `Data.Vec.Relation.Extensional
Pointwise`.
Feel free to have a look at the CHANGELOG in standard library repository
for a more
detailed explanation.

Thanks, that is a very useful heads-up. I've now migrated my code to
D.V.R.InductivePointwise in anticipation of this change.
That's not to say your proofs wouldn't be a welcome contribution to the

library! The
natural place for it in v0.15 will be in the new module
`Data.Vec.Relation.InductivePointwise`. I would probably name them something
like `pointwiseˡ⇒all` and `pointwiseʳ⇒all`, and possibly add their
counterparts
`all⇒pointwiseˡ` and `all⇒pointwiseʳ` as well. If you'd like to add them,
feel free
to submit a pull request to the library and they can be added to the upcoming release.

One snag, though, is that the current upgrade path of the stdlib requires
D.V.All to import D.V.R.InductivePointwise, so I can't add these proofs to
D.V.R.InductivePointwise without causing a circular import... the only
place to add them currently is D.V.All. Would it still make sense for me to
add them to D.V.All?