Make reasoning modular by adding new Reasoning.Syntax module (#2152)

Author: MatthewDaggitt

CHANGELOG.md

@@ -33,6 +33,9 @@ Bug-fixes
   in `Function.Construct.Composition` had their arguments in the wrong order. They have
   been flipped so they can actually be used as a composition operator.
 
+* The combinators `_≃⟨_⟩_` and `_≃˘⟨_⟩_` in `Data.Rational.Properties.≤-Reasoning`
+  now correctly accepts proofs of type `_≃_` instead of the previous proofs of type `_≡_`.
+
 * The following operators were missing a fixity declaration, which has now
   been fixed -
   ```
@@ -536,6 +539,10 @@ Non-backwards compatible changes
   3. Finally, if the above approaches are not viable then you may be forced to explicitly
      use `cong` combined with a lemma that proves the old reduction behaviour.
 
+* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base` 
+  has been made into a data type with the single constructor `*≡*`. The destructor `drop-*≡*`
+  has been added to `Data.Rational.Properties`.
+
 ### Change to the definition of `LeftCancellative` and `RightCancellative`
 
 * The definitions of the types for cancellativity in `Algebra.Definitions` previously
@@ -1222,6 +1229,15 @@ Major improvements
 
 * In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_`
 
+### More modular design of equational reasoning.
+
+* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports 
+  a range of modules containing pre-existing reasoning combinator syntax.
+
+* This makes it possible to add new or rename existing reasoning combinators to a 
+  pre-existing `Reasoning` module in just a couple of lines 
+  (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
+
 Deprecated modules
 ------------------
 
@@ -1793,6 +1809,11 @@ Deprecated names
   sym-↔   ↦   ↔-sym
   ```
 
+* In `Function.Related.Propositional.Reasoning`:
+  ```agda
+  _↔⟨⟩_  ↦  _≡⟨⟩_
+  ```
+  
 * In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`:
   ```
   toForeign   ↦ Foreign.Haskell.Coerce.coerce
@@ -2685,6 +2706,8 @@ Additions to existing modules
   toℕ-inverseˡ  : Inverseˡ _≡_ _≡_ toℕ fromℕ
   toℕ-inverseʳ  : Inverseʳ _≡_ _≡_ toℕ fromℕ
   toℕ-inverseᵇ  : Inverseᵇ _≡_ _≡_ toℕ fromℕ
+  
+  <-asym : Asymmetric _<_
   ```
 
 * Added a new pattern synonym to `Data.Nat.Divisibility.Core`:
@@ -2854,6 +2877,7 @@ Additions to existing modules
   ```agda
   ↥ᵘ-toℚᵘ : ↥ᵘ (toℚᵘ p) ≡ ↥ p
   ↧ᵘ-toℚᵘ : ↧ᵘ (toℚᵘ p) ≡ ↧ p
+  ↥p≡↥q≡0⇒p≡q : ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≡ q
 
   _≥?_ : Decidable _≥_
   _>?_ : Decidable _>_
@@ -2878,6 +2902,10 @@ Additions to existing modules
 
 * Added new definitions in `Data.Rational.Unnormalised.Properties`:
   ```agda
+  ↥p≡0⇒p≃0 : ↥ p ≡ 0ℤ → p ≃ 0ℚᵘ
+  p≃0⇒↥p≡0 : p ≃ 0ℚᵘ → ↥ p ≡ 0ℤ
+  ↥p≡↥q≡0⇒p≃q : ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≃ q
+
   +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
   +-*-rawSemiring     : RawSemiring 0ℓ 0ℓ
 

src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda

@@ -127,10 +127,14 @@ module _ {A : Set a} where
 
 ------------------------------------------------------------------------
 -- Pointwise DSL
+--
 -- A guardedness check does not play well with compositional proofs.
 -- Luckily we can learn from Nils Anders Danielsson's
 -- Beating the Productivity Checker Using Embedded Languages
 -- and design a little compositional DSL to define such proofs
+--
+-- NOTE: also because of the guardedness check we can't use the standard
+-- `Relation.Binary.Reasoning.Syntax` approach.
 
 module pw-Reasoning (S : Setoid a ℓ) where
   private module S = Setoid S

src/Codata/Musical/Colist.agda

@@ -34,6 +34,7 @@ import Relation.Binary.Construct.FromRel as Ind
 import Relation.Binary.Reasoning.Preorder as PreR
 import Relation.Binary.Reasoning.PartialOrder as POR
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.Reasoning.Syntax
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Negation
@@ -165,12 +166,11 @@ Any-∈ {P = P} = mk↔ₛ′
 module ⊑-Reasoning {a} {A : Set a} where
   private module Base = POR (⊑-Poset A)
 
-  open Base public
-    hiding (step-<; begin-strict_; step-≤)
+  open Base public hiding (step-<; step-≤)
+
+  open ⊑-syntax _IsRelatedTo_ _IsRelatedTo_ Base.≤-go public
+  open ⊏-syntax _IsRelatedTo_ _IsRelatedTo_ Base.<-go public
 
-  infixr 2 step-⊑
-  step-⊑ = Base.step-≤
-  syntax step-⊑ x ys⊑zs xs⊑ys = x ⊑⟨ xs⊑ys ⟩ ys⊑zs
 
 -- The subset relation forms a preorder.
 
@@ -179,22 +179,22 @@ module ⊑-Reasoning {a} {A : Set a} where
                  (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys))
   where module ⊑P = Poset (⊑-Poset A)
 
+-- Example uses:
+--
+--    x∈zs : x ∈ zs
+--    x∈zs =
+--      x  ∈⟨ x∈xs ⟩
+--      xs ⊆⟨ xs⊆ys ⟩
+--      ys ≡⟨ ys≡zs ⟩
+--      zs  ∎
 module ⊆-Reasoning {A : Set a} where
   private module Base = PreR (⊆-Preorder A)
 
-  open Base public
-    hiding (step-∼)
-
-  infixr 2 step-⊆
-  infix  1 step-∈
-
-  step-⊆ = Base.step-∼
+  open Base public hiding (step-∼)
 
-  step-∈ : ∀ (x : A) {xs ys} → xs IsRelatedTo ys → x ∈ xs → x ∈ ys
-  step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs
+  open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x)
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public
 
-  syntax step-⊆ xs ys⊆zs xs⊆ys = xs ⊆⟨ xs⊆ys ⟩ ys⊆zs
-  syntax step-∈ x  xs⊆ys x∈xs  = x  ∈⟨ x∈xs  ⟩ xs⊆ys
 
 -- take returns a prefix.
 take-⊑ : ∀ n (xs : Colist A) →

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

@@ -26,7 +26,6 @@ open import Relation.Binary.Core using (REL)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≗_; refl)
 
-open Related.EquationalReasoning hiding (_≡⟨_⟩_)
 private
   module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ)
 
@@ -71,6 +70,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x}
     (∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong ↔-refl (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩
     (∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ SK-sym (↔∈ C) ⟩
     ◇ C P₂ xs₂               ∎
+    where open Related.EquationalReasoning
 
 -- Nested occurrences of ◇ can sometimes be swapped.
 
@@ -95,6 +95,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
     (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y)  ↔⟨ Σ.cong ↔-refl (Σ.cong ↔-refl (SK-sym (↔∈ C₁))) ⟩
     (∃ λ y → y ∈ ys × ◇ _ (flip P y) xs)       ↔⟨ SK-sym (↔∈ C₂) ⟩
     ◇ _ (λ y → ◇ _ (flip P y) xs) ys           ∎
+    where open Related.EquationalReasoning
 
 -- Nested occurrences of ◇ can sometimes be flattened.
 
@@ -162,9 +163,10 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
   map↔∘ : ∀ {xs : ⟦ C ⟧ X} (f : X → Y) → ◇ C P (map f xs) ↔ ◇ C (P ∘′ f) xs
   map↔∘ {xs} f =
    ◇ C P (map f xs)          ↔⟨ ↔Σ C ⟩
-   ∃ (P ∘′ proj₂ (map f xs)) ↔⟨⟩
+   ∃ (P ∘′ proj₂ (map f xs)) ≡⟨⟩
    ∃ (P ∘′ f ∘′ proj₂ xs)    ↔⟨ SK-sym (↔Σ C) ⟩
    ◇ C (P ∘′ f) xs           ∎
+   where open Related.EquationalReasoning
 
 -- Membership in a mapped container can be expressed without reference
 -- to map.
@@ -178,6 +180,7 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
     y ∈ map f xs               ↔⟨ map↔∘ C (y ≡_) f ⟩
     ◇ C (λ x → y ≡ f x) xs     ↔⟨ ↔∈ C ⟩
     ∃ (λ x → x ∈ xs × y ≡ f x) ∎
+    where open Related.EquationalReasoning
 
 -- map is a congruence for bag and set equality and related preorders.
 
@@ -193,6 +196,7 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
     ◇ C (λ y → x ≡ f₂ y) xs₂ ↔⟨ SK-sym (map↔∘ C (_≡_ x) f₂) ⟩
     x ∈ map f₂ xs₂           ∎
     where
+    open Related.EquationalReasoning
     helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y)
     helper y rewrite f₁≗f₂ y = ↔-refl
 
@@ -205,7 +209,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
   remove-linear {xs} m = mk↔ₛ′ t f t∘f f∘t
     where
     open _≃_
-    open P.≡-Reasoning renaming (_∎ to _∎′)
+    open P.≡-Reasoning
 
     position⊸m : ∀ {s} → Position C₂ (shape⊸ m s) ≃ Position C₁ s
     position⊸m = ↔⇒≃ (position⊸ m)
@@ -259,7 +263,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
 
          P.subst (P ∘ proj₂ xs) P.refl p                        ≡⟨⟩
 
-        p                                                       ∎′)
+        p                                                       ∎)
       )
 
     t∘f : t ∘ f ≗ id
@@ -279,7 +283,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
                                                                      (P.trans-symˡ (right-inverse-of position⊸m _)) ⟩
          P.subst (P ∘ proj₂ xs) P.refl p                        ≡⟨⟩
 
-        p                                                       ∎′)
+        p                                                       ∎)
       )
 
 -- Linear endomorphisms are identity functions if bag equality is used.
@@ -290,6 +294,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x} where
   linear-identity {xs} m {x} =
     x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
     x ∈        xs  ∎
+    where open Related.EquationalReasoning
 
 -- If join can be expressed using a linear morphism (in a certain
 -- way), then it can be absorbed by the predicate.
@@ -307,4 +312,6 @@ module _ {s₁ s₂ s₃ p₁ p₂ p₃}
     ◇ C₃ P (⟪ join ⟫⊸ xss′) ↔⟨ remove-linear P join ⟩
     ◇ (C₁ C.∘ C₂) P xss′    ↔⟨ SK-sym $ flatten P xss ⟩
     ◇ C₁ (◇ C₂ P) xss       ∎
-    where xss′ = Inverse.from (Composition.correct C₁ C₂) xss
+    where
+    open Related.EquationalReasoning
+    xss′ = Inverse.from (Composition.correct C₁ C₂) xss

src/Data/Integer/Divisibility/Signed.agda

@@ -30,6 +30,7 @@ open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Nullary.Decidable using (yes; no)
 import Relation.Nullary.Decidable as DEC
+open import Relation.Binary.Reasoning.Syntax
 
 ------------------------------------------------------------------------
 -- Type
@@ -118,15 +119,11 @@ open _∣_ using (quotient) public
 -- Divisibility reasoning
 
 module ∣-Reasoning where
-  private
-    module Base = PreorderReasoning ∣-preorder
+  private module Base = PreorderReasoning ∣-preorder
 
-  open Base public
-    hiding (step-∼; step-≈; step-≈˘)
+  open Base public hiding (step-∼; step-≈; step-≈˘)
 
-  infixr 2 step-∣
-  step-∣ = Base.step-∼
-  syntax step-∣ x y∣z x∣y = x ∣⟨ x∣y ⟩ y∣z
+  open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public
 
 ------------------------------------------------------------------------
 -- Other properties of _∣_

src/Data/Integer/Properties.agda

@@ -364,7 +364,7 @@ i≮i = <-irrefl refl
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
-    <-irrefl
+    <-asym
     <-trans
     (resp₂ _<_)
     <⇒≤

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -37,11 +37,13 @@ open import Function.Related.TypeIsomorphisms
 open import Function.Properties.Inverse using (↔-sym; ↔-trans; to-from)
 open import Level using (Level)
 open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Definitions using (Trans)
 open import Relation.Binary.Bundles using (Preorder; Setoid)
 import Relation.Binary.Reasoning.Setoid as EqR
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)
+open import Relation.Binary.Reasoning.Syntax
 open import Relation.Nullary
 open import Data.List.Membership.Propositional.Properties
 
@@ -90,29 +92,22 @@ bag-=⇒ xs≈ys = ↔⇒ xs≈ys
 ------------------------------------------------------------------------
 -- "Equational" reasoning for _⊆_ along with an additional relatedness
 
-module ⊆-Reasoning where
-  private
-    module PreOrder {a} {A : Set a} = PreorderReasoning (⊆-preorder A)
+module ⊆-Reasoning {A : Set a} where
+  private module Base = PreorderReasoning (⊆-preorder A)
 
-  open PreOrder public
+  open Base public
     hiding (step-≈; step-≈˘; step-∼)
+    renaming (∼-go to ⊆-go)
 
-  infixr 2 step-∼ step-⊆
-  infix  1 step-∈
+  open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) public
+  open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public
 
-  step-⊆ = PreOrder.step-∼
+  module _ {k : Related.ForwardKind} where
+    ∼-go : Trans _∼[ ⌊ k ⌋→ ]_ _IsRelatedTo_ _IsRelatedTo_
+    ∼-go eq = ⊆-go (⇒→ eq)
 
-  step-∈ : ∀ x {xs ys : List A} →
-           xs IsRelatedTo ys → x ∈ xs → x ∈ ys
-  step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs
+    open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public
 
-  step-∼ : ∀ {k} xs {ys zs : List A} →
-           ys IsRelatedTo zs → xs ∼[ ⌊ k ⌋→ ] ys → xs IsRelatedTo zs
-  step-∼ xs ys⊆zs xs≈ys = step-⊆ xs ys⊆zs (⇒→ xs≈ys)
-
-  syntax step-∈ x  xs⊆ys x∈xs  = x ∈⟨ x∈xs ⟩ xs⊆ys
-  syntax step-∼ xs ys⊆zs xs≈ys = xs ∼⟨ xs≈ys ⟩ ys⊆zs
-  syntax step-⊆ xs ys⊆zs xs⊆ys = xs ⊆⟨ xs⊆ys ⟩ ys⊆zs
 
 ------------------------------------------------------------------------
 -- Congruence lemmas

src/Data/List/Relation/Binary/Permutation/Propositional.agda

@@ -16,6 +16,7 @@ open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions using (Reflexive; Transitive)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
+open import Relation.Binary.Reasoning.Syntax
 
 ------------------------------------------------------------------------
 -- An inductive definition of permutation
@@ -73,16 +74,15 @@ data _↭_ : Rel (List A) a where
 
 module PermutationReasoning where
 
-  private
-    module Base = EqReasoning ↭-setoid
+  private module Base = EqReasoning ↭-setoid
 
-  open EqReasoning ↭-setoid public
-    hiding (step-≈; step-≈˘)
+  open Base public hiding (step-≈; step-≈˘)
 
-  infixr 2 step-↭  step-↭˘ step-swap step-prep
+  open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public
 
-  step-↭  = Base.step-≈
-  step-↭˘ = Base.step-≈˘
+  -- Some extra combinators that allow us to skip certain elements
+
+  infixr 2 step-swap step-prep
 
   -- Skip reasoning on the first element
   step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
@@ -94,7 +94,5 @@ module PermutationReasoning where
               xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
   step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))
 
-  syntax step-↭  x y↭z x↭y = x ↭⟨  x↭y ⟩ y↭z
-  syntax step-↭˘ x y↭z y↭x = x ↭˘⟨  y↭x ⟩ y↭z
   syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
   syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z