generic map-cong and such

[mechvel]

Standard library provides map-cong, map-id, map-compose as related to the propositional equality ≡. But the case of List over Setoid is highly usable. And I suggest this:

-----------------------------------------------------------------------
module OfMapsToSetoid {α β β=} (A : Set α) (S : Setoid β β=)
 where
 open Setoid S using (_≈_)  renaming (Carrier to B; reflexive to ≈reflexive;
                                                             refl to ≈refl; sym to ≈sym; trans to ≈trans)
 infixl 2 _≈∘_

 _≈∘_ :  Rel (A → B) _
 f ≈∘ g =  (x : A) → f x ≈ g x

 ≈∘refl : Reflexive _≈∘_
 ≈∘refl _ = ≈refl

 ≈∘reflexive : _≡_ ⇒ _≈∘_
 ≈∘reflexive {x} refl =  ≈∘refl {x}

 ≈∘sym : Symmetric _≈∘_
 ≈∘sym f≈∘g =  ≈sym ∘ f≈∘g

 ≈∘trans : Transitive _≈∘_
 ≈∘trans f≈∘g g≈∘h x =  ≈trans (f≈∘g x) (g≈∘h x)

 ≈∘Equiv : IsEquivalence _≈∘_
 ≈∘Equiv = record{ refl  = \{x}         → ≈∘refl {x}
                            ; sym   = \{x} {y}     → ≈∘sym {x} {y}
                            ; trans = \{x} {y} {z} → ≈∘trans {x} {y} {z} }

 ≈∘Setoid : Setoid (α ⊔ β) (α ⊔ β=)
 ≈∘Setoid = record{ Carrier       = A → B
                              ; _≈_           = _≈∘_
                              ; isEquivalence = ≈∘Equiv }

 lSetoid = ListPoint.setoid S

 open Setoid lSetoid using () renaming (_≈_ to _=l_; refl to =l-refl)

 gen-map-cong : {f g : A → B} → f ≈∘ g → (xs : List A) → map f xs =l map g xs
 gen-map-cong _    []       =  =l-refl
 gen-map-cong f≈∘g (x ∷ xs) =  (f≈∘g x) ∷p (gen-map-cong f≈∘g xs)
 ...
---------------------------------------------------------------------------------

[MatthewDaggitt]

Yup at some point I'll get around to porting all the relevant proofs in Data.List.Properties to Data.List.Relation.Equality.Setoid.

[mechvel]

But there is a more general condition for map f xs ≋ map g ys, which is widely used:

map-pointwise-≈ :  {f g : A → B} {xs ys : List A} → length xs ≡ length ys →
                              All id (zipWith (\x y → f x ≈ g y) xs ys) →  
                              map f xs ≋ map g ys

Here B is the carrier of a setoid, which setoid exports ≈, and ≋ is the pointwise equality induced by ≈. Has lib-1.1 something for this?

[MatthewDaggitt]

Has lib-1.1 something for this?

No, nothing that general.

[jamesmckinna]

Yup at some point I'll get around to porting all the relevant proofs in Data.List.Properties to Data.List.Relation.Equality.Setoid.

Cf. #2360 / #2393 and discussion of module parametrisation in #2397 ... time to open a fresh issue with a roadmap/tasklist for "all the relevant proofs"?