← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Consequences.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/Consequences.agda
7
7
module Relation.Binary.Consequences where
8
8
 
9
9
open import Relation.Binary.Core hiding (refl)
10
 
open import Relation.Nullary.Core
 
10
open import Relation.Nullary
11
11
open import Relation.Binary.PropositionalEquality.Core
12
 
open import Data.Function
 
12
open import Function
13
13
open import Data.Sum
14
14
open import Data.Product
15
15
open import Data.Empty
19
19
open import Relation.Binary.Consequences.Core public
20
20
 
21
21
trans∧irr⟶asym :
22
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} → {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
23
 
  Reflexive ≈ →
24
 
  Transitive < → Irreflexive ≈ < → Asymmetric <
 
22
  ∀ {a ℓ₁ ℓ₂} {A : Set a} → {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
23
  Reflexive _≈_ →
 
24
  Transitive _<_ → Irreflexive _≈_ _<_ → Asymmetric _<_
25
25
trans∧irr⟶asym refl trans irrefl = λ x<y y<x →
26
26
  irrefl refl (trans x<y y<x)
27
27
 
28
28
irr∧antisym⟶asym :
29
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
30
 
  Irreflexive ≈ < → Antisymmetric ≈ < → Asymmetric <
 
29
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
30
  Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ → Asymmetric _<_
31
31
irr∧antisym⟶asym irrefl antisym = λ x<y y<x →
32
32
  irrefl (antisym x<y y<x) x<y
33
33
 
34
34
asym⟶antisym :
35
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
36
 
  Asymmetric < → Antisymmetric ≈ <
 
35
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
36
  Asymmetric _<_ → Antisymmetric _≈_ _<_
37
37
asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
38
38
 
39
39
asym⟶irr :
40
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
41
 
  < Respects₂ ≈ → Symmetric ≈ →
42
 
  Asymmetric < → Irreflexive ≈ <
43
 
asym⟶irr {< = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
 
40
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
41
  _<_ Respects₂ _≈_ → Symmetric _≈_ →
 
42
  Asymmetric _<_ → Irreflexive _≈_ _<_
 
43
asym⟶irr {_<_ = _<_} resp sym asym {x} {y} x≈y x<y = asym x<y y<x
44
44
  where
45
45
  y<y : y < y
46
46
  y<y = proj₂ resp x≈y x<y
48
48
  y<x = proj₁ resp (sym x≈y) y<y
49
49
 
50
50
total⟶refl :
51
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} →
52
 
  ∼ Respects₂ ≈ → Symmetric ≈ →
53
 
  Total ∼ → ≈ ⇒ ∼
54
 
total⟶refl {≈ = ≈} {∼ = ∼} resp sym total = refl
 
51
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
 
52
  _∼_ Respects₂ _≈_ → Symmetric _≈_ →
 
53
  Total _∼_ → _≈_ ⇒ _∼_
 
54
total⟶refl {_≈_ = _≈_} {_∼_ = _∼_} resp sym total = refl
55
55
  where
56
 
  refl : ≈ ⇒ ∼
 
56
  refl : _≈_ ⇒ _∼_
57
57
  refl {x} {y} x≈y with total x y
58
58
  ...              | inj₁ x∼y = x∼y
59
59
  ...              | inj₂ y∼x =
60
60
    proj₁ resp x≈y (proj₂ resp (sym x≈y) y∼x)
61
61
 
62
62
total+dec⟶dec :
63
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {≤ : Rel A ℓ₂} →
64
 
  ≈ ⇒ ≤ → Antisymmetric ≈ ≤ →
65
 
  Total ≤ → Decidable ≈ → Decidable ≤
66
 
total+dec⟶dec {≈ = ≈} {≤ = ≤} refl antisym total _≟_ = dec
 
63
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} →
 
64
  _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
 
65
  Total _≤_ → Decidable _≈_ → Decidable _≤_
 
66
total+dec⟶dec {_≈_ = _≈_} {_≤_ = _≤_} refl antisym total _≟_ = dec
67
67
  where
68
 
  dec : Decidable ≤
 
68
  dec : Decidable _≤_
69
69
  dec x y with total x y
70
70
  ... | inj₁ x≤y = yes x≤y
71
71
  ... | inj₂ y≤x with x ≟ y
73
73
  ...   | no  ¬x≈y = no (λ x≤y → ¬x≈y (antisym x≤y y≤x))
74
74
 
75
75
tri⟶asym :
76
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
77
 
  Trichotomous ≈ < → Asymmetric <
 
76
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
77
  Trichotomous _≈_ _<_ → Asymmetric _<_
78
78
tri⟶asym tri {x} {y} x<y x>y with tri x y
79
79
... | tri< _   _ x≯y = x≯y x>y
80
80
... | tri≈ _   _ x≯y = x≯y x>y
81
81
... | tri> x≮y _ _   = x≮y x<y
82
82
 
83
83
tri⟶irr :
84
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
85
 
  < Respects₂ ≈ → Symmetric ≈ →
86
 
  Trichotomous ≈ < → Irreflexive ≈ <
 
84
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
85
  _<_ Respects₂ _≈_ → Symmetric _≈_ →
 
86
  Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_
87
87
tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri)
88
88
 
89
89
tri⟶dec≈ :
90
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
91
 
  Trichotomous ≈ < → Decidable ≈
 
90
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
91
  Trichotomous _≈_ _<_ → Decidable _≈_
92
92
tri⟶dec≈ compare x y with compare x y
93
93
... | tri< _ x≉y _ = no  x≉y
94
94
... | tri≈ _ x≈y _ = yes x≈y
95
95
... | tri> _ x≉y _ = no  x≉y
96
96
 
97
97
tri⟶dec< :
98
 
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} →
99
 
  Trichotomous ≈ < → Decidable <
 
98
  ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
 
99
  Trichotomous _≈_ _<_ → Decidable _<_
100
100
tri⟶dec< compare x y with compare x y
101
101
... | tri< x<y _ _ = yes x<y
102
102
... | tri≈ x≮y _ _ = no  x≮y