Skip to content

Commit d462216

Browse files
committed
Lists: incorporate feedback from James
1 parent e614c2a commit d462216

File tree

10 files changed

+59
-66
lines changed

10 files changed

+59
-66
lines changed

CHANGELOG.md

Lines changed: 16 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -123,11 +123,6 @@ Additions to existing modules
123123
Env = Vec Carrier
124124
```
125125

126-
* In `Data.List.Base`:
127-
```agda
128-
lookupMaybe : List A → ℕ → Maybe A
129-
```
130-
131126
* In `Data.List.Membership.Setoid.Properties`:
132127
```agda
133128
Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys
@@ -181,14 +176,12 @@ Additions to existing modules
181176

182177
* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
183178
```agda
184-
Unique-dropSnd : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
185-
Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
179+
Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
186180
```
187181

188182
* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
189183
```agda
190-
Unique-dropSnd : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
191-
Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
184+
Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
192185
```
193186

194187
* In `Data.List.Relation.Binary.Equality.Setoid`:
@@ -203,6 +196,20 @@ Additions to existing modules
203196
++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
204197
```
205198

199+
* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
200+
```agda
201+
⊈[] : x ∷ xs ⊈ []
202+
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
203+
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
204+
```
205+
206+
* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
207+
```agda
208+
⊈[] : x ∷ xs ⊈ []
209+
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
210+
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
211+
```
212+
206213
* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
207214
```agda
208215
concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
@@ -230,20 +237,6 @@ Additions to existing modules
230237
∈-dedup : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
231238
```
232239

233-
* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
234-
```agda
235-
⊈[] : x ∷ xs ⊈ []
236-
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
237-
∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
238-
```
239-
240-
* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
241-
```agda
242-
⊈[] : x ∷ xs ⊈ []
243-
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
244-
∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
245-
```
246-
247240
* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
248241
```agda
249242
dedup-++-↭ : Disjoint xs ys →

src/Data/List/Base.agda

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -229,12 +229,6 @@ lookup : ∀ (xs : List A) → Fin (length xs) → A
229229
lookup (x ∷ xs) zero = x
230230
lookup (x ∷ xs) (suc i) = lookup xs i
231231

232-
lookupMaybe : List A Maybe A
233-
lookupMaybe = λ where
234-
[] _ nothing
235-
(x ∷ _) zero just x
236-
(_ ∷ xs) (suc n) lookupMaybe xs n
237-
238232
-- Numerical
239233

240234
upTo : List ℕ

src/Data/List/Membership/Propositional/Properties.agda

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module Data.List.Membership.Propositional.Properties where
1010

1111
open import Algebra.Core using (Op₂)
1212
open import Algebra.Definitions using (Selective)
13-
open import Data.Empty using (⊥-elim)
1413
open import Data.Fin.Base using (Fin)
1514
open import Data.List.Base as List
1615
open import Data.List.Effectful using (monad)
@@ -41,7 +40,7 @@ open import Level using (Level)
4140
open import Relation.Binary.Core using (Rel)
4241
open import Relation.Binary.Definitions as Binary hiding (Decidable)
4342
open import Relation.Binary.PropositionalEquality.Core as ≡
44-
using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_; subst)
43+
using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
4544
open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
4645
import Relation.Binary.Properties.DecTotalOrder as DTOProperties
4746
open import Relation.Nullary.Decidable.Core
@@ -460,10 +459,10 @@ map∷-decomp∈ {xss = _ ∷ _} = λ where
460459

461460
map∷-decomp : xs ∈ map (y ∷_) xss ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
462461
map∷-decomp {xss = _ ∷ _} (here refl) = -, here refl , refl
463-
map∷-decomp {xs = []} {xss = _ ∷ _} (there xs∈) = ⊥-elim ([]∉map∷ xs∈)
462+
map∷-decomp {xs = []} {xss = _ ∷ _} (there xs∈) = contradiction xs∈ []∉map∷
464463
map∷-decomp {xs = x ∷ xs} {xss = _ ∷ _} (there xs∈) =
465464
let eq , p = map∷-decomp∈ xs∈
466-
in -, there p , subst (λ∷ _ ≡ _) eq refl
465+
in -, there p , cong (_∷ _) (sym eq)
467466

468467
∈-map∷⁻ : xs ∈ map (x ∷_) xss x ∈ xs
469468
∈-map∷⁻ {xss = _ ∷ _} = λ where

