Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)

MatthewDaggitt · andreasabel · commit b391a3d3958f · 2024-07-10T10:43:52.000+02:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1238,6 +1238,12 @@ Major improvements
   pre-existing `Reasoning` module in just a couple of lines
   (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
 
+* One pre-requisite for that is that `≡-Reasoning` has been moved from
+  `Relation.Binary.PropositionalEquality.Core` (which shouldn't be
+  imported anyway as it's a `Core` module) to 
+  `Relation.Binary.PropositionalEquality.Properties`.
+  It is still exported by `Relation.Binary.PropositionalEquality`.
+  
 Deprecated modules
 ------------------
 
diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda
@@ -21,6 +21,8 @@ open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
@@ -218,7 +220,7 @@ lookup-transpose n (as ∷ ass) = begin
   lookup as n ∷ lookup (transpose ass) n     ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩
   lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩
   List.map (flip lookup n) (as ∷ ass)        ∎
-  where open P.≡-Reasoning
+  where open ≡-Reasoning
 
 lookup-transpose⁺ : ∀ n (ass : List⁺ (Stream A)) →
                     lookup (transpose⁺ ass) n ≡ List⁺.map (flip lookup n) ass
@@ -228,7 +230,7 @@ lookup-transpose⁺ n (as ∷ ass) = begin
   lookup as n ∷ lookup (transpose ass) n     ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩
   lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩
   List⁺.map (flip lookup n) (as ∷ ass)       ∎
-  where open P.≡-Reasoning
+  where open ≡-Reasoning
 
 lookup-tails : ∀ n (as : Stream A) → lookup (tails as) n ≈ ℕ.iterate tail as n
 lookup-tails zero    as = B.refl
diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda
@@ -26,6 +26,8 @@ open import Level
 open import Relation.Unary using (Pred)
 import Induction.WellFounded as WF
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 import Relation.Binary.Construct.On as On
 
 private
@@ -132,7 +134,7 @@ merge xss = ⟦ merge′ xss ⟧P
 Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss
 Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ ∘ to xss)
   where
-  open P.≡-Reasoning
+  open ≡-Reasoning
 
   -- The from function.
 
diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda
@@ -25,6 +25,8 @@ open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
@@ -116,7 +118,7 @@ lookup-iterate-identity (suc n)  f a = begin
   lookup (iterate f (f a)) n   ≡⟨ lookup-iterate-identity n f (f a) ⟩
   fold (f a) f n               ≡⟨ fold-pull a f (const ∘′ f) (f a) P.refl (λ _ → P.refl) n ⟩
   f (fold a f n)               ≡⟨⟩
-  fold a f (suc n)             ∎ where open P.≡-Reasoning
+  fold a f (suc n)             ∎ where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- DEPRECATED
diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda
@@ -16,6 +16,8 @@ module Data.Fin.Relation.Unary.Top where
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁)
 open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda
@@ -16,9 +16,11 @@ import Data.Vec.Properties as VecProp
 open import Function.Base as Fun using (_∘_; _$_; flip)
 open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; refl; sym; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_; _▻_)
-open PropEq.≡-Reasoning
+open ≡-Reasoning
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
@@ -31,8 +31,8 @@ open import Relation.Nullary
 open import Relation.Nullary.Decidable using (dec-true; dec-false)
 open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; _≢_; refl; cong)
-open PropEq.≡-Reasoning
 import Relation.Binary.PropositionalEquality.Properties as PropEq
+open PropEq.≡-Reasoning
 
 private
   open module D = DecSetoid D
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda
@@ -10,7 +10,8 @@
 
 module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
 open ≡-Reasoning
 
 open import Data.List.Base using (List; []; _∷_; [_])
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
@@ -16,7 +16,9 @@ open import Data.List.Relation.Ternary.Interleaving hiding (map)
 open import Function.Base using (_$_)
 open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; cong; module ≡-Reasoning)
