Lattices.Bounded.Covers¶
Join covers and the sets D_k(L)¶
This is the Lattices.Bounded.Covers module of the agda-lattices library.
A join cover of an element a of a lattice L is a finite set S with
a ≤ ⋁S; it is nontrivial when a ≰ s for every s ∈ S; and a set T
refines S, written T ≪ S, when every member of T lies below some member
of S (Freese, Ježek, and Nation (1995), Section II.1, pp. 29 to 30). The
sets D_k(L) of p. 31 are defined by induction: D₀(L) is the set of join
prime elements, those with no nontrivial join cover, and D_{k+1}(L) is the
set of elements each of whose nontrivial join covers refines to a join cover
inside D_k(L). The sets increase with k, D(L) is their union, and the
condition D(L) = L is the book's definition of a lower bounded lattice, for a
finitely generated one (Theorem 2.13, condition (3)): its constructive content,
that every element has a rank k with a refinement datum, is what lets the
least preimages of a bounded epimorphism be computed
(Lattices.Bounded.Preimage).
This module defines the vocabulary for any lattice of the Setoid tree, with
join covers as nonempty lists (_≤⋁_ of
Lattices.Generation), so that the least element, which lies below every
member of every list, has no nontrivial join cover and is join prime, as the
book's convention for finite lattices wants. It proves that the sets increase
(D-mono, D-≤), that they respect the equality
of the lattice, that a join of elements of D_k lies in D_{k+1} when the
order is decided (D-∨, the book's argument on p. 31, which
splits a cover of a ∨ b according to whether it is trivial for a), and that
in a lattice satisfying Whitman's condition (W) each D_k is closed under
meets (D-∧, p. 33). From the last two facts, Theorem 2.10 (1)
follows: in a lattice with (W) and a decided order, every element generated by
join prime elements lies in some D_k (D-term), and if the
join prime elements generate the lattice then D(L) = L
(D-generated). The free lattice FL(X) on a set with
decidable equality is the first instance (Corollary 2.11,
FL-D-total), and so is its dual, since the generators are
meet prime too (FL-Dᵈ-total). The dual sets Dᵈ_k(L) are
the sets D_k of the dual lattice of Lattices.Dual,
and (W) passes to the dual (SatisfiesW-dual).
Not formalized here: the minimal join cover refinement property and the sets
M(a) of minimal nontrivial join covers (p. 30), which the book uses for
Theorem 5.7 and which Kostinsky's route to his theorem does not need
(Lattices.Kostinsky); and the finite theory of the D relation, which is
Lattices.Bounded.Finite's.
Join covers, refinement, and the sets D_k¶
Fix a lattice 𝑳, with the meet order of
Classical.Properties.Lattice and the joins of nonempty lists of
Lattices.Generation. a ≤⋁ S says that S is a join cover of a,
Nontrivial a S that it is nontrivial, and
T ≪ S that T refines S. Join primality is stated for
binary joins (IsJoinPrime); the list form follows
(joinPrime-list). D k a is membership of
a in D_k(L), with the refinement of a nontrivial cover as data, and
D-total is D(L) = L: every element in some D_k, the k
being its rank.
module _ (𝑳 : Lattice α ρ) where open Lattice-Op 𝑳 using ( _∧_ ; _∨_ ) open Lattice-Order 𝑳 using ( _≤_ ; ≤-refl ; ≤-trans ; ≤-reflexive ; ≤-respˡ-≈ ; ∧-lowerˡ ; ∧-lowerʳ ; ∨-upperˡ ; ∨-upperʳ ) open Setoid 𝔻[ proj₁ 𝑳 ] using ( _≈_ ; sym ) private L : Type α L = 𝕌[ proj₁ 𝑳 ] infix 4 _≤⋁ᴸ_ _≤⋁ᴸ_ : L → List L → Type (α ⊔ˡ ρ) _≤⋁ᴸ_ = _≤⋁_ 𝑳 -- A join cover S of a is nontrivial: a lies below no member of S. Nontrivial : L → List L → Type (α ⊔ˡ ρ) Nontrivial a S = All (λ s → ¬ (a ≤ s)) S infix 4 _≪_ -- T refines S: every member of T lies below some member of S. _≪_ : List L → List L → Type (α ⊔ˡ ρ) T ≪ S = All (λ t → Any (t ≤_) S) T -- a is join prime: below a join only when below a joinand. IsJoinPrime : L → Type (α ⊔ˡ ρ) IsJoinPrime a = ∀ {b c} → a ≤ b ∨ c → a ≤ b ⊎ a ≤ c -- The sets D_k(L) of FJN p. 31: the join prime elements, then the elements each of -- whose nontrivial join covers refines to a join cover inside the previous set. D : ℕ → L → Type (α ⊔ˡ ρ) D zero a = IsJoinPrime a D (suc k) a = (S : List L) → a ≤⋁ᴸ S → Nontrivial a S → Σ[ T ∈ List L ] (T ≪ S) × All (D k) T × a ≤⋁ᴸ T -- D(L) = L: every element lies in some D_k, the k being its rank. D-total : Type (α ⊔ˡ ρ) D-total = ∀ a → Σ[ k ∈ ℕ ] D k a
A join prime element below the join of a list lies below a member
(joinPrime-list), so it has no nontrivial join cover, which is
the book's definition of D₀; a nontrivial cover has no member above the
element (nontrivial-¬any).
-- Rule 4 along a list: a join prime element below a join of a list lies below a member. joinPrime-list : ∀ {a} → IsJoinPrime a → ∀ b bs → a ≤ ⋁⁺ 𝑳 b bs → Any (a ≤_) (b ∷ bs) joinPrime-list jp b [] p = here p joinPrime-list jp b (c ∷ cs) p = [ here , (λ q → there (joinPrime-list jp c cs q)) ]′ (jp p) -- A nontrivial cover has no member above the element. nontrivial-¬any : ∀ {a S} → Nontrivial a S → ¬ Any (a ≤_) S nontrivial-¬any nt any = let (s , s∈ , a≤s) = find any in All.lookup nt s∈ a≤s
The sets increase, and respect equality¶
D₀ ⊆ D₁ ⊆ ⋯: a join prime element has no nontrivial cover to refine, and a
refinement inside D_k is one inside D_{k+1} by induction
(D-mono); hence D_j ⊆ D_k for j ≤ k
(D-≤). Membership respects the equality of the lattice
(D-resp), since the covers of equal elements are the same.
-- D_k ⊆ D_{k+1}. D-mono : ∀ k {a} → D k a → D (suc k) a D-mono zero jp S (≤⋁⁺ {b} {bs} p) nt = ⊥-elim (nontrivial-¬any nt (joinPrime-list jp b bs p)) D-mono (suc k) d S cover nt = let (T , T≪S , allT , a≤T) = d S cover nt in T , T≪S , All.map (D-mono k) allT , a≤T -- D_j ⊆ D_k for j ≤ k. D-≤ : ∀ {j} k → j ≤ℕ k → ∀ {a} → D j a → D k a D-≤ zero j≤0 d = subst (λ i → D i _) (n≤0⇒n≡0 j≤0) d D-≤ (suc k) j≤sk d = [ (λ j<sk → D-mono k (D-≤ k (s≤s⁻¹ j<sk) d)) , (λ j≡sk → subst (λ i → D i _) j≡sk d) ]′ (m≤n⇒m<n∨m≡n j≤sk) -- Membership in D_k respects the equality of 𝑳. D-resp : ∀ k {a a'} → a ≈ a' → D k a → D k a' D-resp zero e jp p = ⊎-map (≤-respˡ-≈ e) (≤-respˡ-≈ e) (jp (≤-respˡ-≈ (sym e) p)) D-resp (suc k) e d S cover nt = let (T , T≪S , allT , a≤T) = d S (≤-≤⋁ 𝑳 (≤-reflexive e) cover) (All.map (λ ¬a'≤s a≤s → ¬a'≤s (≤-respˡ-≈ e a≤s)) nt) in T , T≪S , allT , ≤-≤⋁ 𝑳 (≤-reflexive (sym e)) a≤T
Closure under joins¶
The book's argument on p. 31: if a, b ∈ D_k and S is a nontrivial join
cover of a ∨ b, then S covers a, trivially or not. If trivially, the
one-element list {a} refines S inside D_k; if not, a ∈ D_{k+1} refines
S inside D_k. The same for b, and the two refinements together cover
a ∨ b. Which case holds is decided by the order, so a decision procedure for
it is a hypothesis.
module _ (_≤?_ : ∀ a b → Dec (a ≤ b)) where -- A cover of a ∈ D_k refines to one inside D_k: the refinement when it is nontrivial, -- the list {a} when it is trivial. refine-or-self : ∀ k {a S} → D k a → a ≤⋁ᴸ S → Σ[ U ∈ List L ] (U ≪ S) × All (D k) U × a ≤⋁ᴸ U refine-or-self k {a} {S} d cover with any? (a ≤?_) S ... | yes some = a ∷ [] , (some ∷ []) , (d ∷ []) , ≤⋁⁺ ≤-refl ... | no none = D-mono k d S cover (¬Any⇒All¬ S none) -- FJN p. 31: a join of two elements of D_k lies in D_{k+1}. D-∨ : ∀ k {a b} → D k a → D k b → D (suc k) (a ∨ b) D-∨ k da db S cover _ = let (U , U≪S , allU , a≤U) = refine-or-self k da (≤-≤⋁ 𝑳 ∨-upperˡ cover) (V , V≪S , allV , b≤V) = refine-or-self k db (≤-≤⋁ 𝑳 ∨-upperʳ cover) in U ++ V , ++⁺ U≪S V≪S , ++⁺ allU allV , ∨-≤⋁ 𝑳 (≤⋁-⊆ 𝑳 a≤U ∈-++⁺ˡ) (≤⋁-⊆ 𝑳 b≤V (∈-++⁺ʳ U))
Closure under meets, with (W)¶
In a lattice satisfying Whitman's condition, a meet a ∧ b below the join of
a list has a meetand below the join or lies below a member
(W-list, by induction on the list). So a nontrivial join
cover of a ∧ b is a nontrivial join cover of a or of b, and refines as
one of theirs does: each D_k is closed under meets (D-∧,
the book's remark on p. 33). For k = 0, (W) applied to a ∧ b ≤ c ∨ d puts
a or b below c ∨ d, hence below c or d by primality, or a ∧ b below
c or d outright.
module _ (W : SatisfiesW 𝑳) where -- (W) along a list: a meet below the join of a list. W-list : ∀ {a b} c cs → a ∧ b ≤ ⋁⁺ 𝑳 c cs → (a ≤⋁ᴸ (c ∷ cs) ⊎ b ≤⋁ᴸ (c ∷ cs)) ⊎ Any (a ∧ b ≤_) (c ∷ cs) W-list c [] p = inj₂ (here p) W-list {a} {b} c (d ∷ ds) p = [ (λ q → inj₁ (⊎-map ≤⋁⁺ ≤⋁⁺ q)) , [ (λ q → inj₂ (here q)) , (λ q → [ (λ r → inj₁ (⊎-map (λ s → ≤⋁-⊆ 𝑳 s there) (λ s → ≤⋁-⊆ 𝑳 s there) r)) , (λ r → inj₂ (there r)) ]′ (W-list d ds q)) ]′ ]′ (W a b c (⋁⁺ 𝑳 d ds) p) -- FJN p. 33: in a lattice with (W), each D_k is closed under meets. D-∧ : ∀ k {a b} → D k a → D k b → D k (a ∧ b) D-∧ zero {a} {b} jpa jpb {c} {d} p = [ [ (λ q → ⊎-map (≤-trans ∧-lowerˡ) (≤-trans ∧-lowerˡ) (jpa q)) , (λ q → ⊎-map (≤-trans ∧-lowerʳ) (≤-trans ∧-lowerʳ) (jpb q)) ]′ , id ]′ (W a b c d p) D-∧ (suc k) {a} {b} da db S (≤⋁⁺ {c} {cs} p) nt = [ [ from-a , from-b ]′ , (λ any → ⊥-elim (nontrivial-¬any nt any)) ]′ (W-list c cs p) where from-a : a ≤⋁ᴸ (c ∷ cs) → Σ[ T ∈ List L ] (T ≪ (c ∷ cs)) × All (D k) T × a ∧ b ≤⋁ᴸ T from-a a≤S = let (T , T≪S , allT , a≤T) = da (c ∷ cs) a≤S (All.map (λ ¬ab≤s a≤s → ¬ab≤s (≤-trans ∧-lowerˡ a≤s)) nt) in T , T≪S , allT , ≤-≤⋁ 𝑳 ∧-lowerˡ a≤T from-b : b ≤⋁ᴸ (c ∷ cs) → Σ[ T ∈ List L ] (T ≪ (c ∷ cs)) × All (D k) T × a ∧ b ≤⋁ᴸ T from-b b≤S = let (T , T≪S , allT , b≤T) = db (c ∷ cs) b≤S (All.map (λ ¬ab≤s b≤s → ¬ab≤s (≤-trans ∧-lowerʳ b≤s)) nt) in T , T≪S , allT , ≤-≤⋁ 𝑳 ∧-lowerʳ b≤T
Theorem 2.10 (1): a lattice with (W) generated by join prime elements¶
With the two closures, an induction on terms: in a lattice with (W) and a
decided order, every element of the sublattice generated by join prime elements
lies in some D_k (D-term), a meet of elements of D_i and
D_j in D_{i ⊔ j} and a join in D_{i ⊔ j + 1}. If the join prime elements
generate the lattice, D(L) = L (D-generated). The book's
Theorem 2.10 also gives the exact sets D_n(F) = X^{∧(∨∧)^n} and the minimal
join cover refinement property, neither of which is needed downstream.
module _ (W : SatisfiesW 𝑳) (_≤?_ : ∀ a b → Dec (a ≤ b)) {X : Type χ} (η : X → L) (prime : ∀ x → IsJoinPrime (η x)) where open Evaluation 𝑳 using ( ⟦_⟧ ) -- Theorem 2.10 (1): every element generated by join prime elements lies in some D_k. D-term : ∀ t → Σ[ k ∈ ℕ ] D k (⟦ t ⟧ η) D-term (ℊ x) = zero , prime x D-term (s ∧̇ t) = let (i , ds) = D-term s (j , dt) = D-term t in i ⊔ j , D-∧ W (i ⊔ j) {⟦ s ⟧ η} {⟦ t ⟧ η} (D-≤ {i} (i ⊔ j) (m≤m⊔n i j) ds) (D-≤ {j} (i ⊔ j) (m≤n⊔m i j) dt) D-term (s ∨̇ t) = let (i , ds) = D-term s (j , dt) = D-term t in suc (i ⊔ j) , D-∨ _≤?_ (i ⊔ j) {⟦ s ⟧ η} {⟦ t ⟧ η} (D-≤ {i} (i ⊔ j) (m≤m⊔n i j) ds) (D-≤ {j} (i ⊔ j) (m≤n⊔m i j) dt) -- If the join prime elements generate 𝑳, then D(L) = L. D-generated : (∀ a → Σ[ t ∈ LatTerm X ] ⟦ t ⟧ η ≈ a) → D-total D-generated gen a = let (t , e) = gen a (k , d) = D-term t in k , D-resp k e d
The dual sets, and (W) in the dual¶
The dual sets Dᵈ_k(L) are the sets D_k of the dual lattice, which has the
same carrier, and Dᵈ(L) = L is D(L) = L for the dual. Whitman's condition
is self-dual (SatisfiesW-dual): read in the dual, its
hypothesis s₁ ∧ s₂ ≤ t₁ ∨ t₂ is t₁ ∧ t₂ ≤ s₁ ∨ s₂ in 𝑳, and
its two pairs of alternatives exchange places. A decided order is decided in
the dual (≤ᵈ?).
-- The dual sets Dᵈ_k(L): the sets D_k of the dual lattice. Dᵈ : (𝑳 : Lattice α ρ) → ℕ → 𝕌[ proj₁ 𝑳 ] → Type (α ⊔ˡ ρ) Dᵈ 𝑳 = D (dualLattice 𝑳) -- Dᵈ(L) = L. Dᵈ-total : Lattice α ρ → Type (α ⊔ˡ ρ) Dᵈ-total 𝑳 = D-total (dualLattice 𝑳) module _ (𝑳 : Lattice α ρ) where open LatticeDual 𝑳 using ( ≤ᵈ-flip ; ≤ᵈ-unflip ) open Lattice-Order 𝑳 using ( _≤_ ) open Lattice-Order (dualLattice 𝑳) using () renaming ( _≤_ to _≤ᵈ_ ) -- Whitman's condition is self-dual. SatisfiesW-dual : SatisfiesW 𝑳 → SatisfiesW (dualLattice 𝑳) SatisfiesW-dual W s₁ s₂ t₁ t₂ p = [ (λ q → inj₂ (⊎-map ≤ᵈ-unflip ≤ᵈ-unflip q)) , (λ q → inj₁ (⊎-map ≤ᵈ-unflip ≤ᵈ-unflip q)) ]′ (W t₁ t₂ s₁ s₂ (≤ᵈ-flip p)) -- A decided order is decided in the dual. ≤ᵈ? : (∀ a b → Dec (a ≤ b)) → ∀ a b → Dec (a ≤ᵈ b) ≤ᵈ? _≤?_ a b = map′ ≤ᵈ-unflip ≤ᵈ-flip (b ≤? a)
Corollary 2.11: D(FL(X)) = FL(X), and its dual¶
The generators of FL(X) are join prime by rule 4 of Whitman's procedure and
meet prime by rule 5, FL(X) satisfies (W), and its order is decided when the
equality of X is. So Theorem 2.10 (1) applies to FL(X) and to its dual,
in which a term evaluates to its dual (⟦⟧ᵈ-dual).
module _ {X : Type χ} (_≟_ : DecidableEquality X) where open Decision _≟_ using ( _≤ʷ?_ ) open Lattice-Order (FL X) using ( _≤_ ) open LatticeDual (FL X) using ( ≤ᵈ-flip ; ≤ᵈ-unflip ) open Setoid 𝔻[ proj₁ (FL X) ] using ( reflexive ) open Evaluation (dualLattice (FL X)) using () renaming ( ⟦_⟧ to ⟦_⟧ᵈ ) private _≤?_ : ∀ s t → Dec (s ≤ t) s ≤? t = map′ ≤ʷ→≤ ≤→≤ʷ (s ≤ʷ? t) -- The generators are join prime (rule 4). FL-gen-prime : ∀ x → IsJoinPrime (FL X) (ℊ x) FL-gen-prime x p = ⊎-map ≤ʷ→≤ ≤ʷ→≤ (ℊ≤∨-inv (≤→≤ʷ p)) -- Corollary 2.11: D(FL(X)) = FL(X). FL-D-total : D-total (FL X) FL-D-total = D-generated (FL X) FL-satisfiesW _≤?_ ℊ FL-gen-prime λ t → t , reflexive (⟦⟧-ℊ t) -- The generators are meet prime (rule 5): join prime in the dual. FL-gen-primeᵈ : ∀ x → IsJoinPrime (dualLattice (FL X)) (ℊ x) FL-gen-primeᵈ x p = ⊎-map (λ q → ≤ᵈ-unflip (≤ʷ→≤ q)) (λ q → ≤ᵈ-unflip (≤ʷ→≤ q)) (∧≤ℊ-inv (≤→≤ʷ (≤ᵈ-flip p))) -- In the dual of FL(X), a term evaluates under the generic assignment to its dual. ⟦⟧ᵈ-dual : (t : LatTerm X) → ⟦ t ⟧ᵈ ℊ ≡ dual t ⟦⟧ᵈ-dual (ℊ x) = refl ⟦⟧ᵈ-dual (s ∧̇ t) = cong₂ _∨̇_ (⟦⟧ᵈ-dual s) (⟦⟧ᵈ-dual t) ⟦⟧ᵈ-dual (s ∨̇ t) = cong₂ _∧̇_ (⟦⟧ᵈ-dual s) (⟦⟧ᵈ-dual t) -- The dual of Corollary 2.11: Dᵈ(FL(X)) = FL(X). FL-Dᵈ-total : Dᵈ-total (FL X) FL-Dᵈ-total = D-generated (dualLattice (FL X)) (SatisfiesW-dual (FL X) FL-satisfiesW) (≤ᵈ? (FL X) _≤?_) ℊ FL-gen-primeᵈ λ u → dual u , reflexive (trans (⟦⟧ᵈ-dual (dual u)) (dual-involutive u))
The module checks in about a second of its own.