Added some additional proofs to Data.List.Any.Properties

CHANGELOG.md

@@ -323,6 +323,62 @@ Backwards compatible changes
   +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
   ```
 
+* Added functions to `Data.List`
+  ```agda
+  applyUpTo f n     ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
+  upTo n            ≈ 0      ∷ 1      ∷ ... ∷ n-1    ∷ []
+  applyDownFrom f n ≈ f[n-1] ∷ f[n-2] ∷ ... ∷ f[0]   ∷ []
+  tabulate f        ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
+  allFin n          ≈ 0f     ∷ 1f     ∷ ... ∷ n-1f   ∷ []
+  ```
+
+* Added proofs to `Data.List.Properties`
+  ```agda
+  map-cong₂      : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
+  foldr-++       : foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
+  foldl-++       : foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
+  foldr-∷ʳ       : foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
+  foldl-∷ʳ       : foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
+  reverse-foldr  : foldr f x (reverse ys) ≡ foldl (flip f) x ys
+  reverse-foldr  : foldl f x (reverse ys) ≡ foldr (flip f) x ys
+  length-reverse : length (reverse xs) ≡ length xs
+  ```
+
+* Added proofs to `Data.List.Any.Properties`
+  ```agda
+  lose∘find   : uncurry′ lose (proj₂ (find p)) ≡ p
+  find∘lose   : find (lose x∈xs pp) ≡ (x , x∈xs , pp)
+
+  ∃∈-Any      : (∃ λ x → x ∈ xs × P x) → Any P xs
+
+  Any-⊎⁺      : Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
+  Any-⊎⁻      : Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
+  Any-×⁺      : Any P xs × Any Q ys → Any (λ x → Any (λ y → P x × Q y) ys) xs
+  Any-×⁻      : Any (λ x → Any (λ y → P x × Q y) ys) xs → Any P xs × Any Q ys
+
+  map⁺        : Any (P ∘ f) xs → Any P (map f xs)
+  map⁻        : Any P (map f xs) → Any (P ∘ f) xs
+
+  ++⁺ˡ        : Any P xs → Any P (xs ++ ys)
+  ++⁺ʳ        : Any P ys → Any P (xs ++ ys)
+  ++⁻         : Any P (xs ++ ys) → Any P xs ⊎ Any P ys
+
+  concat⁺     : Any (Any P) xss → Any P (concat xss)
+  concat⁻     : Any P (concat xss) → Any (Any P) xss
+
+  applyUpTo⁺  : P (f i) → i < n → Any P (applyUpTo f n)
+  applyUpTo⁻  : Any P (applyUpTo f n) → ∃ λ i → i < n × P (f i)
+
+  tabulate⁺   : P (f i) → Any P (tabulate f)
+  tabulate⁻   : Any P (tabulate f) → ∃ λ i → P (f i)
+
+  map-with-∈⁺ : (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) → Any P (map-with-∈ xs f)
+  map-with-∈⁻ : Any P (map-with-∈ xs f) → ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
+
+  return⁺     : P x → Any P (return x)
+  return⁻     : Any P (return x) → P x
+  ```
+
 * Added proofs to `Data.Nat.Properties`:
   ```agda
   suc-injective        : suc m ≡ suc n → m ≡ n
@@ -416,45 +472,6 @@ Backwards compatible changes
   ∣-isPartialOrder : IsPartialOrder _≡_ _∣_
   ```
 
-* Added proofs to `Data.List.Properties`
-  ```agda
-  map-cong₂      : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
-  foldr-++       : foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys
-  foldl-++       : foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs
-  foldr-∷ʳ       : foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys
-  foldl-∷ʳ       : foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y
-  reverse-foldr  : foldr f x (reverse ys) ≡ foldl (flip f) x ys
-  reverse-foldr  : foldl f x (reverse ys) ≡ foldr (flip f) x ys
-  length-reverse : length (reverse xs) ≡ length xs
-  ```
-
-* Added functions to `Data.List`
-  ```agda
-  applyUpTo f n     ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
-  upTo n            ≈ 0      ∷ 1      ∷ ... ∷ n-1    ∷ []
-  applyDownFrom f n ≈ f[n-1] ∷ f[n-2] ∷ ... ∷ f[0]   ∷ []
-  tabulate f        ≈ f[0]   ∷ f[1]   ∷ ... ∷ f[n-1] ∷ []
-  allFin n          ≈ 0f     ∷ 1f     ∷ ... ∷ n-1f   ∷ []
-  ```
-
-* Added proofs to `Data.List.Any.Properties`
-  ```agda
-  lose∘find : uncurry′ lose (proj₂ (find p)) ≡ p
-  find∘lose : find (lose x∈xs pp) ≡ (x , x∈xs , pp)
-
-  ∃∈-Any    : (∃ λ x → x ∈ xs × P x) → Any P xs
-
-  ⊎→        : Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
-  ⊎←        : Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
-  ×→        : Any P xs × Any Q ys → Any (λ x → Any (λ y → P x × Q y) ys) xs
-  ×←        : Any (λ x → Any (λ y → P x × Q y) ys) xs → Any P xs × Any Q ys
-
-  map⁺      : Any (P ∘ f) xs → Any P (map f xs)
-  map⁻      : Any P (map f xs) → Any (P ∘ f) xs
-  map⁺∘map⁻ : map⁺ (map⁻ p) ≡ p
-  map⁻∘map⁺ : map⁻ (map⁺ p) ≡ p
-  ```
-
 * Added a functor encapsulating `map` in `Data.Vec`:
   ```agda
   functor = record { _<$>_ = map}