Source code on Github
{-# OPTIONS --safe #-}
module Prelude.Lists.Mappings where
open import Prelude.Init; open SetAsType
open L.Mem using (_∈_; mapWith∈; ∈-++⁻; ∈-++⁺ˡ; ∈-++⁺ʳ)
open L.Perm using (∈-resp-↭; Any-resp-↭)
open import Prelude.General using (⟫_)
open import Prelude.Lists.Membership
open import Prelude.Lists.Permutations
open import Prelude.ToList
private variable
a b p : Level
A : Type a
B : Type b
P : Pred A p
x : A
xs xs′ ys zs : List A
infixr 0 _↦′_ _↦_
_↦′_ : List A → (A → Type ℓ) → Type _
xs ↦′ P = ∀ {x} → x ∈ xs → P x
map↦ = _↦′_
syntax map↦ xs (λ x → f) = ∀[ x ∈ xs ] f
_↦_ : List A → Type b → Type _
xs ↦ B = xs ↦′ const B
dom : ∀ {xs : List A} → xs ↦′ P → List A
dom {xs = xs} _ = xs
codom : xs ↦ B → List B
codom = mapWith∈ _
codom-↦ : ∀ {xs : List A} → (f : xs ↦ B) → codom f ↦ A
codom-↦ {xs = x ∷ _} f = λ where
(here _) → x
(there x∈) → codom-↦ (f ∘ there) x∈
weaken-↦ : xs ↦′ P → ys ⊆ xs → ys ↦′ P
weaken-↦ f ys⊆xs = f ∘ ys⊆xs
cons-↦ : (x : A) → P x → xs ↦′ P → (x ∷ xs) ↦′ P
cons-↦ _ y _ (here refl) = y
cons-↦ _ _ f (there x∈) = f x∈
uncons-↦ : (x ∷ xs) ↦′ P → xs ↦′ P
uncons-↦ = _∘ there
permute-↦ : xs ↭ ys → xs ↦′ P → ys ↦′ P
permute-↦ xs↭ys xs↦ = xs↦ ∘ L.Perm.∈-resp-↭ (↭-sym xs↭ys)
_++/↦_ : xs ↦′ P → ys ↦′ P → xs ++ ys ↦′ P
xs↦ ++/↦ ys↦ = ∈-++⁻ _ >≡> λ where
(inj₁ x∈) → xs↦ x∈
(inj₂ y∈) → ys↦ y∈
destruct-++/↦ : xs ++ ys ↦′ P → (xs ↦′ P) × (ys ↦′ P)
destruct-++/↦ xys↦ = xys↦ ∘ ∈-++⁺ˡ , xys↦ ∘ ∈-++⁺ʳ _
destruct≡-++/↦ : zs ≡ xs ++ ys → zs ↦′ P → (xs ↦′ P) × (ys ↦′ P)
destruct≡-++/↦ refl = destruct-++/↦
extend-↦ : zs ↭ xs ++ ys → xs ↦′ P → ys ↦′ P → zs ↦′ P
extend-↦ zs↭ xs↦ ys↦ = permute-↦ (↭-sym zs↭) (xs↦ ++/↦ ys↦)
cong-↦ : xs ↦′ P → xs′ ≡ xs → xs′ ↦′ P
cong-↦ f refl = f
open ≡-Reasoning
module _ {A : Type ℓ} {xs : List A} {P : Pred A ℓ′} where
_≗↦_ : Rel (xs ↦′ P) _
f ≗↦ f′ = ∀ {x : A} (x∈ : x ∈ xs) → f x∈ ≡ f′ x∈
_≗⟨_⟩↦_ : ∀ {ys : List A} →
(ys ↦′ P) → (p↭ : xs ↭ ys) → (xs ↦′ P) → Type _
f′ ≗⟨ p↭ ⟩↦ f = ∀ {x : A} (x∈ : x ∈ xs) → f′ (∈-resp-↭ p↭ x∈) ≡ f x∈
permute-≗↦ : ∀ {ys : List A}
→ (p↭ : xs ↭ ys)
→ (f : xs ↦′ P)
→ permute-↦ p↭ f ≗⟨ p↭ ⟩↦ f
permute-≗↦ p↭ f {x} x∈ =
begin
permute-↦ p↭ f (∈-resp-↭ p↭ x∈)
≡⟨⟩
(f ∘ ∈-resp-↭ (↭-sym p↭)) (∈-resp-↭ p↭ x∈)
≡⟨⟩
f (∈-resp-↭ (↭-sym p↭) $ ∈-resp-↭ p↭ x∈)
≡⟨ cong f (∈-resp-↭∘∈-resp-↭˘ p↭ x∈) ⟩
f x∈
∎
permute-↦∘permute-↦˘ : ∀ {ys : List A}
→ (p↭ : xs ↭ ys)
→ (f : xs ↦′ P)
→ permute-↦ (↭-sym p↭) (permute-↦ p↭ f) ≗↦ f
permute-↦∘permute-↦˘ p↭ f {x} x∈
rewrite permute-≗↦ p↭ f x∈
| L.Perm.↭-sym-involutive p↭
= cong f $ Any-resp-↭∘Any-resp-↭˘ p↭ x∈
module _ (f : xs ↦′ P) (g : ys ↦′ P) where
destruct-++/↦∘++/↦ :
let f′ , g′ = destruct-++/↦ (f ++/↦ g)
in (f ≗↦ f′) × (g ≗↦ g′)
destruct-++/↦∘++/↦ = f≗ , g≗
where
fg : (xs ↦′ P) × (ys ↦′ P)
fg = destruct-++/↦ (f ++/↦ g)
f′ = fg .proj₁; g′ = fg .proj₂
f≗ : f ≗↦ f′
f≗ x∈ rewrite Any-++⁻∘Any-++⁺ˡ {ys = ys} x∈ = refl
g≗ : g ≗↦ g′
g≗ x∈ rewrite Any-++⁻∘Any-++⁺ʳ {xs = xs} x∈ = refl
destruct≡-++/↦∘cong-↦ :
(eq : zs ≡ xs ++ ys) →
let f′ , g′ = destruct≡-++/↦ eq (cong-↦ (f ++/↦ g) eq)
in (f ≗↦ f′) × (g ≗↦ g′)
destruct≡-++/↦∘cong-↦ refl = destruct-++/↦∘++/↦
module _ {A : Type ℓ} {P : A → Type ℓ′} {x : A} {xs ys zs : List A} where
permute-↦∘permute-↦ :
(p : xs ↭ ys) (q : ys ↭ zs) (f : xs ↦′ P) →
permute-↦ q (permute-↦ p f) ≗↦ permute-↦ (↭-trans p q) f
permute-↦∘permute-↦ p q f x∈ =
begin
permute-↦ q (permute-↦ p f) x∈
≡⟨⟩
f (∈-resp-↭ (↭-sym p) $ ∈-resp-↭ (↭-sym q) x∈)
≡⟨⟩
f (∈-resp-↭ (↭-sym $ ↭-trans p q) x∈)
≡⟨⟩
permute-↦ (↭-trans p q) f x∈
∎
module _ {A : Type ℓ} {xs ys : List A} {P : Pred A ℓ′} where
_≗⟨_⊆⟩↦_ : ys ↦′ P → (p : ys ⊆ xs) → xs ↦′ P → Type _
f′ ≗⟨ p ⊆⟩↦ f = f′ ≗↦ (f ∘ p)
weaken-≗↦ : (p : ys ⊆ xs) (f : xs ↦′ P)
→ weaken-↦ f p ≗⟨ p ⊆⟩↦ f
weaken-≗↦ _ _ _ = refl
_≗↦ˡ_ : xs ++ ys ↦′ P → xs ↦′ P → Type _
fg ≗↦ˡ f = (fg ∘ L.Mem.∈-++⁺ˡ) ≗↦ f
++-≗↦ˡ : (f : xs ↦′ P) (g : ys ↦′ P)
→ (f ++/↦ g) ≗↦ˡ f
++-≗↦ˡ _ _ (here _) = refl
++-≗↦ˡ _ _ (there x∈) rewrite ∈-++⁻∘∈-++⁺ˡ {ys = ys} x∈ = refl
_≗↦ʳ_ : xs ++ ys ↦′ P → ys ↦′ P → Type _
fg ≗↦ʳ g = (fg ∘ L.Mem.∈-++⁺ʳ _) ≗↦ g
++-≗↦ʳ : (f : xs ↦′ P) (g : ys ↦′ P)
→ (f ++/↦ g) ≗↦ʳ g
++-≗↦ʳ f g y∈ with ⟫ xs
... | ⟫ [] = refl
... | ⟫ _ ∷ xs′ rewrite ∈-++⁻∘∈-++⁺ʳ {xs = xs} y∈ = refl
_≗↦ˡʳ_,_ : xs ++ ys ↦′ P → xs ↦′ P → ys ↦′ P → Type _
fg ≗↦ˡʳ f , g = (fg ≗↦ˡ f) × (fg ≗↦ʳ g)
++-≗↦ˡʳ : (f : xs ↦′ P) (g : ys ↦′ P)
→ (f ++/↦ g) ≗↦ˡʳ f , g
++-≗↦ˡʳ f g = ++-≗↦ˡ f g , ++-≗↦ʳ f g
++/↦-inj₂ : ∀ (f : xs ↦′ P) (g : ys ↦′ P) (x∈ : x ∈ xs ++ ys) (y∈ : x ∈ ys)
→ ∈-++⁻ xs x∈ ≡ inj₂ y∈
→ (f ++/↦ g) x∈ ≡ g y∈
++/↦-inj₂ {xs = xs} _ _ x∈ _ eq
with inj₂ _ ← ∈-++⁻ xs x∈
with refl ← eq
= refl
++/↦≡-inj₂ : (eq : zs ≡ xs ++ ys)
→ ∀ (f : xs ↦′ P) (g : ys ↦′ P) (x∈ : x ∈ zs) (y∈ : x ∈ ys)
→ ∈-++⁻ xs (subst (x ∈_) eq x∈) ≡ inj₂ y∈
→ subst (_↦′ P) (sym eq) (f ++/↦ g) x∈ ≡ g y∈
++/↦≡-inj₂ refl = ++/↦-inj₂
++/↦-there : (f : x ∷ xs ↦′ P) (g : ys ↦′ P)
→ ((f ∘ there) ++/↦ g) ≗↦ ((f ++/↦ g) ∘ there)
++/↦-there {xs = []} _ _ {_} _ = refl
++/↦-there {xs = _ ∷ _} _ _ {_} (here _) = refl
++/↦-there {xs = xs@(_ ∷ _)} _ _ {_} (there x∈)
with ∈-++⁻ xs (there x∈)
... | inj₁ _ = refl
... | inj₂ _ = refl
uncons-≗↦ : (f : x ∷ xs ↦′ P) (g : ys ↦′ P)
→ uncons-↦ (f ++/↦ g) ≗↦ (uncons-↦ f ++/↦ g)
uncons-≗↦ f g {y} y∈ =
begin uncons-↦ (f ++/↦ g) y∈ ≡⟨⟩
(f ++/↦ g) (there y∈) ≡⟨ sym $ ++/↦-there f g y∈ ⟩
((f ∘ there) ++/↦ g) y∈ ≡⟨⟩
(uncons-↦ f ++/↦ g) y∈ ∎
instance
ToList-↦ : ∀ {xs : List A} → ToList (xs ↦ B) (A × B)
ToList-↦ {xs = xs} .toList f = zip xs (codom f)