+  using (_≡_; refl; sym; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open ≡-Reasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -43,6 +43,8 @@ open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Binary.Definitions as B
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no)
@@ -219,7 +221,7 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
      (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
 ×↔ {P = P} {Q = Q} {xs} {ys} = mk↔ₛ′ Any-×⁺ Any-×⁻ to∘from from∘to
   where
-  open P.≡-Reasoning
+  open ≡-Reasoning
 
   from∘to : ∀ pq → Any-×⁻ (Any-×⁺ pq) ≡ pq
   from∘to (p , q) =
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
@@ -20,7 +20,7 @@ open import Data.Product.Base as Prod
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.PropositionalEquality.Core as P
-  using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning)
+  using (_≡_; _≢_; refl; trans; cong; subst)
 open import Relation.Nullary as Nullary hiding (recompute)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core using (Rel)
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
@@ -24,6 +24,8 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Binary.Definitions using (tri<; tri>; tri≈; Symmetric)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; subst; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Nullary.Decidable using (Dec)
 open import Relation.Nullary.Negation using (contradiction)
 import Relation.Nullary.Decidable as Dec
@@ -190,7 +192,7 @@ c*gcd[m,n]≡gcd[cm,cn] c@(suc _) m n = begin
   c * gcd m n                   ≡⟨ cong (c *_) (P.sym (gcd[cm,cn]/c≡gcd[m,n] c m n)) ⟩
   c * (gcd (c * m) (c * n) / c) ≡⟨ m*[n/m]≡n (gcd-greatest (m∣m*n m) (m∣m*n n)) ⟩
   gcd (c * m) (c * n)           ∎
-  where open P.≡-Reasoning
+  where open ≡-Reasoning
 
 gcd[m,n]≤n : ∀ m n .{{_ : NonZero n}} → gcd m n ≤ n
 gcd[m,n]≤n m n = ∣⇒≤ (gcd[m,n]∣n m n)
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
@@ -18,7 +18,9 @@ open import Data.Nat.GCD
 open import Data.Product.Base using (_×_; _,_; uncurry′; ∃)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality.Core as P
-  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
+  using (_≡_; refl; sym; trans; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Nullary.Decidable using (False; fromWitnessFalse)
 
 private
diff --git a/src/Data/String/Unsafe.agda b/src/Data/String/Unsafe.agda
@@ -16,8 +16,11 @@ open import Data.Product.Base using (proj₂)
 open import Data.String.Base
 open import Function.Base using (_∘′_)
 
-open import Relation.Binary.PropositionalEquality.Core; open ≡-Reasoning
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)
+open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of tail
diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda
@@ -22,6 +22,8 @@ open import Function.Base using (_∘_; id; _$_)
 open import Level using (Level)
 open import Relation.Nullary.Decidable.Core using (recompute)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
@@ -66,7 +68,7 @@ private
     m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ P.cong (m +_) (ℕₚ.+-comm ⌈ k /2⌉ ⌊ k /2⌋) ⟩
     m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ P.cong (m +_) (ℕₚ.⌊n/2⌋+⌈n/2⌉≡n k) ⟩
     m + k                   ≡⟨ eq ⟩
-    n                       ∎ where open P.≡-Reasoning
+    n                       ∎ where open ≡-Reasoning
 
 padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n
 padBoth aₗ aᵣ as@(vs , m≤n)
diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda
@@ -15,6 +15,8 @@ open import Data.Vec.Recursive
 open import Data.Vec.Base using (Vec; _∷_)
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Relation.Binary.PropositionalEquality.Core as P
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open ≡-Reasoning
 
 private
diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -18,7 +18,9 @@ open import Data.Vec.Base
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions using (Sym; Trans)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; trans; sym; cong; module ≡-Reasoning)
+  using (_≡_; refl; trans; sym; cong)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Effect/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda
@@ -16,6 +16,8 @@ open import Data.Product.Base using (_×_; _,_)
 open import Function.Base
 open import Level
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 
 private
   variable
