From 1eb69a9e60e3409432bd4fe1030ed4ecc8280350 Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 18 Apr 2018 17:56:16 -0300 Subject: [PATCH] further work on Collections --- src/Collections.lagda | 164 +++++++++++++++++++++++++++++ src/extra/Collections-setoid.lagda | 162 ++++++++++++++++++++++++++++ src/extra/ModuleInfix.agda | 19 ++++ 3 files changed, 345 insertions(+) create mode 100644 src/Collections.lagda create mode 100644 src/extra/Collections-setoid.lagda create mode 100644 src/extra/ModuleInfix.agda diff --git a/src/Collections.lagda b/src/Collections.lagda new file mode 100644 index 00000000..e40873fa --- /dev/null +++ b/src/Collections.lagda @@ -0,0 +1,164 @@ +--- +title : "Collections: Collections represented as Lists" +layout : page +permalink : /Collections +--- + +This chapter presents operations on collections and a number of +useful operations on them. + + +## Imports + +\begin{code} +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; _≢_; refl; sym; trans; cong) +open Eq.≡-Reasoning +open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) +-- open import Data.Nat.Properties using +-- (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ) +open import Relation.Nullary using (¬_) +open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Data.Empty using (⊥; ⊥-elim) +open import Isomorphism using (_≃_) +open import Function using (_∘_) +open import Level using (Level) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) +open import Data.List.All using (All; []; _∷_) +open import Data.List.Any using (Any; here; there) +open import Data.Maybe using (Maybe; just; nothing) +-- open import Data.List.Any.Membership.Propositional using (_∈_) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Nullary.Negation using (contraposition; ¬?) +open import Relation.Nullary.Product using (_×-dec_) +-- open import Relation.Binary using (IsEquivalence) +\end{code} + + +## Collections + +\begin{code} +infix 0 _↔_ + +_↔_ : Set → Set → Set +A ↔ B = (A → B) × (B → A) + +module Collection (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where + +-- abstract + + Coll : Set → Set + Coll A = List A + + [_] : A → Coll A + [ x ] = x ∷ [] + + infix 4 _∈_ + infix 4 _⊆_ + infixl 5 _∪_ + infixl 5 _\\_ + + data _∈_ : A → Coll A → Set where + + here : ∀ {x xs} → + ---------- + x ∈ x ∷ xs + + there : ∀ {w x xs} → + w ∈ xs → + ---------- + w ∈ x ∷ xs + + _⊆_ : Coll A → Coll A → Set + xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys + + _∪_ : Coll A → Coll A → Coll A + _∪_ = _++_ + + _\\_ : Coll A → A → Coll A + xs \\ x = filter (¬? ∘ (_≟ x)) xs + + lemma₅ : ∀ {w x xs} → w ∈ xs → w ≢ x → w ∈ xs \\ x + lemma₅ {w} {x} here w≢ with w ≟ x + ... | yes refl = ⊥-elim (w≢ refl) + ... | no _ = here + lemma₅ {_} {x} {y ∷ _} (there w∈) w≢ with y ≟ x + ... | yes refl = lemma₅ w∈ w≢ + ... | no _ = there (lemma₅ w∈ w≢) + + lemma₆ : ∀ {x : A} {xs ys : Coll A} → xs \\ x ⊆ ys ↔ xs ⊆ x ∷ ys + lemma₆ = ⟨ forward , backward ⟩ + where + + forward : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys + forward {x} ⊆ys {w} w∈ with w ≟ x + ... | yes refl = here + ... | no w≢ = there (⊆ys (lemma₅ w∈ w≢)) + + backward = {!!} + + + ⊆-refl : ∀ {xs} → xs ⊆ xs + ⊆-refl ∈xs = ∈xs + + ⊆-trans : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs + ⊆-trans xs⊆ ys⊆ = ys⊆ ∘ xs⊆ + + lemma₁ : ∀ {w xs} → w ∈ xs ↔ [ w ] ⊆ xs + lemma₁ = ⟨ forward , backward ⟩ + where + + forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs + forward ∈xs here = ∈xs + forward ∈xs (there ()) + + backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs + backward ⊆xs = ⊆xs here + + lemma₂ : ∀ {xs ys} → xs ⊆ xs ∪ ys + lemma₂ here = here + lemma₂ (there ∈xs) = there (lemma₂ ∈xs) + + lemma₃ : ∀ {xs ys} → ys ⊆ xs ∪ ys + lemma₃ {[]} ∈ys = ∈ys + lemma₃ {x ∷ xs} ∈ys = there (lemma₃ {xs} ∈ys) + + lemma₄ : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys ↔ w ∈ xs ∪ ys + lemma₄ = ⟨ forward , backward ⟩ + where + + forward : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys → w ∈ xs ∪ ys + forward (inj₁ ∈xs) = lemma₂ ∈xs + forward (inj₂ ∈ys) = lemma₃ ∈ys + + backward : ∀ {xs ys w} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys + backward {[]} ∈ys = inj₂ ∈ys + backward {x ∷ xs} here = inj₁ here + backward {x ∷ xs} (there w∈) with backward {xs} w∈ + ... | inj₁ ∈xs = inj₁ (there ∈xs) + ... | inj₂ ∈ys = inj₂ ∈ys + + +\end{code} + + +## Standard Library + +Definitions similar to those in this chapter can be found in the standard library. +\begin{code} +-- EDIT +\end{code} +The standard library version of `IsMonoid` differs from the +one given here, in that it is also parameterised on an equivalence relation. + + +## Unicode + +This chapter uses the following unicode. + + EDIT + ∷ U+2237 PROPORTION (\::) + ⊗ U+2297 CIRCLED TIMES (\otimes) + ∈ U+2208 ELEMENT OF (\in) + ∉ U+2209 NOT AN ELEMENT OF (\inn) diff --git a/src/extra/Collections-setoid.lagda b/src/extra/Collections-setoid.lagda new file mode 100644 index 00000000..0a58366a --- /dev/null +++ b/src/extra/Collections-setoid.lagda @@ -0,0 +1,162 @@ +--- +title : "Collections: Collections represented as Lists" +layout : page +permalink : /Collections +--- + +This chapter presents operations on collections and a number of +useful operations on them. + + +## Imports + +\begin{code} +-- import Relation.Binary.PropositionalEquality as Eq +-- open Eq using (_≡_; refl; sym; trans; cong) +-- open Eq.≡-Reasoning +open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) +-- open import Data.Nat.Properties using +-- (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ) +open import Relation.Nullary using (¬_) +open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Isomorphism using (_≃_) +open import Function using (_∘_) +open import Level using (Level) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) +open import Data.List.All using (All; []; _∷_) +open import Data.List.Any using (Any; here; there) +open import Data.Maybe using (Maybe; just; nothing) +-- open import Data.List.Any.Membership.Propositional using (_∈_) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Nullary.Negation using (contraposition; ¬?) +open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Binary using (IsEquivalence) +\end{code} + + +## Collections + +\begin{code} +infix 0 _↔_ + +_↔_ : Set → Set → Set +A ↔ B = (A → B) × (B → A) + +module Collection + (A : Set) + (_≈_ : A → A → Set) + (isEquivalence : IsEquivalence _≈_) + where + + open IsEquivalence isEquivalence + + abstract + + Coll : Set → Set + Coll A = List A +\end{code} + +Collections support the same abbreviations as lists for writing +collections with a small number of elements. +\begin{code} + [_] : A → Coll A + [ x ] = x ∷ [] +\end{code} + +\begin{code} + infix 4 _∈_ + infix 4 _⊆_ + infix 5 _∪_ + + _∈_ : A → Coll A → Set + w ∈ xs = Any (w ≈_) xs + + _⊆_ : Coll A → Coll A → Set + xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys + + _∪_ : Coll A → Coll A → Coll A + _∪_ = _++_ + + preserves : ∀ {u v xs} → u ≈ v → u ∈ xs → v ∈ xs + preserves u≈v (here u≈) = here (trans (sym u≈v) u≈) + preserves u≈v (there u∈) = there (preserves u≈v u∈) + + ⊆-refl : ∀ {xs} → xs ⊆ xs + ⊆-refl ∈xs = ∈xs + + ⊆-trans : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs + ⊆-trans xs⊆ ys⊆ = ys⊆ ∘ xs⊆ + + lemma₁ : ∀ {w xs} → w ∈ xs ↔ [ w ] ⊆ xs + lemma₁ = ⟨ forward , backward ⟩ + where + + forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs + forward ∈xs (here w≈) = preserves (sym w≈) ∈xs -- ∈xs + forward ∈xs (there ()) + + backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs + backward ⊆xs = ⊆xs (here refl) + + lemma₂ : ∀ {xs ys} → xs ⊆ xs ∪ ys + lemma₂ (here w≈) = here w≈ + lemma₂ (there ∈xs) = there (lemma₂ ∈xs) + + lemma₃ : ∀ {xs ys} → ys ⊆ xs ∪ ys + lemma₃ {[]} ∈ys = ∈ys + lemma₃ {x ∷ xs} ∈ys = there (lemma₃ {xs} ∈ys) + + lemma₄ : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys ↔ w ∈ xs ∪ ys + lemma₄ = ⟨ forward , backward ⟩ + where + + forward : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys → w ∈ xs ∪ ys + forward (inj₁ ∈xs) = lemma₂ ∈xs + forward (inj₂ ∈ys) = lemma₃ ∈ys + + backward : ∀ {xs ys w} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys + backward {[]} ∈ys = inj₂ ∈ys + backward {x ∷ xs} (here w≈) = inj₁ (here w≈) + backward {x ∷ xs} (there w∈) with backward {xs} w∈ + ... | inj₁ ∈xs = inj₁ (there ∈xs) + ... | inj₂ ∈ys = inj₂ ∈ys + + +\end{code} + +# Operations with decidable equivalence + +\begin{code} + module DecCollection (_≟_ : ∀ (x y : A) → Dec (x ≈ y)) where + + abstract + + infix 5 _\\_ + + _\\_ : Coll A → A → Coll A + xs \\ x = filter (¬? ∘ (x ≟_)) xs + + +\end{code} + + +## Standard Library + +Definitions similar to those in this chapter can be found in the standard library. +\begin{code} +-- EDIT +\end{code} +The standard library version of `IsMonoid` differs from the +one given here, in that it is also parameterised on an equivalence relation. + + +## Unicode + +This chapter uses the following unicode. + + EDIT + ∷ U+2237 PROPORTION (\::) + ⊗ U+2297 CIRCLED TIMES (\otimes) + ∈ U+2208 ELEMENT OF (\in) + ∉ U+2209 NOT AN ELEMENT OF (\inn) diff --git a/src/extra/ModuleInfix.agda b/src/extra/ModuleInfix.agda new file mode 100644 index 00000000..0ea6ffe5 --- /dev/null +++ b/src/extra/ModuleInfix.agda @@ -0,0 +1,19 @@ +module ModuleInfix where + +open import Data.List using (List; _∷_; []) +open import Data.Bool using (Bool; true; false) + +module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where + + infix 1 _≤_ + infix 2 _⊝_ + + insert : A → List A → List A + insert x [] = x ∷ [] + insert x (y ∷ ys) with zero ≤ (y ⊝ x) + insert x (y ∷ ys) | true = x ∷ y ∷ ys + insert x (y ∷ ys) | false = y ∷ insert x ys + + sort : List A → List A + sort [] = [] + sort (x ∷ xs) = insert x (sort xs)