1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
4
-- Compatibility module. Pending for removal. Use
5
-- Data.Fin.Subset.Properties instead.
4
6
------------------------------------------------------------------------
6
8
module Data.Fin.Subset.Props where
9
import Algebra.Props.BooleanAlgebra as BoolProp
10
open import Data.Empty using (⊥-elim)
11
open import Data.Fin using (Fin); open Data.Fin.Fin
12
open import Data.Fin.Subset
13
open import Data.Nat using (ℕ)
14
open import Data.Product
15
open import Data.Sum as Sum
16
open import Data.Vec hiding (_∈_)
18
open import Function.Equality using (_⟨$⟩_)
19
open import Function.Equivalence
20
using (_⇔_; equivalence; module Equivalence)
21
open import Relation.Binary
22
open import Relation.Binary.PropositionalEquality as P using (_≡_)
24
------------------------------------------------------------------------
26
drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
27
drop-there (there x∈p) = x∈p
29
drop-∷-⊆ : ∀ {n s₁ s₂} {p₁ p₂ : Subset n} → s₁ ∷ p₁ ⊆ s₂ ∷ p₂ → p₁ ⊆ p₂
30
drop-∷-⊆ p₁s₁⊆p₂s₂ x∈p₁ = drop-there $ p₁s₁⊆p₂s₂ (there x∈p₁)
32
drop-∷-Empty : ∀ {n s} {p : Subset n} → Empty (s ∷ p) → Empty p
33
drop-∷-Empty ¬∃∈ (x , x∈p) = ¬∃∈ (suc x , there x∈p)
35
------------------------------------------------------------------------
37
∉⊥ : ∀ {n} {x : Fin n} → x ∉ ⊥
40
⊥⊆ : ∀ {n} {p : Subset n} → ⊥ ⊆ p
44
Empty-unique : ∀ {n} {p : Subset n} →
46
Empty-unique {p = []} ¬∃∈ = P.refl
47
Empty-unique {p = s ∷ p} ¬∃∈ with Empty-unique (drop-∷-Empty ¬∃∈)
48
Empty-unique {p = outside ∷ .⊥} ¬∃∈ | P.refl = P.refl
49
Empty-unique {p = inside ∷ .⊥} ¬∃∈ | P.refl =
50
⊥-elim (¬∃∈ (zero , here))
52
------------------------------------------------------------------------
54
∈⊤ : ∀ {n} {x : Fin n} → x ∈ ⊤
56
∈⊤ {x = suc x} = there ∈⊤
58
⊆⊤ : ∀ {n} {p : Subset n} → p ⊆ ⊤
61
------------------------------------------------------------------------
63
x∈⁅y⁆⇔x≡y : ∀ {n} {x y : Fin n} → x ∈ ⁅ y ⁆ ⇔ x ≡ y
64
x∈⁅y⁆⇔x≡y {x = x} {y} =
65
equivalence (to y) (λ x≡y → P.subst (λ y → x ∈ ⁅ y ⁆) x≡y (x∈⁅x⁆ x))
68
to : ∀ {n x} (y : Fin n) → x ∈ ⁅ y ⁆ → x ≡ y
69
to (suc y) (there p) = P.cong suc (to y p)
71
to zero (there p) with ∉⊥ p
74
x∈⁅x⁆ : ∀ {n} (x : Fin n) → x ∈ ⁅ x ⁆
76
x∈⁅x⁆ (suc x) = there (x∈⁅x⁆ x)
78
------------------------------------------------------------------------
80
∪⇔⊎ : ∀ {n} {p₁ p₂ : Subset n} {x} → x ∈ p₁ ∪ p₂ ⇔ (x ∈ p₁ ⊎ x ∈ p₂)
81
∪⇔⊎ = equivalence (to _ _) from
83
to : ∀ {n} (p₁ p₂ : Subset n) {x} → x ∈ p₁ ∪ p₂ → x ∈ p₁ ⊎ x ∈ p₂
85
to (inside ∷ p₁) (s₂ ∷ p₂) here = inj₁ here
86
to (outside ∷ p₁) (inside ∷ p₂) here = inj₂ here
87
to (s₁ ∷ p₁) (s₂ ∷ p₂) (there x∈p₁∪p₂) =
88
Sum.map there there (to p₁ p₂ x∈p₁∪p₂)
90
⊆∪ˡ : ∀ {n p₁} (p₂ : Subset n) → p₁ ⊆ p₁ ∪ p₂
92
⊆∪ˡ (s ∷ p₂) here = here
93
⊆∪ˡ (s ∷ p₂) (there x∈p₁) = there (⊆∪ˡ p₂ x∈p₁)
95
⊆∪ʳ : ∀ {n} (p₁ p₂ : Subset n) → p₂ ⊆ p₁ ∪ p₂
96
⊆∪ʳ p₁ p₂ rewrite BooleanAlgebra.∨-comm (booleanAlgebra _) p₁ p₂
99
from : ∀ {n} {p₁ p₂ : Subset n} {x} → x ∈ p₁ ⊎ x ∈ p₂ → x ∈ p₁ ∪ p₂
100
from (inj₁ x∈p₁) = ⊆∪ˡ _ x∈p₁
101
from (inj₂ x∈p₂) = ⊆∪ʳ _ _ x∈p₂
103
------------------------------------------------------------------------
106
module NaturalPoset where
108
open module BA {n} = BoolProp (booleanAlgebra n) public
110
open module Po {n} = Poset (poset {n = n}) public
112
-- _⊆_ is equivalent to the natural lattice order.
114
orders-equivalent : ∀ {n} {p₁ p₂ : Subset n} → p₁ ⊆ p₂ ⇔ p₁ ≤ p₂
115
orders-equivalent = equivalence (to _ _) (from _ _)
117
to : ∀ {n} (p₁ p₂ : Subset n) → p₁ ⊆ p₂ → p₁ ≤ p₂
118
to [] [] p₁⊆p₂ = P.refl
119
to (inside ∷ p₁) (_ ∷ p₂) p₁⊆p₂ with p₁⊆p₂ here
120
to (inside ∷ p₁) (.inside ∷ p₂) p₁⊆p₂ | here = P.cong (_∷_ inside) (to p₁ p₂ (drop-∷-⊆ p₁⊆p₂))
121
to (outside ∷ p₁) (_ ∷ p₂) p₁⊆p₂ = P.cong (_∷_ outside) (to p₁ p₂ (drop-∷-⊆ p₁⊆p₂))
123
from : ∀ {n} (p₁ p₂ : Subset n) → p₁ ≤ p₂ → p₁ ⊆ p₂
124
from [] [] p₁≤p₂ x = x
125
from (.inside ∷ _) (_ ∷ _) p₁≤p₂ here rewrite P.cong head p₁≤p₂ = here
126
from (_ ∷ p₁) (_ ∷ p₂) p₁≤p₂ (there xs[i]=x) =
127
there (from p₁ p₂ (P.cong tail p₁≤p₂) xs[i]=x)
130
poset : ℕ → Poset _ _ _
135
; isPartialOrder = record
136
{ isPreorder = record
137
{ isEquivalence = P.isEquivalence
138
; reflexive = λ i≡j → from ⟨$⟩ reflexive i≡j
139
; trans = λ x⊆y y⊆z → from ⟨$⟩ trans (to ⟨$⟩ x⊆y) (to ⟨$⟩ y⊆z)
141
; antisym = λ x⊆y y⊆x → antisym (to ⟨$⟩ x⊆y) (to ⟨$⟩ y⊆x)
146
open module E {p₁ p₂} =
147
Equivalence (orders-equivalent {n = n} {p₁ = p₁} {p₂ = p₂})
10
open import Data.Fin.Subset.Properties public
added
removed
src/Data/Fin/Subset/Props.agda