@@ -111,4 +113,4 @@ record Morphism {I : Set i} {F₁ F₂ : IFun I f}
     op (A₁._⊛_ (A₁.pure f) x)       ≡⟨ op-⊛ _ _ ⟩
     A₂._⊛_ (op (A₁.pure f)) (op x)  ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩
     A₂._⊛_ (A₂.pure f) (op x)       ∎
-    where open P.≡-Reasoning
+    where open ≡-Reasoning
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
@@ -29,6 +29,8 @@ open import Function.Related.Propositional
 import Function.Construct.Identity as Identity
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
 import Relation.Nullary.Indexed as I
@@ -284,7 +286,7 @@ private
     from C↔D (to C↔D (f (from A↔B (to A↔B x))))  ≡⟨ strictlyInverseʳ C↔D _ ⟩
     f (from A↔B (to A↔B x))                        ≡⟨ P.cong f $ strictlyInverseʳ A↔B x ⟩
     f x                                              ∎)
-  where open Inverse; open P.≡-Reasoning
+  where open Inverse; open ≡-Reasoning
 
 →-cong :  Extensionality a c → Extensionality b d →
           ∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda
@@ -91,35 +91,3 @@ resp₂ _∼_ = respʳ _∼_ , respˡ _∼_
 
 ≢-sym : Symmetric {A = A} _≢_
 ≢-sym x≢y =  x≢y ∘ sym
-
-------------------------------------------------------------------------
--- Convenient syntax for equational reasoning
-
--- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
--- Rather than instantiating the latter with (setoid A), we reimplement
--- equation chains from scratch since then goals are printed much more
--- readably.
-
-module ≡-Reasoning {A : Set a} where
-
-  infix  3 _∎
-  infixr 2 _≡⟨⟩_ step-≡ step-≡˘
-  infix  1 begin_
-
-  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
-  begin_ x≡y = x≡y
-
-  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
-  _ ≡⟨⟩ x≡y = x≡y
-
-  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
-  step-≡ _ y≡z x≡y = trans x≡y y≡z
-
-  step-≡˘ : ∀ (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z
-  step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z
-
-  _∎ : ∀ (x : A) → x ≡ x
-  _∎ _ = refl
-
-  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
-  syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
diff --git a/src/Relation/Binary/PropositionalEquality/Properties.agda b/src/Relation/Binary/PropositionalEquality/Properties.agda
@@ -23,6 +23,8 @@ open import Relation.Binary.Definitions
 import Relation.Binary.Properties.Setoid as Setoid
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Unary using (Pred)
+open import Relation.Binary.Reasoning.Syntax
+
 
 private
   variable
@@ -188,3 +190,16 @@ preorder A = Setoid.≈-preorder (setoid A)
 
 poset : Set a → Poset _ _ _
 poset A = Setoid.≈-poset (setoid A)
+
+------------------------------------------------------------------------
+-- Reasoning
+
+-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
+-- Rather than instantiating the latter with (setoid A), we reimplement
+-- equation chains from scratch since then goals are printed much more
+-- readably.
+module ≡-Reasoning {a} {A : Set a} where
+
+  open begin-syntax {A = A} _≡_ id public
+  open ≡-syntax {A = A} _≡_ trans public
+  open end-syntax {A = A} _≡_ refl public
diff --git a/src/Relation/Binary/Reasoning/Syntax.agda b/src/Relation/Binary/Reasoning/Syntax.agda
@@ -22,7 +22,6 @@ open import Relation.Binary.PropositionalEquality.Core as P
 --   Relation/Binary/HeterogeneousEquality
 --   Effect/Monad/Partiality
 --   Effect/Monad/Partiality/All
---   Relation/Binary/PropositionalEquality/Core
 --   Codata/Guarded/Stream/Relation/Binary/Pointwise
 --   Codata/Sized/Stream/Bisimilarity
 --   Function/Reasoning
