Change argument order for binary reasoning combinators (#1045)

Author: MatthewDaggitt

CHANGELOG.md

@@ -21,6 +21,67 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+#### Changes to how equational reasoning is implemented
+
+* NOTE: __Uses__ of equational reasoning remains unchanged. These changes should only
+  affect users who are renaming/hiding the library's equational reasoning combinators.
+
+* Previously all equational reasoning combinators (e.g. `_≈⟨_⟩_`, `_≡⟨_⟩_`, `_≤⟨_⟩_`)
+  have been defined in the following style:
+  ```agda
+  infixr 2 _≡⟨_⟩_
+
+  _≡⟨_⟩_ : ∀ x {y z : A} → x ≡ y → y ≡ z → x ≡ z
+  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
+  ```
+  The type checker therefore infers the RHS of the equational step from the LHS + the
+  type of the proof. For example for `x ≈⟨ x≈y ⟩ y ∎` it is inferred that `y ∎`
+  must have type `y IsRelatedTo y` from `x : A` and `x≈y : x ≈ y`.
+
+* There are two problems with this. Firstly, it means that the reasoning combinators are
+  not compatible with macros (i.e. tactics) that attempt to automatically generate proofs
+  for `x≈y`. This is because the reflection machinary does not have access to the type of RHS
+  as it cannot be inferred. In practice this meant that the new reflective solvers
+  `Tactic.RingSolver` and `Tactic.MonoidSolver` could not be used inside the equational
+  reasoning. Secondly the inference procedure itself is slower as described in this
+  [exchange](https://lists.chalmers.se/pipermail/agda/2016/009090.html)
+  on the Agda mailing list.
+
+* Therefore, as suggested on the mailing list, the order of arguments to the combinators
+  have been reversed so that instead the type of the proof is inferred from the LHS + RHS.
+  ```agda
+  infixr -2 step-≡
+
+  step-≡ : ∀ x {y z : A} → y ≡ z → x ≡ y → x ≡ z
+  step-≡ y≡z x≡y = trans x≡y y≡z
+
+  syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
+  ```
+  where the `syntax` declaration is then used to recover the original order of the arguments.
+  This change enables the use of macros and anecdotally speeds up type checking by a
+  factor of 5.
+
+* No changes are needed when defining new combinators, as the old and new styles are
+  compatible. Having said that you may want to switch to the new style for the benefits
+  described above.
+
+* One drawback is that hiding and renaming the combinators no longer works as before,
+  as `_≡⟨_⟩_` etc. are now syntax instead of names. For example instead of:
+  ```agda
+  open SetoidReasoning hiding (_≈⟨_⟩_) renaming (_≡⟨_⟩_ to _↭⟨_⟩_)
+  ```
+  one must now write :
+  ```agda
+  open SetoidReasoning hiding (step-≈; step-≡)
+
+  infixr 2 step-↭
+  step-↭ = step-≡
+  syntax step-↭ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
+  ```
+  This is more verbose than before, but we hope that the advantages outlined above
+  outweigh this minor inconvenience. (As an aside, it is hoped that at some point Agda might
+  provide the ability to rename syntax that automatically generates the above boilerplate).
+
 #### Tweak to definition of `Permutation.refl`
 
 * The definition of `refl` in `Data.List.Relation.Binary.Permutation.Homogeneous/Setoid`

README/Data/Nat.agda

@@ -39,13 +39,13 @@ ex₃ m n = *-comm m n
 -- provides some combinators for equational reasoning.
 
 open Relation.Binary.PropositionalEquality using (cong; module ≡-Reasoning)
-open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
 
 ex₄ : ∀ m n → m * (n + 0) ≡ n * m
 ex₄ m n = begin
   m * (n + 0)  ≡⟨ cong (_*_ m) (+-identityʳ n) ⟩
   m * n        ≡⟨ *-comm m n ⟩
   n * m        ∎
+  where open ≡-Reasoning
 
 -- The module SemiringSolver in Data.Nat.Solver contains a solver
 -- for natural number equalities involving variables, constants, _+_

src/Codata/Musical/Colist.agda

@@ -457,10 +457,15 @@ Any-∈ {P = P} = record
   antisym []       [] = []
   antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂)
 
-module ⊑-Reasoning where
-  private
-    open module R {a} {A : Set a} = POR (⊑-Poset A)
-      public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_)
+module ⊑-Reasoning {a} {A : Set a} where
+  private module Base = POR (⊑-Poset A)
+
+  open Base public
+    hiding (step-<; begin-strict_; step-≤)
+
+  infixr 2 step-⊑
+  step-⊑ = Base.step-≤
+  syntax step-⊑ x ys⊑zs xs⊑ys = x ⊑⟨ xs⊑ys ⟩ ys⊑zs
 
 -- The subset relation forms a preorder.
 
