------------------------------------------------------------------------
-- The Agda standard library
--
-- Symmetric interior of a binary relation
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Construct.Interior.Symmetric where
open import Data.Bool.Base using (_∧_)
open import Function.Base using (flip; _∘_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive; Trans; Asymmetric; Empty; Decidable)
open import Relation.Binary.Structures
using (IsEquivalence; IsPreorder; IsPartialOrder; IsDecPartialOrder
; IsDecEquivalence)
open import Relation.Binary.Bundles using (Poset; DecPoset)
open import Relation.Nullary.Decidable.Core
open import Relation.Nullary.Reflects
private
variable
a ℓ : Level
A : Set a
R S T : Rel A ℓ
------------------------------------------------------------------------
-- Definition
infixr 4 _,_
record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where
constructor _,_
field
lhs≤rhs : R x y
rhs≤lhs : R y x
open SymInterior public
------------------------------------------------------------------------
-- Properties
-- The symmetric interior is symmetric.
symmetric : Symmetric (SymInterior R)
symmetric (r , r′) = r′ , r
-- The symmetric interior of R is greater than (or equal to) any other symmetric
-- relation contained by R.
unfold : Symmetric S → S ⇒ R → S ⇒ SymInterior R
unfold sym f s = f s , f (sym s)
-- SymInterior preserves various properties.
reflexive : Reflexive R → Reflexive (SymInterior R)
reflexive refl = refl , refl
trans : Trans R S T → Trans S R T →
Trans (SymInterior R) (SymInterior S) (SymInterior T)
trans trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′
transitive : Transitive R → Transitive (SymInterior R)
transitive tr = trans tr tr
-- The symmetric interior of a strict relation is empty.
asymmetric⇒empty : Asymmetric R → Empty (SymInterior R)
asymmetric⇒empty asym (r , r′) = asym r r′
-- Decidability
decidable : Decidable R → Decidable (SymInterior R)
does (decidable R? x y) = does (R? x y) ∧ does (R? y x)
proof (decidable R? x y) = proof (R? x y) reflects proof (R? y x)
where
_reflects_ : ∀ {bxy byx} → Reflects (R x y) bxy → Reflects (R y x) byx →
Reflects (SymInterior R x y) (bxy ∧ byx)
ofʸ rxy reflects ofʸ ryx = of (rxy , ryx)
ofʸ rxy reflects ofⁿ ¬ryx = of (¬ryx ∘ rhs≤lhs)
ofⁿ ¬rxy reflects _ = of (¬rxy ∘ lhs≤rhs)
-- A reflexive transitive relation _≤_ gives rise to a poset in which the
-- equivalence relation is SymInterior _≤_.
module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
isEquivalence : IsEquivalence (SymInterior R)
isEquivalence = record
{ refl = reflexive refl
; sym = symmetric
; trans = transitive trans
}
isPreorder : IsPreorder (SymInterior R) R
isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = lhs≤rhs
; trans = trans
}
isPartialOrder : IsPartialOrder (SymInterior R) R
isPartialOrder = record
{ isPreorder = isPreorder
; antisym = _,_
}
poset : Poset _ ℓ ℓ
poset = record { isPartialOrder = isPartialOrder }
module _ (R? : Decidable R) where
isDecPartialOrder : IsDecPartialOrder (SymInterior R) R
isDecPartialOrder = record
{ isPartialOrder = isPartialOrder
; _≟_ = decidable R?
; _≤?_ = R?
}
decPoset : DecPoset _ ℓ ℓ
decPoset = record { isDecPartialOrder = isDecPartialOrder }
open DecPoset public
using (isDecPreorder; decPreorder)
isDecEquivalence : IsDecEquivalence (SymInterior R)
isDecEquivalence = DecPoset.Eq.isDecEquivalence decPoset
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