refactor: Any.Propertiess

Author: jamesmckinna

src/Data/List/Fresh/Relation/Unary/Any/Properties.agda

@@ -19,7 +19,7 @@ open import Function.Base using (_∘′_)
 open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary.Decidable.Core
-open import Relation.Unary  as U using (Pred)
+open import Relation.Unary as Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nary using (∀[_]; _⇒_; ∁; Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
@@ -30,37 +30,40 @@ private
     a b p q r s : Level
     A : Set a
     B : Set b
+    P : Pred A p
+    Q : Pred A q
+    R : Rel A r
+    xs ys : List# A R
+
 
 ------------------------------------------------------------------------
 -- NonEmpty
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  Any⇒NonEmpty : {xs : List# A R} → Any P xs → NonEmpty xs
-  Any⇒NonEmpty {xs = cons x xs pr} p  = cons x xs pr
+Any⇒NonEmpty : Any P xs → NonEmpty xs
+Any⇒NonEmpty {xs = cons x xs pr} p  = cons x xs pr
 
 ------------------------------------------------------------------------
 -- Correspondence between Any and All
 
-module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P⇒¬Q : ∀[ P ⇒ ∁ Q ]) where
+module _ (P⇒¬Q : ∀[ P ⇒ ∁ Q ]) where
 
-  Any⇒¬All : {xs : List# A R} → Any P xs → ¬ (All Q xs)
+  Any⇒¬All : Any P xs → ¬ (All Q xs)
   Any⇒¬All (here p)   (q ∷ _)  = P⇒¬Q p q
   Any⇒¬All (there ps) (_ ∷ qs) = Any⇒¬All ps qs
 
-  All⇒¬Any : {xs : List# A R} → All P xs → ¬ (Any Q xs)
+  All⇒¬Any : All P xs → ¬ (Any Q xs)
   All⇒¬Any (p ∷ _)  (here q)   = P⇒¬Q p q
   All⇒¬Any (_ ∷ ps) (there qs) = All⇒¬Any ps qs
 
-module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
+module _ (P? : Decidable P) where
 
-  ¬All⇒Any : {xs : List# A R} → ¬ (All P xs) → Any (∁ P) xs
+  ¬All⇒Any : ¬ (All P xs) → Any (∁ P) xs
   ¬All⇒Any {xs = []}      ¬ps = contradiction [] ¬ps
   ¬All⇒Any {xs = x ∷# xs} ¬ps with P? x
   ... |  true because  [p] = there (¬All⇒Any (¬ps ∘′ (invert [p] ∷_)))
   ... | false because [¬p] = here (invert [¬p])
 
-  ¬Any⇒All : {xs : List# A R} → ¬ (Any P xs) → All (∁ P) xs
+  ¬Any⇒All : ¬ (Any P xs) → All (∁ P) xs
   ¬Any⇒All {xs = []}      ¬ps = []
   ¬Any⇒All {xs = x ∷# xs} ¬ps with P? x
   ... |  true because  [p] = contradiction (here (invert [p])) ¬ps
@@ -69,30 +72,23 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- remove
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  length-remove : {xs : List# A R} (k : Any P xs) →
-    length xs ≡ suc (length (xs ─ k))
-  length-remove (here _)  = refl
-  length-remove (there p) = cong suc (length-remove p)
+length-remove : (k : Any P xs) → length xs ≡ suc (length (xs ─ k))
+length-remove (here _)  = refl
+length-remove (there p) = cong suc (length-remove p)
 
 ------------------------------------------------------------------------
 -- append
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  append⁺ˡ : {xs ys : List# A R} {ps : All (_# ys) xs} →
-             Any P xs → Any P (append xs ys ps)
-  append⁺ˡ (here px) = here px
-  append⁺ˡ (there p) = there (append⁺ˡ p)
+append⁺ˡ : {ps : All (_# ys) xs} → Any P xs → Any P (append xs ys ps)
+append⁺ˡ (here px) = here px
+append⁺ˡ (there p) = there (append⁺ˡ p)
 
-  append⁺ʳ : {xs ys : List# A R} {ps : All (_# ys) xs} →
-             Any P ys → Any P (append xs ys ps)
-  append⁺ʳ {xs = []}      p = p
-  append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)
+append⁺ʳ : {ps : All (_# ys) xs} → Any P ys → Any P (append xs ys ps)
+append⁺ʳ {xs = []}      p = p
+append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)
 
-  append⁻ : ∀ xs {ys : List# A R} {ps : All (_# ys) xs} →
-            Any P (append xs ys ps) → Any P xs ⊎ Any P ys
-  append⁻ []        p         = inj₂ p
-  append⁻ (x ∷# xs) (here px) = inj₁ (here px)
-  append⁻ (x ∷# xs) (there p) = Sum.map₁ there (append⁻ xs p)
+append⁻ : ∀ xs {ps : All (_# ys) xs} →
+          Any P (append xs ys ps) → Any P xs ⊎ Any P ys
+append⁻ []        p         = inj₂ p
+append⁻ (x ∷# xs) (here px) = inj₁ (here px)
+append⁻ (x ∷# xs) (there p) = Sum.map₁ there (append⁻ xs p)