1
------------------------------------------------------------------------
2
-- Conversion of < to ≤, along with a number of properties
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
8
-- relation equivalent to the original one (and similarly for
11
open import Relation.Binary
13
module Relation.Binary.StrictToNonStrict
15
(_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
18
open import Relation.Nullary
19
open import Relation.Binary.Consequences
20
open import Data.Function
21
open import Data.Product
23
open import Data.Empty
25
------------------------------------------------------------------------
28
-- _<_ can be turned into _≤_ as follows:
31
x ≤ y = (x < y) ⊎ (x ≈ y)
33
------------------------------------------------------------------------
34
-- The converted relations have certain properties
35
-- (if the original relations have certain other properties)
40
antisym : IsEquivalence _≈_ →
44
antisym eq trans irrefl = as
46
module Eq = IsEquivalence eq
48
as : Antisymmetric _≈_ _≤_
50
as (inj₁ _) (inj₂ y≈x) = Eq.sym y≈x
51
as (inj₁ x<y) (inj₁ y<x) =
52
⊥-elim (trans∧irr⟶asym {≈ = _≈_} Eq.refl trans irrefl x<y y<x)
54
trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ →
55
Transitive _<_ → Transitive _≤_
56
trans eq <-resp-≈ <-trans = tr
58
module Eq = IsEquivalence eq
61
tr (inj₁ x<y) (inj₁ y<z) = inj₁ $ <-trans x<y y<z
62
tr (inj₁ x<y) (inj₂ y≈z) = inj₁ $ proj₁ <-resp-≈ y≈z x<y
63
tr (inj₂ x≈y) (inj₁ y<z) = inj₁ $ proj₂ <-resp-≈ (Eq.sym x≈y) y<z
64
tr (inj₂ x≈y) (inj₂ y≈z) = inj₂ $ Eq.trans x≈y y≈z
66
≤-resp-≈ : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → _≤_ Respects₂ _≈_
67
≤-resp-≈ eq <-resp-≈ = ((λ {_ _ _} → resp₁) , (λ {_ _ _} → resp₂))
69
module Eq = IsEquivalence eq
71
resp₁ : ∀ {x y' y} → y' ≈ y → x ≤ y' → x ≤ y
72
resp₁ y'≈y (inj₁ x<y') = inj₁ (proj₁ <-resp-≈ y'≈y x<y')
73
resp₁ y'≈y (inj₂ x≈y') = inj₂ (Eq.trans x≈y' y'≈y)
75
resp₂ : ∀ {y x' x} → x' ≈ x → x' ≤ y → x ≤ y
76
resp₂ x'≈x (inj₁ x'<y) = inj₁ (proj₂ <-resp-≈ x'≈x x'<y)
77
resp₂ x'≈x (inj₂ x'≈y) = inj₂ (Eq.trans (Eq.sym x'≈x) x'≈y)
79
total : Trichotomous _≈_ _<_ → Total _≤_
80
total <-tri x y with <-tri x y
81
... | tri< x<y x≉y x≯y = inj₁ (inj₁ x<y)
82
... | tri≈ x≮y x≈y x≯y = inj₁ (inj₂ x≈y)
83
... | tri> x≮y x≉y x>y = inj₂ (inj₁ x>y)
85
decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
86
decidable ≈-dec <-dec x y with ≈-dec x y | <-dec x y
87
... | yes x≈y | _ = yes (inj₂ x≈y)
88
... | no x≉y | yes x<y = yes (inj₁ x<y)
89
... | no x≉y | no x≮y = no helper
92
helper (inj₁ x<y) = x≮y x<y
93
helper (inj₂ x≈y) = x≉y x≈y
95
decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
96
decidable' compare x y with compare x y
97
... | tri< x<y _ _ = yes (inj₁ x<y)
98
... | tri≈ _ x≈y _ = yes (inj₂ x≈y)
99
... | tri> x≮y x≉y _ = no helper
102
helper (inj₁ x<y) = x≮y x<y
103
helper (inj₂ x≈y) = x≉y x≈y
added
removed
src/Relation/Binary/StrictToNonStrict.agda
