------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the generalised view of appending two lists
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Ternary.Appending.Properties where
open import Data.List.Base using (List; [])
open import Data.List.Relation.Ternary.Appending
open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
open import Data.Product.Base as Product using (∃-syntax; _×_; _,_)
open import Function.Base using (id)
open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Pointwise.Properties as Pw using (transitive)
open import Level using (Level)
open import Relation.Binary.Core using (REL; Rel; _⇒_)
open import Relation.Binary.Definitions using (Trans)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Binary.Construct.Composition using (_;_)
private
variable
a ℓ l r : Level
A A′ B B′ C C′ D D′ : Set a
R S T U V W X Y : REL A B ℓ
as bs cs ds : List A
module _ (RST : Trans R S T) (USV : Trans U S V) where
respʳ-≋ : Appending R U as bs cs → Pointwise S cs ds → Appending T V as bs ds
respʳ-≋ ([]++ rs) es = []++ Pw.transitive USV rs es
respʳ-≋ (l ∷ lrs) (e ∷ es) = RST l e ∷ respʳ-≋ lrs es
module _ {T : REL A B l} (RST : Trans R S T)
{W : REL A B r} (ERW : Trans U V W)
where
respˡ-≋ : ∀ {as′ bs′} → Pointwise R as′ as → Pointwise U bs′ bs →
Appending S V as bs cs → Appending T W as′ bs′ cs
respˡ-≋ [] esʳ ([]++ rs) = []++ Pw.transitive ERW esʳ rs
respˡ-≋ (eˡ ∷ esˡ) esʳ (l ∷ lrs) = RST eˡ l ∷ respˡ-≋ esˡ esʳ lrs
conicalˡ : Appending R S as bs [] → as ≡ []
conicalˡ ([]++ rs) = refl
conicalʳ : Appending R S as bs [] → bs ≡ []
conicalʳ ([]++ []) = refl
through→ :
(R ⇒ (S ; T)) →
((U ; V) ⇒ (W ; T)) →
∃[ xs ] Pointwise U as xs × Appending V R xs bs cs →
∃[ ys ] Appending W S as bs ys × Pointwise T ys cs
through→ f g (_ , [] , []++ rs) =
let _ , rs′ , ps′ = Pw.unzip (Pw.map f rs) in
_ , []++ rs′ , ps′
through→ f g (_ , p ∷ ps , l ∷ lrs) =
let _ , l′ , p′ = g (_ , p , l) in
Product.map _ (Product.map (l′ ∷_) (p′ ∷_)) (through→ f g (_ , ps , lrs))
through← :
((R ; S) ⇒ T) →
((U ; S) ⇒ (V ; W)) →
∃[ ys ] Appending U R as bs ys × Pointwise S ys cs →
∃[ xs ] Pointwise V as xs × Appending W T xs bs cs
through← f g (_ , []++ rs′ , ps′) =
_ , [] , []++ (Pw.transitive (λ r′ p′ → f (_ , r′ , p′)) rs′ ps′)
through← f g (_ , l′ ∷ lrs′ , p′ ∷ ps′) =
let _ , p , l = g (_ , l′ , p′) in
Product.map _ (Product.map (p ∷_) (l ∷_)) (through← f g (_ , lrs′ , ps′))
assoc→ :
(R ⇒ (S ; T)) →
((U ; V) ⇒ (W ; T)) →
((Y ; V) ⇒ X) →
∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds →
∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds
assoc→ f g h (_ , []++ rs , lrs′) =
let _ , mss , ss′ = through→ f g (_ , rs , lrs′) in
_ , mss , []++ ss′
assoc→ f g h (_ , l ∷ lrs , l′ ∷ lrs′) =
Product.map₂ (Product.map₂ (h (_ , l , l′) ∷_)) (assoc→ f g h (_ , lrs , lrs′))
assoc← :
((S ; T) ⇒ R) →
((W ; T) ⇒ (U ; V)) →
(X ⇒ (Y ; V)) →
∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds →
∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
assoc← f g h (_ , mss , []++ ss′) =
let _ , rs , lrs′ = through← f g (_ , mss , ss′) in
_ , []++ rs , lrs′
assoc← f g h (_ , mss , m′ ∷ mss′) =
let _ , l , l′ = h m′ in
Product.map _ (Product.map (l ∷_) (l′ ∷_)) (assoc← f g h (_ , mss , mss′))
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