src/Data/List/Membership/Setoid/Properties.agda

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -393,7 +393,7 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
393393

394394
module _
395395
(S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
396-
{P : Pred (S₁ .Carrier) p} (P? : Decidable P) (resp : P Respects (S₁ .Setoid._≈_))
396+
{P : Pred _ p} (P? : Decidable P) (resp : P Respects _)
397397
{f xs y} where
398398

399399
open Setoid S₁ renaming (_≈_ to _≈₁_)
@@ -513,4 +513,3 @@ module _ (S : Setoid c ℓ) where
513513

514514
All-∉-swap : {xs ys} All (_∉ ys) xs All (_∉ xs) ys
515515
All-∉-swap p = All.¬Any⇒All¬ _ ((All.All¬⇒¬Any p) ∘ Any-∈-swap)
516-

src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation using (¬_)
2626

2727
module _ {c ℓ} (S : Setoid c ℓ) where
2828

29-
open Setoid S using (__; reflexive) renaming (Carrier to A)
29+
open Setoid S using (__; reflexive) renaming (Carrier to A)
3030

3131
------------------------------------------------------------------------
3232
-- Relational properties
@@ -40,7 +40,7 @@ module _ {c ℓ} (S : Setoid c ℓ) where
4040
------------------------------------------------------------------------
4141

4242
Disjoint⇒AllAll : {xs ys} Disjoint S xs ys
43-
All (λ x All (λ y ¬ x ≈ y) ys) xs
43+
All (λ x All (x ≉_) ys) xs
4444
Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
4545
(All.tabulate (λ v∈xs v∈ys xs#ys (Any.map reflexive v∈xs , v∈ys)))
4646

src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions using (DecidableEquality)
3333
------------------------------------------------------------------------
3434
-- deduplicate
3535

36-
module _ {a}{A : Set a} (_≟_ : DecidableEquality A) where
36+
module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
3737

3838
private
3939
dedup≡ = deduplicate _≟_

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional
2828
import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
2929
open import Data.Nat.Base using (ℕ; _≤_)
3030
import Data.Product.Base as Product
31-
import Data.Sum.Base as Sum
31+
open import Data.Sum.Base as Sum using (_⊎_)
3232
open import Effect.Monad
3333
open import Function.Base using (_∘_; _∘′_; id; _$_)
3434
open import Function.Bundles using (_↔_; Inverse; Equivalence)
@@ -62,6 +62,9 @@ private
6262
⊈[] : x ∷ xs ⊈ []
6363
⊈[] = Subset.⊈[] (setoid _)
6464

65+
⊆[]⇒≡[] : {A : Set a} (_⊆ []) ⋐ (_≡ [])
66+
⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A)
67+
6568
------------------------------------------------------------------------
6669
-- Relational properties with _≋_ (pointwise equality)
6770
------------------------------------------------------------------------
@@ -158,12 +161,12 @@ xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _)
158161
∈-∷⁺ʳ : {x} x ∈ ys xs ⊆ ys x ∷ xs ⊆ ys
159162
∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _)
160163

164+
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys y ∈ xs ⊎ xs ⊆ ys
165+
⊆∷⇒∈∨⊆ = Subset.⊆∷⇒∈∨⊆ (setoid _)
166+
161167
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys y ∉ xs xs ⊆ ys
162168
⊆∷∧∉⇒⊆ = Subset.⊆∷∧∉⇒⊆ (setoid _)
163169

164-
∈∷∧⊆⇒∈ : x ∈ y ∷ xs xs ⊆ ys x ∈ y ∷ ys
165-
∈∷∧⊆⇒∈ = Subset.∈∷∧⊆⇒∈ (setoid _)
166-
167170
------------------------------------------------------------------------
168171
-- _++_
169172

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
module Data.List.Relation.Binary.Subset.Setoid.Properties where
1010

1111
open import Data.Bool.Base using (Bool; true; false)
12-
open import Data.Empty using (⊥-elim)
1312
open import Data.List.Base hiding (_∷ʳ_; find)
1413
import Data.List.Properties as List
1514
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
@@ -23,6 +22,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
2322
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
2423
import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ
2524
open import Data.Product.Base using (_,_)
25+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
2626
open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
2727
open import Level using (Level)
2828
open import Relation.Nullary using (¬_; does; yes; no)
@@ -35,6 +35,7 @@ open import Relation.Binary.Bundles using (Setoid; Preorder)
3535
open import Relation.Binary.Structures using (IsPreorder)
3636
import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
3737
open import Relation.Binary.Reasoning.Syntax
38+
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
3839

