------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of membership for AVL sets
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Tree.AVL.Sets.Membership.Properties
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
where
open import Data.Bool.Base using (true; false)
open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
open import Data.Sum.Base as Sum using (_⊎_)
open import Data.Unit.Base using (tt)
open import Function.Base using (_∘_; _∘′_; const)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Nullary using (¬_; yes; no; Reflects)
open import Relation.Nullary.Reflects using (fromEquivalence)
open StrictTotalOrder strictTotalOrder renaming (Carrier to A)
open import Data.Tree.AVL.Sets strictTotalOrder
open import Data.Tree.AVL.Sets.Membership strictTotalOrder
open import Data.Tree.AVL.Map.Membership.Propositional strictTotalOrder using (_∈ₖᵥ_)
import Data.Tree.AVL.Map.Membership.Propositional.Properties strictTotalOrder as Map
open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ
private
variable
x y : A
s : ⟨Set⟩
∈toMap : x ∈ s → (x , tt) ∈ₖᵥ s
∈toMap = Mapₚ.map (_, refl)
∈fromMap : (x , tt) ∈ₖᵥ s → x ∈ s
∈fromMap = Mapₚ.map proj₁
------------------------------------------------------------------------
-- empty
∈-empty : x ∉ empty
∈-empty = Map.∈ₖᵥ-empty ∘ ∈toMap
------------------------------------------------------------------------
-- singleton
∈-singleton⁺ : x ∈ singleton x
∈-singleton⁺ = ∈fromMap Map.∈ₖᵥ-singleton⁺
∈-singleton⁻ : x ∈ singleton y → x ≈ y
∈-singleton⁻ p = proj₁ (Map.∈ₖᵥ-singleton⁻ (∈toMap p))
------------------------------------------------------------------------
-- insert
∈-insert⁺ : x ∈ s → x ∈ insert y s
∈-insert⁺ {x = x} {s = s} {y = y} x∈s with x ≟ y
... | yes x≈y = ∈fromMap (Map.∈ₖᵥ-Respectsˡ (Eq.sym x≈y , refl) Map.∈ₖᵥ-insert⁺⁺)
... | no x≉y = ∈fromMap (Map.∈ₖᵥ-insert⁺ x≉y (∈toMap x∈s))
∈-insert⁺⁺ : x ∈ insert x s
∈-insert⁺⁺ = ∈fromMap Map.∈ₖᵥ-insert⁺⁺
∈-insert⁻ : x ∈ insert y s → x ≈ y ⊎ x ∈ s
∈-insert⁻ = Sum.map proj₁ (∈fromMap ∘ proj₂) ∘ Map.∈ₖᵥ-insert⁻ ∘ ∈toMap
------------------------------------------------------------------------
-- member
∈-member : x ∈ s → member x s ≡ true
∈-member = Map.∈ₖᵥ-member ∘′ ∈toMap
∉-member : x ∉ s → member x s ≡ false
∉-member x∉s = Map.∉ₖᵥ-member (const (x∉s ∘ ∈fromMap))
member-∈ : member x s ≡ true → x ∈ s
member-∈ = ∈fromMap ∘′ proj₂ ∘′ Map.member-∈ₖᵥ
member-∉ : member x s ≡ false → x ∉ s
member-∉ p = Map.member-∉ₖᵥ p tt ∘ ∈toMap
member-Reflects-∈ : Reflects (x ∈ s) (member x s)
member-Reflects-∈ {x = x} {s = s} with member x s in eq
... | true = Reflects.ofʸ (member-∈ eq)
... | false = Reflects.ofⁿ (member-∉ eq)
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