/usr/share/agda-stdlib/Relation/Binary/Consequences.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------
module Relation.Binary.Consequences where
open import Relation.Binary.Core hiding (refl)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality.Core
open import Function
open import Data.Sum
open import Data.Product
open import Data.Empty
-- Some of the definitions can be found in the following module:
open import Relation.Binary.Consequences.Core public
trans∧irr⟶asym :
∀ {a ℓ₁ ℓ₂} {A : Set a} → {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Reflexive _≈_ →
Transitive _<_ → Irreflexive _≈_ _<_ → Asymmetric _<_
trans∧irr⟶asym refl trans irrefl = λ x<y y<x →
irrefl refl (trans x<y y<x)
irr∧antisym⟶asym :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ → Asymmetric _<_
irr∧antisym⟶asym irrefl antisym = λ x<y y<x →
irrefl (antisym x<y y<x) x<y
asym⟶antisym :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Asymmetric _<_ → Antisymmetric _≈_ _<_
asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
asym⟶irr :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
_<_ Respects₂ _≈_ → Symmetric _≈_ →
Asymmetric _<_ → Irreflexive _≈_ _<_
asym⟶irr {_<_ = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
where
y<y : y < y
y<y = proj₂ resp x≈y x<y
y<x : y < x
y<x = proj₁ resp (sym x≈y) y<y
total⟶refl :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
_∼_ Respects₂ _≈_ → Symmetric _≈_ →
Total _∼_ → _≈_ ⇒ _∼_
total⟶refl {_≈_ = _≈_} {_∼_ = _∼_} resp sym total = refl
where
refl : _≈_ ⇒ _∼_
refl {x} {y} x≈y with total x y
... | inj₁ x∼y = x∼y
... | inj₂ y∼x =
proj₁ resp x≈y (proj₂ resp (sym x≈y) y∼x)
total+dec⟶dec :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} →
_≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
Total _≤_ → Decidable _≈_ → Decidable _≤_
total+dec⟶dec {_≈_ = _≈_} {_≤_ = _≤_} refl antisym total _≟_ = dec
where
dec : Decidable _≤_
dec x y with total x y
... | inj₁ x≤y = yes x≤y
... | inj₂ y≤x with x ≟ y
... | yes x≈y = yes (refl x≈y)
... | no ¬x≈y = no (λ x≤y → ¬x≈y (antisym x≤y y≤x))
tri⟶asym :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Trichotomous _≈_ _<_ → Asymmetric _<_
tri⟶asym tri {x} {y} x<y x>y with tri x y
... | tri< _ _ x≯y = x≯y x>y
... | tri≈ _ _ x≯y = x≯y x>y
... | tri> x≮y _ _ = x≮y x<y
tri⟶irr :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
_<_ Respects₂ _≈_ → Symmetric _≈_ →
Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_
tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri)
tri⟶dec≈ :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Trichotomous _≈_ _<_ → Decidable _≈_
tri⟶dec≈ compare x y with compare x y
... | tri< _ x≉y _ = no x≉y
... | tri≈ _ x≈y _ = yes x≈y
... | tri> _ x≉y _ = no x≉y
tri⟶dec< :
∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
Trichotomous _≈_ _<_ → Decidable _<_
tri⟶dec< compare x y with compare x y
... | tri< x<y _ _ = yes x<y
... | tri≈ x≮y _ _ = no x≮y
... | tri> x≮y _ _ = no x≮y
map-NonEmpty : ∀ {a b p q} {A : Set a} {B : Set b}
{P : REL A B p} {Q : REL A B q} →
P ⇒ Q → NonEmpty P → NonEmpty Q
map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))
|