------------------------------------------------------------------------
-- The Agda standard library
--
-- List scans: properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Scans.Properties where
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_; toList)
import Data.List.Properties as List using (map-∘)
open import Data.List.Scans.Base using (scanr⁺; scanr; scanl⁺; scanl)
open import Function.Base using (_∘_; _$_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≗_; refl; trans; cong; cong₂)
private
variable
a b : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Properties
-- scanr⁺ and scanr
module _ (f : A → B → B) (e : B) where
private
h = List.foldr f e
scanr⁺-defn : scanr⁺ f e ≗ List⁺.map h ∘ List⁺.tails
scanr⁺-defn [] = refl
scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
in cong₂ (λ z → f x z ∷_) (cong List⁺.head eq) (cong toList eq)
scanr-defn : scanr f e ≗ List.map h ∘ List.tails
scanr-defn xs = cong toList (scanr⁺-defn xs)
-- scanl⁺ and scanl
module _ (f : A → B → A) where
private
h = List.foldl f
scanl⁺-defn : ∀ e → scanl⁺ f e ≗ List⁺.map (h e) ∘ List⁺.inits
scanl⁺-defn e [] = refl
scanl⁺-defn e (x ∷ xs) = let eq = scanl⁺-defn (f e x) xs in
cong (e ∷_) $ cong (f e x ∷_) $ trans (cong List⁺.tail eq) (List.map-∘ _)
scanl-defn : ∀ e → scanl f e ≗ List.map (h e) ∘ List.inits
scanl-defn e xs = cong toList (scanl⁺-defn e xs)
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