------------------------------------------------------------------------
-- The Agda standard library
--
-- Property related to Grouped
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Unary.Grouped.Properties where
open import Data.Bool.Base using (true; false)
open import Data.List.Base using ([]; [_]; _∷_; map; derun)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as All
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.Grouped
open import Data.Product.Base using (_,_)
open import Function.Base using (_∘_; _on_)
open import Level using (Level)
open import Relation.Binary.Definitions as B
open import Relation.Binary.Core using (_⇔_; REL; Rel)
open import Relation.Unary as U using (Pred)
open import Relation.Nullary.Decidable.Core using (does; yes; no)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
private
variable
a b c p q : Level
A B C : Set a
------------------------------------------------------------------------
-- map
module _ (P : Rel A p) (Q : Rel B q) where
map⁺ : ∀ {f xs} → P ⇔ (Q on f) → Grouped P xs → Grouped Q (map f xs)
map⁺ P⇔Q [] = []
map⁺ P⇔Q@(_ , Q⇒P) (all[¬Px,xs] ∷≉ g[xs]) = All.gmap⁺ (_∘ Q⇒P) all[¬Px,xs] ∷≉ map⁺ P⇔Q g[xs]
map⁺ P⇔Q@(P⇒Q , _) (Px₁x₂ ∷≈ g[xs]) = P⇒Q Px₁x₂ ∷≈ map⁺ P⇔Q g[xs]
map⁻ : ∀ {f xs} → P ⇔ (Q on f) → Grouped Q (map f xs) → Grouped P xs
map⁻ {xs = []} P⇔Q [] = []
map⁻ {xs = _ ∷ []} P⇔Q ([] ∷≉ []) = [] ∷≉ []
map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(P⇒Q , _) (all[¬Qx,xs] ∷≉ g) = All.gmap⁻ (_∘ P⇒Q) all[¬Qx,xs] ∷≉ map⁻ P⇔Q g
map⁻ {xs = _ ∷ _ ∷ _} P⇔Q@(_ , Q⇒P) (Qx₁x₂ ∷≈ g) = Q⇒P Qx₁x₂ ∷≈ map⁻ P⇔Q g
------------------------------------------------------------------------
-- [_]
module _ (P : Rel A p) where
[_]⁺ : ∀ x → Grouped P [ x ]
[_]⁺ x = [] ∷≉ []
------------------------------------------------------------------------
-- derun
module _ {P : Rel A p} (P? : B.Decidable P) where
grouped[xs]⇒unique[derun[xs]] : ∀ xs → Grouped P xs → AllPairs (λ x y → ¬ P x y) (derun P? xs)
grouped[xs]⇒unique[derun[xs]] [] [] = []
grouped[xs]⇒unique[derun[xs]] (x ∷ []) ([] ∷≉ []) = [] ∷ []
grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (all[¬Px,y∷xs]@(¬Pxy ∷ _) ∷≉ grouped[y∷xs]) with P? x y
... | yes Pxy = contradiction Pxy ¬Pxy
... | no _ = All.derun⁺ P? all[¬Px,y∷xs] ∷ grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[y∷xs]
grouped[xs]⇒unique[derun[xs]] (x ∷ y ∷ xs) (Pxy ∷≈ grouped[xs]) with P? x y
... | yes _ = grouped[xs]⇒unique[derun[xs]] (y ∷ xs) grouped[xs]
... | no ¬Pxy = contradiction Pxy ¬Pxy
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