[Agda] map⊆

[Nils Anders Danielsson]

On 2014-10-10 19:46, Sergei Meshveliani wrote:
> 1)  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → {xs ys : List C} →
>                                          xs ⊆ ys → map f xs ⊆' map f ys
>     is not close to Standard library
>     (so that an user home-made implementation has sense),

I don't think a function of this type exists in the library.

> 2) its special case of _≡_ {A = C} and _≡_ {A = C'}  set for _≈_ and
>     _≈'_  respectively  is done by
>     Data.List.Any.Membership.map-mono.

Yes.

I've attached two implementations of your function, both using the
library. One is short (not counting import statements…) and IMO not very
readable, the other is longer, more modular, and should be easier to
understand.

-- 
/NAD
-------------- next part --------------
open import Data.List using (map)
open import Data.List.Any as Any using (Any)
open import Data.List.Any.Properties using (Any↔; map↔)
open import Data.Product using (∃; _×_; _,_)
import Function.Related as Related
open import Relation.Binary
  using (Setoid; module Setoid; _Preserves_⟶_; _Respects_)

open Any.Membership-≡ using (_∈_; find; lose)

module _ {a₁ a₂} (A : Setoid a₁ a₂) where

  open Setoid A
    using () renaming (Carrier to AC; _≈_ to _≈A_; refl to reflA)
  open Any.Membership A using () renaming (_⊆_ to _⊆A_)

  Any-mono′ : ∀ {p} {P : AC → Set p} →
                                       P    Respects _≈A_ →
              (λ xs → ∃ λ x → x ∈ xs × P x) Respects _⊆A_
  Any-mono′ P-resp xs⊆ys (x , x∈xs , Px) =
    let x-∈A-xs                  = lose x∈xs reflA
        y , y∈ys ,        x≈y    = find (xs⊆ys x-∈A-xs)
    in  y , y∈ys , P-resp x≈y Px

  Any-mono : ∀ {p} {P : AC → Set p} →
                 P Respects _≈A_ →
             Any P Respects _⊆A_
  Any-mono {P = P} P-resp {xs} {ys} xs⊆ys =
    Any P xs                ↔⟨ sym Any↔ ⟩
    (∃ λ v → v ∈ xs × P v)  ∼⟨ Any-mono′ P-resp xs⊆ys ⟩
    (∃ λ v → v ∈ ys × P v)  ↔⟨ Any↔ ⟩
    Any P ys                ∎
    where open Related.EquationalReasoning

  module _ {b₁ b₂} (B : Setoid b₁ b₂) where

    open Setoid B using () renaming (Carrier to BC; _≈_ to _≈B_)
    open Any.Membership B using () renaming (_∈_ to _∈B_; _⊆_ to _⊆B_)

    map-mono : {f : AC → BC} →
                   f Preserves _≈A_ ⟶ _≈B_ →
               map f Preserves _⊆A_ ⟶ _⊆B_
    map-mono {f} f-pres {xs} {ys} xs⊆ys {y} =
      y ∈B map f xs            ↔⟨ sym map↔ ⟩
      Any (λ x → y ≈B f x) xs  ∼⟨ Any-mono (λ {u v} u≈v y≈fu → begin
                                              y    ≈⟨ y≈fu ⟩
                                              f u  ≈⟨ f-pres u≈v ⟩
                                              f v  □)
                                           xs⊆ys ⟩
      Any (λ x → y ≈B f x) ys  ↔⟨ map↔ ⟩
      y ∈B map f ys            ∎
      where
      open Related.EquationalReasoning
      open import Relation.Binary.EqReasoning B renaming (_∎ to _□)
-------------- next part --------------
open import Data.List using (map)
import Data.List.Any as Any
open import Data.List.Any.Properties using (Any↔; map↔)
open import Data.Product as Prod using (_,_)
open import Function using (id; _∘_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse
  using (module Inverse) renaming (_∘_ to _⊚_)
open import Relation.Binary using (Setoid; module Setoid; _Preserves_⟶_)

open Any.Membership-≡ using (find; lose)

module _ {a₁ a₂} (A : Setoid a₁ a₂)
         {b₁ b₂} (B : Setoid b₁ b₂) where

  open Setoid A renaming (Carrier to AC; _≈_ to _≈A_; refl to reflA)
  open Setoid B renaming (Carrier to BC; _≈_ to _≈B_; trans to transB)
  open Any.Membership A using () renaming (_⊆_ to _⊆A_)
  open Any.Membership B using () renaming (_⊆_ to _⊆B_)

  map-mono : {f : AC → BC} →
                 f Preserves _≈A_ ⟶ _≈B_ →
             map f Preserves _⊆A_ ⟶ _⊆B_
  map-mono f-pres xs⊆ys =
    _⟨$⟩_ (Inverse.to (map↔ ⊚ Any↔)) ∘
    (λ { (_ , v∈xs , u≈fv) →
         Prod.map id
                  (Prod.map id λ v≈w → transB u≈fv (f-pres v≈w))
                  (find (xs⊆ys (lose v∈xs reflA))) }) ∘
    _⟨$⟩_ (Inverse.from (map↔ ⊚ Any↔))