------------------------------------------------------------------------
-- The Agda standard library
--
-- Application of substitutions to lists, along with various lemmas
------------------------------------------------------------------------
-- This module illustrates how Data.Fin.Substitution.Lemmas.AppLemmas
-- can be used.
{-# OPTIONS --cubical-compatible --safe #-}
open import Data.Fin.Substitution.Lemmas using (Lemmas₄; AppLemmas)
open import Data.Nat.Base using (ℕ)
module Data.Fin.Substitution.List {ℓ} {T : ℕ → Set ℓ} (lemmas₄ : Lemmas₄ T) where
open import Data.List.Base using (List; map)
open import Data.List.Properties using (map-id; map-cong; map-∘)
open import Data.Fin.Substitution using (Sub)
import Function.Base as Fun
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
private
variable
m n : ℕ
ListT : ℕ → Set ℓ
ListT = List Fun.∘ T
open module L = Lemmas₄ lemmas₄ using (_/_; id; _⊙_)
------------------------------------------------------------------------
-- Listwise application of a substitution, plus lemmas about it
infixl 8 _//_
_//_ : ListT m → Sub T m n → ListT n
ts // ρ = map (λ σ → σ / ρ) ts
appLemmas : AppLemmas ListT T
appLemmas = record
{ application = record { _/_ = _//_ }
; lemmas₄ = lemmas₄
; id-vanishes = λ ts → begin
ts // id ≡⟨ map-cong L.id-vanishes ts ⟩
map Fun.id ts ≡⟨ map-id ts ⟩
ts ∎
; /-⊙ = λ {_ _ _ ρ₁ ρ₂} ts → begin
ts // ρ₁ ⊙ ρ₂ ≡⟨ map-cong L./-⊙ ts ⟩
map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-∘ ts ⟩
ts // ρ₁ // ρ₂ ∎
} where open ≡-Reasoning
open AppLemmas appLemmas public
hiding (_/_) renaming (_/✶_ to _//✶_)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4