Relation.Binary.PropositionalEquality over-use, (#2345)

* Relation.Binary.PropositionalEquality over-use, can usually be .Core and/or .Properties

* unused import

* another large batch of dependency cleanup, mostly cenetered on Relation.Binary.PropositionalEquality.

* another big batch of making imports more precise.

* last big batch. After this will come some tweaks based on reviews.

* fix things pointed out in review; add CHANGELOG.

* Update DecPropositional.agda

Bad merge

* proper merge

Author: JacquesCarette

CHANGELOG.md

@@ -30,6 +30,12 @@ Non-backwards compatible changes
 Other major improvements
 ------------------------
 
+Minor improvements
+------------------
+The size of the dependency graph for many modules has been
+reduced. This may lead to speed ups for first-time loading of some
+modules.
+
 Deprecated modules
 ------------------
 

src/Algebra/Consequences/Propositional.agda

@@ -14,7 +14,10 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (Symmetric; Total)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; cong₂; subst)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (setoid)
 open import Relation.Unary using (Pred)
 
 open import Algebra.Core

src/Algebra/Definitions/RawSemiring.agda

@@ -8,7 +8,7 @@
 
 open import Algebra.Bundles using (RawSemiring)
 open import Data.Sum.Base using (_⊎_)
-open import Data.Nat using (ℕ; zero; suc)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
 

src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

@@ -6,27 +6,29 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice
+open import Algebra.Lattice using (BooleanAlgebra; isBooleanAlgebraʳ;
+  isDistributiveLatticeʳʲᵐ)
 
 module Algebra.Lattice.Properties.BooleanAlgebra.Expression
   {b} (B : BooleanAlgebra b b)
   where
 
 open BooleanAlgebra B
 
-open import Effect.Applicative as Applicative
-open import Effect.Monad
 open import Data.Fin.Base using (Fin)
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 import Data.Vec.Effectful as Vec
 import Function.Identity.Effectful as Identity
 open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)
+open import Effect.Applicative as Applicative
 open import Function.Base using (_∘_; _$_; flip)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 import Relation.Binary.Reflection as Reflection
 
 -- Expressions made up of variables and the operations of a boolean
@@ -68,7 +70,7 @@ module Naturality
   (f : Applicative.Morphism A₁ A₂)
   where
 
-  open ≡.≡-Reasoning
+  open ≡-Reasoning
   open Applicative.Morphism f
   open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
   open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -25,7 +25,8 @@ import Relation.Binary.Reflection            as Reflection
 import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 open import Relation.Nullary.Decidable using (Dec)
 
 module Algebra.Solver.IdempotentCommutativeMonoid

src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda

@@ -9,16 +9,17 @@
 
 module Algebra.Solver.IdempotentCommutativeMonoid.Example where
 
-open import Relation.Binary.PropositionalEquality using (_≡_)
+import Algebra.Solver.IdempotentCommutativeMonoid as ICM-Solver
 
 open import Data.Bool.Base using (_∨_)
 open import Data.Bool.Properties using (∨-idempotentCommutativeMonoid)
 
 open import Data.Fin.Base using (zero; suc)
 open import Data.Vec.Base using ([]; _∷_)
 
-open import Algebra.Solver.IdempotentCommutativeMonoid
-  ∨-idempotentCommutativeMonoid
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+
+open ICM-Solver ∨-idempotentCommutativeMonoid
 
 test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ x
 test a b c = let _∨_ = _⊕_ in

src/Codata/Sized/Cofin.agda

@@ -8,15 +8,15 @@
 
 module Codata.Sized.Cofin where
 
-open import Size
-open import Codata.Sized.Thunk
+open import Size using (∞)
+open import Codata.Sized.Thunk using (force)
 open import Codata.Sized.Conat as Conat
   using (Conat; zero; suc; infinity; _ℕ<_; sℕ≤s; _ℕ≤infinity)
 open import Codata.Sized.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s)
-open import Data.Nat.Base
-open import Data.Fin.Base as Fin hiding (fromℕ; fromℕ<; toℕ)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Fin.Base using (Fin; zero; suc)
 open import Function.Base using (_∋_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
 -- The type

src/Data/Container/Combinator/Properties.agda

@@ -9,16 +9,15 @@
 module Data.Container.Combinator.Properties where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
-open import Data.Container.Core
+open import Data.Container.Core using (Container; ⟦_⟧)
 open import Data.Container.Combinator
-open import Data.Container.Relation.Unary.Any
 open import Data.Empty using (⊥-elim)
 open import Data.Product.Base as P using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
 open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
 open import Function.Base as F using (_∘′_)
-open import Function.Bundles
+open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (_⊔_; lower)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; cong)
 
 -- I have proved some of the correctness statements under the
 -- assumption of functional extensionality. I could have reformulated

