------------------------------------------------------------------------ -- The Agda standard library -- -- Data.List.Any.Membership instantiated with propositional equality, -- along with some additional definitions. ------------------------------------------------------------------------ module Data.List.Any.Membership.Propositional where open import Data.Empty open import Data.Fin open import Function.Inverse using (_↔_) open import Function.Related as Related hiding (_∼[_]_) open import Data.List.Base as List using (List; []; _∷_) open import Data.List.Any using (Any; map) import Data.List.Any.Membership as Membership open import Data.Product as Prod using (∃; _×_; _,_; uncurry′; proj₂) open import Relation.Nullary open import Relation.Binary hiding (Decidable) import Relation.Binary.InducedPreorders as Ind open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_) open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) private module M {a} {A : Set a} = Membership (PropEq.setoid A) open M public hiding (lose) lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs lose {P = P} = M.lose (PropEq.subst P) -- _⊆_ is a preorder. ⊆-preorder : ∀ {a} → Set a → Preorder _ _ _ ⊆-preorder A = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_ (PropEq.subst (_∈_ _)) -- Set and bag equality and related preorders. open Related public using (Kind; Symmetric-kind) renaming ( implication to subset ; reverse-implication to superset ; equivalence to set ; injection to subbag ; reverse-injection to superbag ; bijection to bag ) [_]-Order : Kind → ∀ {a} → Set a → Preorder _ _ _ [ k ]-Order A = Related.InducedPreorder₂ k (_∈_ {A = A}) [_]-Equality : Symmetric-kind → ∀ {a} → Set a → Setoid _ _ [ k ]-Equality A = Related.InducedEquivalence₂ k (_∈_ {A = A}) infix 4 _∼[_]_ _∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _ _∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys -- Bag equality implies the other relations. bag-=⇒ : ∀ {k a} {A : Set a} {xs ys : List A} → xs ∼[ bag ] ys → xs ∼[ k ] ys bag-=⇒ xs≈ys = ↔⇒ xs≈ys -- "Equational" reasoning for _⊆_. module ⊆-Reasoning where import Relation.Binary.PreorderReasoning as PreR private open module PR {a} {A : Set a} = PreR (⊆-preorder A) public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_) infixr 2 _∼⟨_⟩_ infix 1 _∈⟨_⟩_ _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs _∼⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} → xs ∼[ ⌊ k ⌋→ ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs xs ∼⟨ xs≈ys ⟩ ys≈zs = xs ⊆⟨ ⇒→ xs≈ys ⟩ ys≈zs