From 9a5ec9fc4b51dc4514f5f15db7fc72c90422f13e Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sun, 8 Sep 2024 15:23:24 +0100
Subject: [PATCH] Add two lemmas to `Data.List.Membership.Setoid.Properties` 
 (#2465)

* fixes first part of issue #2463; second part creates dependency cycle

* refactor to break dependency cycle

* renamed in line with review suggestions

* fix  bug
---
 CHANGELOG.md                                  | 11 +++
 .../List/Membership/Setoid/Properties.agda    | 16 ++++
 .../List/Relation/Unary/All/Properties.agda   | 65 +------------
 .../Relation/Unary/All/Properties/Core.agda   | 96 +++++++++++++++++++
 4 files changed, 128 insertions(+), 60 deletions(-)
 create mode 100644 src/Data/List/Relation/Unary/All/Properties/Core.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8125735a2b..62f9b4b8e5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -93,6 +93,11 @@ New modules
 
   NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.
 
+* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  Data.List.Relation.Unary.All.Properties.Core
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -113,6 +118,12 @@ Additions to existing modules
   Env = Vec Carrier
  ```
 
+* In `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  Any-∈-swap :  Any (_∈ ys) xs → Any (_∈ xs) ys
+  All-∉-swap :  All (_∉ ys) xs → All (_∉ xs) ys
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   product≢0 : All NonZero ns → NonZero (product ns)
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 48303dec37..76bbd8beaf 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -17,6 +17,7 @@ import Data.List.Membership.Setoid as Membership
 import Data.List.Relation.Binary.Equality.Setoid as Equality
 open import Data.List.Relation.Unary.All as All using (All)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+import Data.List.Relation.Unary.All.Properties.Core as All
 import Data.List.Relation.Unary.Any.Properties as Any
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z<s; _<_)
@@ -446,3 +447,18 @@ module _ (S : Setoid c ℓ) where
   ∈-∷=⁻ (here x≈z)   y≉v (there y∈) = there y∈
   ∈-∷=⁻ (there x∈xs) y≉v (here y≈z) = here y≈z
   ∈-∷=⁻ (there x∈xs) y≉v (there y∈) = there (∈-∷=⁻ x∈xs y≉v y∈)
+
+------------------------------------------------------------------------
+-- Any/All symmetry wrt _∈_/_∉_
+
+module _ (S : Setoid c ℓ) where
+
+  open Setoid S using (sym)
+  open Membership S
+
+  Any-∈-swap :  ∀ {xs ys} → Any (_∈ ys) xs → Any (_∈ xs) ys
+  Any-∈-swap = Any.swap ∘ Any.map (Any.map sym)
+
+  All-∉-swap :  ∀ {xs ys} → All (_∉ ys) xs → All (_∉ xs) ys
+  All-∉-swap p = All.¬Any⇒All¬ _ ((All.All¬⇒¬Any p) ∘ Any-∈-swap)
+
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 9e3c4968c8..b466f93054 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -61,6 +61,11 @@ private
     x y : A
     xs ys : List A
 
+------------------------------------------------------------------------
+-- Re-export Core Properties
+
+open import Data.List.Relation.Unary.All.Properties.Core public
+
 ------------------------------------------------------------------------
 -- Properties regarding Null
 
@@ -85,66 +90,6 @@ null⇒Null {xs = _ ∷ _} ()
 
 -- See also Data.List.Relation.Unary.All.Properties.WithK.[]=-irrelevant.
 