src/Data/Container/Indexed/Combinator.agda

@@ -9,7 +9,8 @@
 module Data.Container.Indexed.Combinator where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
-open import Data.Container.Indexed
+open import Data.Container.Indexed using (Container; _◃_/_; ⟦_⟧;
+  Command; Response; ◇; next)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product.Base as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
@@ -18,10 +19,10 @@ open import Data.Sum.Relation.Unary.All as All using (All)
 open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
 open import Function.Bundles using (mk↔ₛ′)
 open import Function.Indexed.Bundles using (_↔ᵢ_)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂)
   renaming (_⟨×⟩_ to _⟪×⟫_; _⟨⊙⟩_ to _⟪⊙⟫_; _⟨⊎⟩_ to _⟪⊎⟫_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
   using (_≗_; refl; cong)
 
 private

src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda

@@ -8,13 +8,15 @@
 
 module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where
 
-open import Axiom.Extensionality.Propositional
-open import Data.Container.Indexed.Core
+open import Axiom.Extensionality.Propositional using (Extensionality)
+open import Data.Container.Indexed.Core using (Container; ⟦_⟧)
 open import Data.Container.Indexed.Relation.Binary.Pointwise
+  using (Pointwise)
 open import Data.Product.Base using (_,_; Σ-syntax; -,_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; subst; cong)
 
 private variable
@@ -28,18 +30,18 @@ module _
   where
 
   refl : (∀ i → Reflexive (R i)) → Reflexive (Pointwise C R o)
-  refl R-refl = P.refl , λ p → R-refl _
+  refl R-refl = ≡.refl , λ p → R-refl _
 
   sym : (∀ i → Symmetric (R i)) → Symmetric (Pointwise C R o)
-  sym R-sym (P.refl , f) = P.refl , λ p → R-sym _ (f p)
+  sym R-sym (≡.refl , f) = ≡.refl , λ p → R-sym _ (f p)
 
   trans : (∀ i → Transitive (R i)) → Transitive (Pointwise C R o)
-  trans R-trans (P.refl , f) (P.refl , g) = P.refl , λ p → R-trans _ (f p) (g p)
+  trans R-trans (≡.refl , f) (≡.refl , g) = ≡.refl , λ p → R-trans _ (f p) (g p)
 
 -- If propositional equality is extensional, then `Eq _≡_` and `_≡_` coincide.
 Eq⇒≡ : {C : Container I O ℓˢ ℓᵖ} {X : I → Set ℓˣ} {R : (i : I) → Rel (X i) ℓᵉ}
        {o : O} {xs ys : ⟦ C ⟧ X o} →
        Extensionality ℓᵖ ℓˣ →
        Pointwise C (λ (i : I) → _≡_ {A = X i}) o xs ys →
        xs ≡ ys
-Eq⇒≡ ext (P.refl , f≈f′) = cong -,_ (ext f≈f′)
+Eq⇒≡ ext (≡.refl , f≈f′) = cong -,_ (ext f≈f′)

src/Data/Container/Membership.agda

@@ -10,10 +10,10 @@ module Data.Container.Membership where
 
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
-open import Data.Container.Core
-open import Data.Container.Relation.Unary.Any
+open import Data.Container.Core using (Container; ⟦_⟧)
+open import Data.Container.Relation.Unary.Any using (◇)
 
 module _ {s p} {C : Container s p} {x} {X : Set x} where
 

src/Data/Container/Morphism/Properties.agda

@@ -12,7 +12,7 @@ open import Level using (_⊔_; suc)
 open import Function.Base as F using (_$_)
 open import Data.Product.Base using (∃; proj₁; proj₂; _,_)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; _≗_)
 
 open import Data.Container.Core
 open import Data.Container.Morphism

src/Data/Container/Relation/Binary/Pointwise/Properties.agda

@@ -8,9 +8,10 @@
 
 module Data.Container.Relation.Binary.Pointwise.Properties where
 
-open import Axiom.Extensionality.Propositional
-open import Data.Container.Core
+open import Axiom.Extensionality.Propositional using (Extensionality)
+open import Data.Container.Core using (Container; ⟦_⟧)
 open import Data.Container.Relation.Binary.Pointwise