@@ -469,16 +474,22 @@ module ⊑-Reasoning where
                  (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys))
   where module ⊑P = Poset (⊑-Poset A)
 
-module ⊆-Reasoning where
-  private
-    open module R {a} {A : Set a} = PreR (⊆-Preorder A)
-      public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)
+module ⊆-Reasoning {a} {A : Set a} where
+  private module Base = PreR (⊆-Preorder A)
+
+  open Base public
+    hiding (step-∼)
+
+  infixr 2 step-⊆
+  infix  1 step-∈
+
+  step-⊆ = Base.step-∼
 
-  infix 1 _∈⟨_⟩_
+  step-∈ : ∀ (x : A) {xs ys} → xs IsRelatedTo ys → x ∈ xs → x ∈ ys
+  step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs
 
-  _∈⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {xs ys} →
-           x ∈ xs → xs IsRelatedTo ys → x ∈ ys
-  x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
+  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.
 

src/Data/Integer/Divisibility.agda

@@ -3,6 +3,7 @@
 --
 -- Unsigned divisibility
 ------------------------------------------------------------------------
+
 -- For signed divisibility see `Data.Integer.Divisibility.Signed`
 
 {-# OPTIONS --without-K --safe #-}

src/Data/Integer/Divisibility/Signed.agda

@@ -110,9 +110,19 @@ open _∣_ using (quotient) public
 ∣-preorder : Preorder _ _ _
 ∣-preorder = record { isPreorder = ∣-isPreorder }
 
-module ∣-Reasoning = PreorderReasoning ∣-preorder
-  hiding   (_≈⟨_⟩_)
-  renaming (_∼⟨_⟩_ to _∣⟨_⟩_)
+------------------------------------------------------------------------
+-- Divisibility reasoning
+
+module ∣-Reasoning where
+  private
+    module Base = PreorderReasoning ∣-preorder
+
+  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
 
 ------------------------------------------------------------------------
 -- Other properties of _∣_

src/Data/Integer/Properties.agda

@@ -306,7 +306,7 @@ module ≤-Reasoning where
     <-≤-trans
     ≤-<-trans
     public
-    hiding (_≈⟨_⟩_; _≈˘⟨_⟩_)
+    hiding (step-≈; step-≈˘)
 
 ------------------------------------------------------------------------
 -- Properties of -_

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

@@ -87,19 +87,24 @@ module ⊆-Reasoning where
     module PreOrder {a} {A : Set a} = PreorderReasoning (⊆-preorder A)
 
     open PreOrder
-      hiding (_≈⟨_⟩_; _≈˘⟨_⟩_)
-      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)
+      hiding (step-≈; step-≈˘; step-∼)
 
-  infixr 2 _∼⟨_⟩_
-  infix  1 _∈⟨_⟩_
+  infixr 2 step-∼ step-⊆
+  infix  1 step-∈
 
-  _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} →
-           x ∈ xs → xs IsRelatedTo ys → x ∈ ys
-  x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
+  step-⊆ = PreOrder.step-∼
 
-  _∼⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} →
-           xs ∼[ ⌊ k ⌋→ ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs
-  xs ∼⟨ xs≈ys ⟩ ys≈zs = xs ⊆⟨ ⇒→ xs≈ys ⟩ ys≈zs
+  step-∈ : ∀ {a} {A : Set a} x {xs ys : List A} →
+           xs IsRelatedTo ys → x ∈ xs → x ∈ ys
+  step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs
+
+  step-∼ : ∀ {k a} {A : Set a} 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

@@ -67,21 +67,28 @@ data _↭_ : Rel (List A) a where
 
 module PermutationReasoning where
 
-  open EqReasoning ↭-setoid
-    using (_IsRelatedTo_; relTo)
+  private
+    module Base = EqReasoning ↭-setoid
 
   open EqReasoning ↭-setoid public
-    using (begin_ ; _∎ ; _≡⟨⟩_; _≡⟨_⟩_)
-    renaming (_≈⟨_⟩_ to _↭⟨_⟩_; _≈˘⟨_⟩_ to _↭˘⟨_⟩_)
+    hiding (step-≈; step-≈˘)
 
-  infixr 2 _∷_<⟨_⟩_  _∷_∷_<<⟨_⟩_
+  infixr 2 step-↭  step-↭˘ step-swap step-prep
+
+  step-↭  = Base.step-≈
+  step-↭˘ = Base.step-≈˘
 
   -- Skip reasoning on the first element
-  _∷_<⟨_⟩_ : ∀ x xs {ys zs : List A} → xs ↭ ys →
-               (x ∷ ys) IsRelatedTo zs → (x ∷ xs) IsRelatedTo zs
-  x ∷ xs <⟨ xs↭ys ⟩ rel = relTo (trans (prep x xs↭ys) (begin rel))
+  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
+              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
+  step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel))
 
   -- Skip reasoning about the first two elements