-------------------------------------------------------------------------
--- Lemmas relating Any, All and negation.
-
-¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
-¬Any⇒All¬ []       ¬p = []
-¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there)
-
-All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
-All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
-All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p
-
-¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
-¬All⇒Any¬ dec []       ¬∀ = contradiction [] ¬∀
-¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
-... |  true because  [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p])))
-... | false because [¬p] = here (invert [¬p])
-
-Any¬⇒¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs
-Any¬⇒¬All (here  ¬p) = ¬p           ∘ All.head
-Any¬⇒¬All (there ¬p) = Any¬⇒¬All ¬p ∘ All.tail
-
-¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs
-¬Any↠All¬ = mk↠ₛ {to = ¬Any⇒All¬ _} (λ y → All¬⇒¬Any y , to∘from y)
-  where
-  to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p
-  to∘from []         = refl
-  to∘from (¬p ∷ ¬ps) = cong₂ _∷_ refl (to∘from ¬ps)
-
-  -- If equality of functions were extensional, then the surjection
-  -- could be strengthened to a bijection.
-
-  from∘to : Extensionality _ _ →
-            ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p
-  from∘to ext []       ¬p = ext λ ()
-  from∘to ext (x ∷ xs) ¬p = ext λ
-    { (here p)  → refl
-    ; (there p) → cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
-    }
-
-Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
-Any¬⇔¬All dec = mk⇔ Any¬⇒¬All (¬All⇒Any¬ dec _)
-
-private
-  -- If equality of functions were extensional, then the logical
-  -- equivalence could be strengthened to a surjection.
-  to∘from : Extensionality _ _ → (dec : Decidable P) →
-            (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
-  to∘from ext P ¬∀ = ext λ ∀P → contradiction ∀P ¬∀
-
-module _ {_~_ : REL A B ℓ} where
-
-  All-swap : ∀ {xs ys} →
-             All (λ x → All (x ~_) ys) xs →
-             All (λ y → All (_~ y) xs) ys
-  All-swap {ys = []}     _   = []
-  All-swap {ys = y ∷ ys} []  = All.universal (λ _ → []) (y ∷ ys)
-  All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) =
-    (x~y ∷ (All.map All.head pxs)) ∷
-    All-swap (x~ys ∷ (All.map All.tail pxs))
-
 ------------------------------------------------------------------------
 -- Defining properties of lookup and _[_]=_
 --
diff --git a/src/Data/List/Relation/Unary/All/Properties/Core.agda b/src/Data/List/Relation/Unary/All/Properties/Core.agda
new file mode 100644
index 0000000000..758ede3110
--- /dev/null
+++ b/src/Data/List/Relation/Unary/All/Properties/Core.agda
@@ -0,0 +1,96 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties related to All
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Unary.All.Properties.Core where
+
+open import Axiom.Extensionality.Propositional using (Extensionality)
+open import Data.Bool.Base using (true; false)
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.Product.Base as Product using (_,_)
+open import Function.Base using (_∘_; _$_)
+open import Function.Bundles using (_↠_; mk↠ₛ; _⇔_; mk⇔)
+open import Level using (Level)
+open import Relation.Binary.Core using (REL)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Decidable.Core using (_because_)
+open import Relation.Unary using (Decidable; Pred; Universal)
+
+private
+  variable
+    a b p ℓ : Level
+    A : Set a
+    B : Set b
+    P : Pred A p
+    x y : A
+    xs ys : List A
+
+------------------------------------------------------------------------
+-- Lemmas relating Any, All and negation.
+
+¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
+¬Any⇒All¬ []       ¬p = []
+¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there)
+
+All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
+All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
+All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p
+
+¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
+¬All⇒Any¬ dec []       ¬∀ = contradiction [] ¬∀
+¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
+... |  true because  [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p])))
+... | false because [¬p] = here (invert [¬p])
+
+Any¬⇒¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs
+Any¬⇒¬All (here  ¬p) = ¬p           ∘ All.head
+Any¬⇒¬All (there ¬p) = Any¬⇒¬All ¬p ∘ All.tail
+
+¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs
+¬Any↠All¬ = mk↠ₛ {to = ¬Any⇒All¬ _} (λ y → All¬⇒¬Any y , to∘from y)
+  where
+  to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p
+  to∘from []         = refl
+  to∘from (¬p ∷ ¬ps) = cong₂ _∷_ refl (to∘from ¬ps)
+
+  -- If equality of functions were extensional, then the surjection
+  -- could be strengthened to a bijection.
+
+  from∘to : Extensionality _ _ →
+            ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p
+  from∘to ext []       ¬p = ext λ ()
+  from∘to ext (x ∷ xs) ¬p = ext λ
+    { (here p)  → refl
+    ; (there p) → cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
+    }
+
+Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
+Any¬⇔¬All dec = mk⇔ Any¬⇒¬All (¬All⇒Any¬ dec _)
+
+private
+  -- If equality of functions were extensional, then the logical
+  -- equivalence could be strengthened to a surjection.
+  to∘from : Extensionality _ _ → (dec : Decidable P) →
+            (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
+  to∘from ext P ¬∀ = ext λ ∀P → contradiction ∀P ¬∀
+
+module _ {_~_ : REL A B ℓ} where
+
+  All-swap : ∀ {xs ys} →
+             All (λ x → All (x ~_) ys) xs →
+             All (λ y → All (_~ y) xs) ys
+  All-swap {ys = []}     _   = []
+  All-swap {ys = y ∷ ys} []  = All.universal (λ _ → []) (y ∷ ys)
+  All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) =
+    (x~y ∷ (All.map All.head pxs)) ∷
+    All-swap (x~ys ∷ (All.map All.tail pxs))
+