+  using (Pointwise; _,_)
 open import Data.Product.Base using (_,_; Σ-syntax; -,_)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)

src/Data/Container/Relation/Unary/Any/Properties.agda

@@ -8,23 +8,25 @@
 
 module Data.Container.Relation.Unary.Any.Properties where
 
-open import Level
-open import Algebra
+open import Algebra.Bundles using (CommutativeSemiring)
 open import Data.Product.Base using (∃; _×_; ∃₂; _,_; proj₂)
 open import Data.Product.Properties using (Σ-≡,≡→≡)
 open import Data.Product.Function.NonDependent.Propositional using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
-open import Function.Base
-open import Function.Bundles
+open import Function.Base using (_∘_; _∘′_; id; flip; _$_)
+open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
 open import Function.Properties.Inverse using (↔-refl)
 open import Function.Properties.Inverse.HalfAdjointEquivalence using (_≃_; ↔⇒≃)
 open import Function.Related.Propositional as Related using (Related; SK-sym)
 open import Function.Related.TypeIsomorphisms
+  using (×-⊎-commutativeSemiring; ∃∃↔∃∃; Σ-assoc; ×-comm)
+open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred ; _∪_ ; _∩_)
 open import Relation.Binary.Core using (REL)
-open import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≗_; refl)
+open import Relation.Binary.PropositionalEquality.Properties as ≡
 
 private
   module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ)

src/Data/Fin/Induction.agda

@@ -7,8 +7,13 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 {-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
+module Data.Fin.Induction where
+
+open import Data.Fin.Base using (Fin; zero; suc; _<_; toℕ; inject₁;
+  _≥_; _>_; fromℕ; _≺_)
+open import Data.Fin.Properties using (toℕ-inject₁; ≤-refl; <-cmp;
+  toℕ≤n; toℕ-injective; toℕ-fromℕ; toℕ-lower₁; inject₁-lower₁;
+  pigeonhole; ≺⇒<′)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s)
 open import Data.Nat.Properties using (n<1+n; ≤⇒≯)
 import Data.Nat.Induction as ℕ
@@ -18,8 +23,9 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
 import Data.Vec.Relation.Unary.Linked.Properties as Linked
 open import Function.Base using (flip; _$_)
-open import Induction
-open import Induction.WellFounded as WF
+open import Induction using (RecStruct)
+open import Induction.WellFounded as WF using (WellFounded; WfRec;
+  module Subrelation)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (StrictPartialOrder)
@@ -30,13 +36,12 @@ import Relation.Binary.Construct.Flip.Ord as Ord
 import Relation.Binary.Construct.NonStrictToStrict as ToStrict
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; subst; trans; cong)
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 
-module Data.Fin.Induction where
-
 private
   variable
     ℓ : Level

src/Data/Fin/Permutation.agda

@@ -9,27 +9,29 @@
 module Data.Fin.Permutation where
 
 open import Data.Bool.Base using (true; false)
-open import Data.Empty using (⊥-elim)
-open import Data.Fin.Base
-open import Data.Fin.Patterns
-open import Data.Fin.Properties
+open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
+open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
+  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_; proj₂)
 open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)
 open import Function.Construct.Symmetry using (↔-sym)
-open import Function.Definitions
+open import Function.Definitions using (StrictlyInverseˡ; StrictlyInverseʳ)
 open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
 open import Relation.Nullary.Decidable using (dec-yes; dec-no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≢_; refl; sym; trans; subst; →-to-⟶; cong; cong₂; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open ≡-Reasoning
 
 private
@@ -241,7 +243,7 @@ module _ (π : Permutation (suc m) (suc n)) where
   lift₀-remove p (suc i) = punchOut-zero (πʳ (suc i)) p
     where
     punchOut-zero : ∀ {i} (j : Fin (suc n)) {neq} → i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
-    punchOut-zero 0F {neq} p = ⊥-elim (neq p)
+    punchOut-zero 0F {neq} p = contradiction p neq
     punchOut-zero (suc j) refl = refl
 
 ↔⇒≡ : Permutation m n → m ≡ n

src/Data/Fin/Permutation/Components.agda

@@ -9,15 +9,19 @@
 module Data.Fin.Permutation.Components where
 
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
 open import Data.Fin.Properties
+  using (_≟_; opposite-prop; opposite-involutive; opposite-suc)
 open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
 open import Data.Product.Base using (proj₂)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (does; _because_; yes; no)
 open import Relation.Nullary.Decidable using (dec-true; dec-false)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; trans)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Algebra.Definitions using (Involutive)
 open ≡-Reasoning