------------------------------------------------------------------------
-- 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 _//✶_)