-  _∷_∷_<<⟨_⟩_ : ∀ x y xs {ys zs : List A} → xs ↭ ys →
-                  (y ∷ x ∷ ys) IsRelatedTo zs → (x ∷ y ∷ xs) IsRelatedTo zs
-  x ∷ y ∷ xs <<⟨ xs↭ys ⟩ rel = relTo (trans (swap x y xs↭ys) (begin rel))
+  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
+              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

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

@@ -72,27 +72,38 @@ _↭_ = Homogeneous.Permutation _≈_
 
 module PermutationReasoning where
 
-  open SetoidReasoning ↭-setoid
-    using (_IsRelatedTo_; relTo)
+  private
+    module Base = SetoidReasoning ↭-setoid
 
   open SetoidReasoning ↭-setoid public
-    using (begin_ ; _∎ ; _≡⟨⟩_; _≡⟨_⟩_)
-    renaming (_≈⟨_⟩_ to _↭⟨_⟩_; _≈˘⟨_⟩_ to _↭˘⟨_⟩_)
+    hiding (step-≈; step-≈˘)
 
-  infixr 2 _∷_<⟨_⟩_  _∷_∷_<<⟨_⟩_ _≋⟨_⟩_ _≋˘⟨_⟩_
+  infixr 2 step-↭  step-↭˘ step-≋ step-≋˘ step-swap step-prep
 
-  -- Skip reasoning on the first element
-  _∷_<⟨_⟩_ : ∀ x xs {ys zs : List A} → xs ↭ ys →
-               (x ∷ ys) IsRelatedTo zs → (x ∷ xs) IsRelatedTo zs
-  x ∷ xs <⟨ xs↭ys ⟩ rel = relTo (trans (↭-prep _ xs↭ys) (begin rel))
+  step-↭  = Base.step-≈
+  step-↭˘ = Base.step-≈˘
 
-  -- Skip reasoning about the first two elements
-  _∷_∷_<<⟨_⟩_ : ∀ x y xs {ys zs : List A} → xs ↭ ys →
-                  (y ∷ x ∷ ys) IsRelatedTo zs → (x ∷ y ∷ xs) IsRelatedTo zs
-  x ∷ y ∷ xs <<⟨ xs↭ys ⟩ rel = relTo (trans (↭-swap _ _ xs↭ys) (begin rel))
+  -- Step with pointwise list equality
+  step-≋ : ∀ x {y z} → y IsRelatedTo z → x ≋ y → x IsRelatedTo z
+  step-≋ x (relTo y↔z) x≋y = relTo (trans (refl x≋y) y↔z)
 
-  _≋⟨_⟩_ : ∀ x {y z} → x ≋ y → y IsRelatedTo z → x IsRelatedTo z
-  x ≋⟨ x≈y ⟩ (relTo y↔z) = relTo (trans (refl x≈y) y↔z)
+  -- Step with flipped pointwise list equality
+  step-≋˘ : ∀ x {y z} → y IsRelatedTo z → y ≋ x → x IsRelatedTo z
+  step-≋˘ x y↭z y≋x = x ≋⟨ ≋-sym y≋x ⟩ y↭z
 
-  _≋˘⟨_⟩_ : ∀ x {y z} → y ≋ x → y IsRelatedTo z → x IsRelatedTo z
-  x ≋˘⟨ y≈x ⟩ y∼z = x ≋⟨ ≋-sym y≈x ⟩ y∼z
+  -- Skip reasoning on the first element
+  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
+              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
+  step-prep x xs rel xs↭ys = relTo (trans (prep Eq.refl xs↭ys) (begin rel))
+
+  -- Skip reasoning about the first two elements
+  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
+              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
+  step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl 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-≋  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

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -70,7 +70,7 @@ module _ {a} (A : Set a) where
 
 module ⊆-Reasoning {a} (A : Set a) where
   open Setoidₚ.⊆-Reasoning (setoid A) public
-    hiding (_≋⟨_⟩_; _≋˘⟨_⟩_; _≋⟨⟩_)
+    hiding (step-≋; step-≋˘; _≋⟨⟩_)
 
 ------------------------------------------------------------------------
 -- Properties relating _⊆_ to various list functions