------------------------------------------------------------------------
-- The Agda standard library
--
-- Core properties related to propositional list membership.
------------------------------------------------------------------------
-- This file is needed to break the cyclic dependency with the proof
-- `Any-cong` in `Data.List.Relation.Unary.Any.Properties` which relies
-- on `Any↔` defined in this file.
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Membership.Propositional.Properties.Core where
open import Data.List.Base using (List; [])
open import Data.List.Membership.Propositional using (_∈_; _∉_; find; lose)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.Product.Base as Product using (_,_; ∃; _×_)
open import Function.Base using (flip; id; _∘_)
open import Function.Bundles using (_↔_; mk↔ₛ′)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; trans; cong; resp)
open import Relation.Unary using (Pred; _⊆_)
private
variable
a p q : Level
A : Set a
x : A
xs : List A
------------------------------------------------------------------------
-- Basics
∉[] : x ∉ []
∉[] ()
------------------------------------------------------------------------
-- find satisfies a simple equality when the predicate is a
-- propositional equality.
find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl)
find-∈ (here refl) = refl
find-∈ (there x∈xs)
= cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find-∈ x∈xs)
------------------------------------------------------------------------
-- Lemmas relating map and find.
module _ {P : Pred A p} where
map∘find : (p : Any P xs) → let x , x∈xs , px = find p in
{f : (x ≡_) ⊆ P} → f refl ≡ px →
Any.map f x∈xs ≡ p
map∘find (here p) hyp = cong here hyp
map∘find (there p) hyp = cong there (map∘find p hyp)
find∘map : ∀ {Q : Pred A q} {xs} (p : Any P xs) (f : P ⊆ Q) →
let x , x∈xs , px = find p in
find (Any.map f p) ≡ (x , x∈xs , f px)
find∘map (here p) f = refl
find∘map (there p) f
= cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find∘map p f)
------------------------------------------------------------------------
-- Any can be expressed using _∈_
module _ {P : Pred A p} where
∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs
∃∈-Any (x , x∈xs , px) = lose x∈xs px
∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
∃∈-Any∘find p = map∘find p refl
find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
find∘∃∈-Any p@(x , x∈xs , px)
= trans (find∘map x∈xs (flip (resp P) px))
(cong (λ (x , x∈xs , eq) → x , x∈xs , resp P eq px) (find-∈ x∈xs))
Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs
Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any
------------------------------------------------------------------------
-- Hence, find and lose are inverses (more or less).
lose∘find : ∀ {P : Pred A p} {xs} (p : Any P xs) → ∃∈-Any (find p) ≡ p
lose∘find = ∃∈-Any∘find
find∘lose : ∀ (P : Pred A p) {x xs}
(x∈xs : x ∈ xs) (px : P x) →
find (lose {P = P} x∈xs px) ≡ (x , x∈xs , px)
find∘lose P {x} x∈xs px = find∘∃∈-Any (x , x∈xs , px)
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