3940
open Setoid using (Carrier)
4041

@@ -54,6 +55,10 @@ module _ (S : Setoid a ℓ) where
5455
⊈[] : {x xs} x ∷ xs ⊈ []
5556
⊈[] p = Membershipₚ.∉[] S $ p (here refl)
5657

58+
⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
59+
⊆[]⇒≡[] {x = []} _ = ≡.refl
60+
⊆[]⇒≡[] {x = _ ∷ _} p with () ⊈[] p
61+
5762
------------------------------------------------------------------------
5863
-- Relational properties with _≋_ (pointwise equality)
5964
------------------------------------------------------------------------
@@ -201,15 +206,18 @@ module _ (S : Setoid a ℓ) where
201206
∈-∷⁺ʳ x∈ys _ (here v≈x) = ∈-resp-≈ S (sym v≈x) x∈ys
202207
∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
203208

209+
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys y ∈ xs ⊎ xs ⊆ ys
210+
⊆∷⇒∈∨⊆ {xs = []} []⊆y∷ys = inj₂ λ ()
211+
⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there
212+
... | inj₁ y∈xs = inj₁ $ there y∈xs
213+
... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl)
214+
... | here x≈y = inj₁ $ here (sym x≈y)
215+
... | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys)
216+
204217
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys y ∉ xs xs ⊆ ys
205-
⊆∷∧∉⇒⊆ xs⊆ y∉ x∈ = case xs⊆ x∈ of λ where
206-
(here x≈) ⊥-elim $ y∉ (∈-resp-≈ S x≈ x∈)
207-
(there p) p
208-
209-
∈∷∧⊆⇒∈ : x ∈ y ∷ xs xs ⊆ ys x ∈ y ∷ ys
210-
∈∷∧⊆⇒∈ = λ where
211-
(here x≡y) _ here x≡y
212-
(there x∈) xs⊆ there $ xs⊆ x∈
218+
⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys
219+
... | inj₁ y∈xs = contradiction y∈xs y∉xs
220+
... | inj₂ xs⊆ys = xs⊆ys
213221

214222
------------------------------------------------------------------------
215223
-- ++

src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -164,8 +164,5 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where
164164
------------------------------------------------------------------------
165165
-- ∷
166166

167-
Unique-dropSnd : Unique (x ∷ y ∷ xs) Unique (x ∷ xs)
168-
Unique-dropSnd = Setoid.Unique-dropSnd (setoid _)
169-
170-
Unique∷⇒head∉tail : Unique (x ∷ xs) x ∉ xs
171-
Unique∷⇒head∉tail = Setoid.Unique∷⇒head∉tail (setoid _)
167+
Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) x ∉ xs
168+
Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _)

src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Data.List.Relation.Binary.Disjoint.Setoid.Properties
1616
open import Data.List.Relation.Unary.Any using (here; there)
1717
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
1818
open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
19-
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; _∷_)
19+
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
2020
open import Data.List.Relation.Unary.Unique.Setoid
2121
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
2222
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
@@ -165,14 +165,14 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
165165
module _ (S : Setoid a ℓ) where
166166

167167
open Setoid S renaming (Carrier to A)
168-
open Membership S using (_∈_; _∉_)
168+
open Membership S using (_∉_)
169169

170-
private variable x y : A; xs : List A
170+
private
171+
variable
172+
x y : A
173+
xs : List A
171174

172-
Unique-dropSnd : Unique S (x ∷ y ∷ xs) Unique S (x ∷ xs)
173-
Unique-dropSnd ((_ ∷ x∉) ∷ uniq) = x∉ AllPairs.∷ drop⁺ S 1 uniq
174-
175-
Unique∷⇒head∉tail : Unique S (x ∷ xs) x ∉ xs
176-
Unique∷⇒head∉tail uniq@((x∉ ∷ _) ∷ _) = λ where
177-
(here x≈) x∉ x≈
178-
(there x∈) Unique∷⇒head∉tail (Unique-dropSnd uniq) x∈
175+
Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) x ∉ xs
176+
Unique[x∷xs]⇒x∉xs ((x≉ ∷ x∉) ∷ _ ∷ uniq) = λ where
177+
(here x≈) x≉ x≈
178+
(there x∈) Unique[x∷xs]⇒x∉xs (x∉ AllPairs.∷ uniq) x∈

0 commit comments

Comments
 (0)