{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Unary.First.Properties where
open import Data.Fin.Base using (suc)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.List.Relation.Unary.First
import Data.Sum as Sum
open import Function.Base using (_∘′_; _$_; _∘_; id)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
open import Relation.Nullary.Negation using (contradiction)
module _ {a b p q} {A : Set a} {B : Set b} {P : Pred B p} {Q : Pred B q} where
map⁺ : {f : A → B} → First (P ∘′ f) (Q ∘′ f) ⊆ First P Q ∘′ List.map f
map⁺ [ qfx ] = [ qfx ]
map⁺ (pfxs ∷ pqfxs) = pfxs ∷ map⁺ pqfxs
map⁻ : {f : A → B} → First P Q ∘′ List.map f ⊆ First (P ∘′ f) (Q ∘′ f)
map⁻ {f} {x ∷ xs} [ qfx ] = [ qfx ]
map⁻ {f} {x ∷ xs} (pfx ∷ pqfxs) = pfx ∷ map⁻ pqfxs
module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
++⁺ : ∀ {xs ys} → All P xs → First P Q ys → First P Q (xs List.++ ys)
++⁺ [] pqys = pqys
++⁺ (px ∷ pxs) pqys = px ∷ ++⁺ pxs pqys
⁺++ : ∀ {xs} → First P Q xs → ∀ ys → First P Q (xs List.++ ys)
⁺++ [ qx ] ys = [ qx ]
⁺++ (px ∷ pqxs) ys = px ∷ ⁺++ pqxs ys
module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
All⇒¬First p⇒¬q (px ∷ pxs) [ qx ] = contradiction qx (p⇒¬q px)
All⇒¬First p⇒¬q (_ ∷ pxs) (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
First⇒¬All q⇒¬p [ qx ] (px ∷ pxs) = q⇒¬p qx px
First⇒¬All q⇒¬p (_ ∷ pqxs) (_ ∷ pxs) = First⇒¬All q⇒¬p pqxs pxs
unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
unique-index p⇒¬q [ _ ] [ _ ] = refl
unique-index p⇒¬q [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
unique-index p⇒¬q (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = ≡.cong suc (unique-index p⇒¬q f₁ f₂)
irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
irrelevant p⇒¬q p-irr q-irr [ px ] [ qx ] = ≡.cong [_] (q-irr px qx)
irrelevant p⇒¬q p-irr q-irr [ qx ] (px ∷ _) = contradiction qx (p⇒¬q px)
irrelevant p⇒¬q p-irr q-irr (px ∷ _) [ qx ] = contradiction qx (p⇒¬q px)
irrelevant p⇒¬q p-irr q-irr (px ∷ f) (qx ∷ g) =
≡.cong₂ _∷_ (p-irr px qx) (irrelevant p⇒¬q p-irr q-irr f g)
module _ {a p} {A : Set a} {P : Pred A p} where
first? : Decidable P → Decidable (First P (∁ P))
first? P? xs = Sum.toDec
$ Sum.map₂ (All⇒¬First contradiction)
$ first (Sum.fromDec ∘ P?) xs
cofirst? : Decidable P → Decidable (First (∁ P) P)
cofirst? P? xs = Sum.toDec
$ Sum.map₂ (All⇒¬First id)
$ first (Sum.swap ∘ Sum.fromDec ∘ P?) xs
module _ {a p} {A : Set a} {P : Pred A p} where
fromAny∘toAny≗id : ∀ {xs} → fromAny {Q = P} {x = xs} ∘′ toAny ≗ id
fromAny∘toAny≗id [ qx ] = refl
fromAny∘toAny≗id (px ∷ pqxs) = ≡.cong (_ ∷_) (fromAny∘toAny≗id pqxs)
toAny∘fromAny≗id : ∀ {xs} → toAny {Q = P} ∘′ fromAny {x = xs} ≗ id
toAny∘fromAny≗id (here px) = refl
toAny∘fromAny≗id (there v) = ≡.cong there (toAny∘fromAny≗id v)
module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
toView : ∀ {as} → First P Q as → FirstView P Q as
toView [ qx ] = [] ++ qx ∷ _
toView (px ∷ pqxs) with toView pqxs
... | pxs ++ qy ∷ ys = (px ∷ pxs) ++ qy ∷ ys
fromView : ∀ {as} → FirstView P Q as → First P Q as
fromView (pxs ++ qy ∷ ys) = ++⁺ pxs [ qy ]