From 15f128b2c9092851b8d1cc5cf76a44d8306932c6 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 17 Oct 2023 09:26:05 +0900 Subject: [PATCH 1/3] =?UTF-8?q?Move=20=E2=89=A1-Reasoning=20from=20Core=20?= =?UTF-8?q?to=20Properties=20and=20implement=20using=20syntax?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 6 ++++ src/Codata/Guarded/Stream/Properties.agda | 6 ++-- src/Codata/Musical/Colist/Infinite-merge.agda | 4 ++- src/Codata/Sized/Stream/Properties.agda | 4 ++- src/Data/Fin/Relation/Unary/Top.agda | 2 ++ src/Data/Fin/Substitution/Lemmas.agda | 4 ++- src/Data/List/Countdown.agda | 2 +- .../Example/UniqueBoundVariables.agda | 3 +- .../Ternary/Interleaving/Properties.agda | 4 ++- .../List/Relation/Unary/Any/Properties.agda | 4 ++- src/Data/Nat/Coprimality.agda | 2 +- src/Data/Nat/GCD.agda | 4 ++- src/Data/Nat/LCM.agda | 4 ++- src/Data/String/Unsafe.agda | 5 ++- src/Data/Vec/Bounded/Base.agda | 4 ++- src/Data/Vec/Recursive/Properties.agda | 2 ++ .../Vec/Relation/Binary/Equality/Cast.agda | 4 ++- src/Effect/Applicative/Indexed.agda | 4 ++- src/Function/Related/TypeIsomorphisms.agda | 4 ++- .../Binary/PropositionalEquality/Core.agda | 32 ------------------- .../PropositionalEquality/Properties.agda | 15 +++++++++ src/Relation/Binary/Reasoning/Syntax.agda | 1 - 22 files changed, 70 insertions(+), 50 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 89e22ce60e..2dcdb3d924 100644 --- 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 index bd41d1967e..3742aab856 100644 --- 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 index cbc142ff5a..584880a768 100644 --- 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 index d2cf4e3205..40cb3fc961 100644 --- 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 index b6a567a9a8..a884a09243 100644 --- 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 index ffa26e64fb..8b4d0b176a 100644 --- 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 index 8d6761de27..dbfd75b332 100644 --- 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 index 39a6fe65a1..163818b6e8 100644 --- 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 index dff26bb6b2..5317d5a7c5 100644 --- 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 index aba1a777ee..b88bdfbe95 100644 --- 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 index f6f91b44e5..1df320ea96 100644 --- 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 index 555a902df6..b88947c707 100644 --- 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 index 545870574f..5dff2eb530 100644 --- 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 index ff1ff28408..35b408f131 100644 --- 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 index 63649e940e..c926c9dfb1 100644 --- 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 index b012e59a80..d036134a45 100644 --- 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 index adca0a42f2..f65981f7a3 100644 --- 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 index 30e9b632bb..f547e68b27 100644 --- 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 index 830bb6f8bb..9fb1fded28 100644 --- 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 index c0c4030b83..848258348b 100644 --- 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 index 9515b77700..a420e45b64 100644 --- 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 index 4837fe33f4..e8286bee30 100644 --- 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 From 23e616ec324835ffaadae34bed8a01eccbc294a0 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 17 Oct 2023 15:41:52 +0900 Subject: [PATCH 2/3] Rename symmetric reasoning combinators. Minimal set of changes --- CHANGELOG.md | 48 ++++-- .../Vec/Relation/Binary/Equality/Cast.agda | 16 +- .../Stream/Relation/Binary/Pointwise.agda | 35 ++++- src/Data/Integer/Properties.agda | 2 +- .../Relation/Binary/BagAndSetEquality.agda | 2 +- .../Binary/Permutation/Propositional.agda | 6 +- .../Relation/Binary/Permutation/Setoid.agda | 8 +- .../Binary/Subset/Setoid/Properties.agda | 2 +- src/Data/Nat/Binary/Properties.agda | 2 +- src/Data/Nat/Divisibility.agda | 2 +- src/Data/Nat/Properties.agda | 2 +- src/Data/Rational/Properties.agda | 33 +++-- .../Rational/Unnormalised/Properties.agda | 31 ++-- src/Data/Vec/Properties.agda | 16 +- .../Vec/Relation/Binary/Equality/Cast.agda | 49 +++---- .../ReflexiveTransitive/Properties.agda | 2 +- .../Binary/HeterogeneousEquality.agda | 14 +- src/Relation/Binary/Reasoning/Syntax.agda | 137 ++++++++++++++---- 18 files changed, 268 insertions(+), 139 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dcdb3d924..728f892002 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -849,6 +849,7 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` + ### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder` * Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its @@ -989,6 +990,39 @@ Non-backwards compatible changes Relation.Binary.Reasoning.PartialOrder ``` +### 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`) + +* 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`. + +### Renaming of symmetric combinators for equational reasoning + +* We've had various complaints about the symmetric version of reasoning combinators + that use the syntax `_R˘⟨_⟩_` for some relation `R`, (e.g. `_≡˘⟨_⟩_` and `_≃˘⟨_⟩_`) + introduced in `v1.0`. In particular: + 1. The symbol `˘` is hard to type. + 2. The symbol `˘` doesn't convey the direction of the equality + 3. The left brackets aren't vertically aligned with the left brackets of the non-symmetric version. + +* To address these problems we have renamed all the symmetric versions of the + combinators from `_R˘⟨_⟩_` to `_R⟨_⟨_` (the direction of the last bracket is flipped + to indicate the quality goes from right to left). + +* The old combinators still exist but have been deprecated. However due to + [Agda issue #5617](https://github.com/agda/agda/issues/5617), the deprecation warnings + don't fire correctly. We will not remove the old combinators before the above issue is + addressed. However, we still encourage migrating to the new combinators! + ### Other * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used @@ -1229,20 +1263,6 @@ 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`) - -* 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/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/README/Data/Vec/Relation/Binary/Equality/Cast.agda index fb76544ed7..c13d0d8481 100644 --- a/README/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/README/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -86,7 +86,7 @@ example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x example1a-fromList-∷ʳ x xs eq = begin cast eq (fromList (xs L.∷ʳ x)) ≡⟨⟩ - cast eq (fromList (xs L.++ L.[ x ])) ≡˘⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟩ + cast eq (fromList (xs L.++ L.[ x ])) ≡⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟨ cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩ cast eq₂ (fromList xs ++ [ x ]) ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩ fromList xs ∷ʳ x ∎ @@ -105,7 +105,7 @@ example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc example1b-fromList-∷ʳ x xs eq = begin fromList (xs L.∷ʳ x) ≈⟨⟩ fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩ - fromList xs ++ [ x ] ≈˘⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟩ + fromList xs ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟨ fromList xs ∷ʳ x ∎ where open CastReasoning @@ -149,7 +149,7 @@ example2b eq xs a ys = begin (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ -- index: suc m + n reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ -- index: suc m + n (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n - reverse xs ++ (a ∷ ys) ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩ -- index: m + suc n + reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n xs ʳ++ (a ∷ ys) ∎ -- index: m + suc n where open CastReasoning @@ -201,11 +201,11 @@ example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys → cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a) example4-cong² {m = m} {n} eq a xs ys = begin - reverse ((xs ++ [ a ]) ++ ys) ≈˘⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)) + reverse ((xs ++ [ a ]) ++ ys) ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)) (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a)) - (unfold-∷ʳ _ a xs)) ⟩ + (unfold-∷ʳ _ a xs)) ⟨ reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩ - reverse ys ++ reverse (xs ∷ʳ a) ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩ + reverse ys ++ reverse (xs ∷ʳ a) ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨ ys ʳ++ reverse (xs ∷ʳ a) ∎ where open CastReasoning @@ -237,7 +237,7 @@ example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin -- and then switch to the reasoning system of `_≈[_]_`. example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs example6a-reverse-∷ʳ {n = n} x xs = begin-≡ - reverse (xs ∷ʳ x) ≡˘⟨ ≈-reflexive refl ⟩ + reverse (xs ∷ʳ x) ≡⟨ ≈-reflexive refl ⟨ reverse (xs ∷ʳ x) ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩ reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩ x ∷ reverse xs ∎ @@ -249,6 +249,6 @@ example6b-reverse-∷ʳ-by-induction x (y ∷ xs) = begin reverse (y ∷ (xs ∷ʳ x)) ≡⟨ reverse-∷ y (xs ∷ʳ x) ⟩ reverse (xs ∷ʳ x) ∷ʳ y ≡⟨ cong (_∷ʳ y) (example6b-reverse-∷ʳ-by-induction x xs) ⟩ (x ∷ reverse xs) ∷ʳ y ≡⟨⟩ - x ∷ (reverse xs ∷ʳ y) ≡˘⟨ cong (x ∷_) (reverse-∷ y xs) ⟩ + x ∷ (reverse xs ∷ʳ y) ≡⟨ cong (x ∷_) (reverse-∷ y xs) ⟨ x ∷ reverse (y ∷ xs) ∎ where open ≡-Reasoning diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda index 9f573cc711..a4908e851f 100644 --- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda +++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda @@ -180,7 +180,7 @@ module pw-Reasoning (S : Setoid a ℓ) where run `rs .tail = run (`tail `rs) infix 1 begin_ - infixr 2 _↺⟨_⟩_ _↺˘⟨_⟩_ _∼⟨_⟩_ _∼˘⟨_⟩_ _≈⟨_⟩_ _≈˘⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_ + infixr 2 _↺⟨_⟩_ _↺⟨_⟨_ _∼⟨_⟩_ _∼⟨_⟨_ _≈⟨_⟩_ _≈⟨_⟨_ _≡⟨_⟩_ _≡⟨_⟨_ _≡⟨⟩_ infix 3 _∎ -- Beginning of a proof @@ -189,16 +189,41 @@ module pw-Reasoning (S : Setoid a ℓ) where (begin `rs) .tail = run (`rs .tail) pattern _↺⟨_⟩_ as as∼bs bs∼cs = `trans {as = as} (`step as∼bs) bs∼cs - pattern _↺˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`step bs∼as)) bs∼cs + pattern _↺⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`step bs∼as)) bs∼cs pattern _∼⟨_⟩_ as as∼bs bs∼cs = `trans {as = as} (`lift as∼bs) bs∼cs - pattern _∼˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`lift bs∼as)) bs∼cs + pattern _∼⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`lift bs∼as)) bs∼cs pattern _≈⟨_⟩_ as as∼bs bs∼cs = `trans {as = as} (`bisim as∼bs) bs∼cs - pattern _≈˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs + pattern _≈⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs pattern _≡⟨_⟩_ as as∼bs bs∼cs = `trans {as = as} (`refl as∼bs) bs∼cs - pattern _≡˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs + pattern _≡⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs pattern _≡⟨⟩_ as as∼bs = `trans {as = as} (`refl P.refl) as∼bs pattern _∎ as = `refl {as = as} P.refl + + -- Deprecated v2.0 + infixr 2 _↺˘⟨_⟩_ _∼˘⟨_⟩_ _≈˘⟨_⟩_ _≡˘⟨_⟩_ + pattern _↺˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`step bs∼as)) bs∼cs + pattern _∼˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`lift bs∼as)) bs∼cs + pattern _≈˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs + pattern _≡˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs + {-# WARNING_ON_USAGE _↺˘⟨_⟩_ + "Warning: _↺˘⟨_⟩_ was deprecated in v2.0. + Please use _↺⟨_⟨_ instead." + #-} + {-# WARNING_ON_USAGE _∼˘⟨_⟩_ + "Warning: _∼˘⟨_⟩_ was deprecated in v2.0. + Please use _∼⟨_⟨_ instead." + #-} + {-# WARNING_ON_USAGE _≈˘⟨_⟩_ + "Warning: _≈˘⟨_⟩_ was deprecated in v2.0. + Please use _≈⟨_⟨_ instead." + #-} + {-# WARNING_ON_USAGE _≡˘⟨_⟩_ + "Warning: _≡˘⟨_⟩_ was deprecated in v2.0. + Please use _≡⟨_⟨_ instead." + #-} + + module ≈-Reasoning {a} {A : Set a} where open pw-Reasoning (P.setoid A) public diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 13ed3deab8..4e3d999011 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -371,7 +371,7 @@ module ≤-Reasoning where <-≤-trans ≤-<-trans public - hiding (step-≈; step-≈˘) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) ------------------------------------------------------------------------ -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_ diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index f842ae8087..a5f6fbec14 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -96,7 +96,7 @@ module ⊆-Reasoning {A : Set a} where private module Base = PreorderReasoning (⊆-preorder A) open Base public - hiding (step-≈; step-≈˘; step-∼; step-≲) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) renaming (≲-go to ⊆-go) open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) public diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index 28cf25d9ed..382b4f4520 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -76,9 +76,11 @@ module PermutationReasoning where private module Base = EqReasoning ↭-setoid - open Base public hiding (step-≈; step-≈˘) + open Base public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) + renaming (∼-go to ↭-go) - open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public -- Some extra combinators that allow us to skip certain elements diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index 0d375226db..234993113a 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -90,10 +90,12 @@ module PermutationReasoning where private module Base = SetoidReasoning ↭-setoid - open Base public hiding (step-≈; step-≈˘) + open Base public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) + renaming (∼-go to ↭-go) - open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public - open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (Base.∼-go ∘′ refl) ≋-sym public + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public -- Some extra combinators that allow us to skip certain elements diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index bb20fd417f..0c344758b7 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -118,7 +118,7 @@ module ⊆-Reasoning (S : Setoid a ℓ) where private module Base = PreorderReasoning (⊆-preorder S) open Base public - hiding (step-≲; step-≈; step-≈˘; step-∼) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼) renaming (≲-go to ⊆-go; ≈-go to ≋-go) open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → Base.begin x) public diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 9e8976842e..65ac8005fd 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -613,7 +613,7 @@ module ≤-Reasoning where <-≤-trans ≤-<-trans public - hiding (step-≈; step-≈˘) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) ------------------------------------------------------------------------ -- Properties of _<ℕ_ diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 63037a49b2..b5c74798cb 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -121,7 +121,7 @@ module ∣-Reasoning where private module Base = PreorderReasoning ∣-preorder open Base public - hiding (step-≈; step-≈˘; step-∼; step-≲) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) renaming (≲-go to ∣-go) open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∣-go public diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 74350e1f6b..7ecb431cce 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -498,7 +498,7 @@ module ≤-Reasoning where <-≤-trans ≤-<-trans public - hiding (step-≈; step-≈˘) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) open ≤-Reasoning diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 915eb6e058..a2d4c97788 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -441,7 +441,7 @@ fromℚᵘ-cong : fromℚᵘ Preserves _≃ᵘ_ ⟶ _≡_ fromℚᵘ-cong {p} {q} p≃q = toℚᵘ-injective (begin-equality toℚᵘ (fromℚᵘ p) ≃⟨ toℚᵘ-fromℚᵘ p ⟩ p ≃⟨ p≃q ⟩ - q ≃˘⟨ toℚᵘ-fromℚᵘ q ⟩ + q ≃⟨ toℚᵘ-fromℚᵘ q ⟨ toℚᵘ (fromℚᵘ q) ∎) where open ℚᵘ.≤-Reasoning @@ -749,7 +749,8 @@ module ≤-Reasoning where ≤-<-trans as Triple - open Triple public hiding (step-≈; step-≈˘) + open Triple public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) ≃-go : Trans _≃_ _IsRelatedTo_ _IsRelatedTo_ ≃-go = Triple.≈-go ∘′ ≃⇒≡ @@ -1242,7 +1243,7 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i *-cancelʳ-≤-pos : ∀ r .{{_ : Positive r}} → p * r ≤ q * r → p ≤ q *-cancelʳ-≤-pos {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-pos (toℚᵘ r) (begin - toℚᵘ p ℚᵘ.* toℚᵘ r ≃˘⟨ toℚᵘ-homo-* p r ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) @@ -1255,7 +1256,7 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i *-monoʳ-≤-nonNeg r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin toℚᵘ (p * r) ≃⟨ toℚᵘ-homo-* p r ⟩ toℚᵘ p ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonNeg (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ - toℚᵘ q ℚᵘ.* toℚᵘ r ≃˘⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ q ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* q r ⟨ toℚᵘ (q * r) ∎) where open ℚᵘ.≤-Reasoning @@ -1266,7 +1267,7 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i *-monoʳ-≤-nonPos r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ toℚᵘ q ℚᵘ.* toℚᵘ r ≤⟨ ℚᵘ.*-monoˡ-≤-nonPos (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩ - toℚᵘ p ℚᵘ.* toℚᵘ r ≃˘⟨ toℚᵘ-homo-* p r ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ toℚᵘ (p * r) ∎) where open ℚᵘ.≤-Reasoning @@ -1275,9 +1276,9 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i *-cancelʳ-≤-neg : ∀ r .{{_ : Negative r}} → p * r ≤ q * r → p ≥ q *-cancelʳ-≤-neg {p} {q} r pr≤qr = toℚᵘ-cancel-≤ (ℚᵘ.*-cancelʳ-≤-neg _ (begin - toℚᵘ p ℚᵘ.* toℚᵘ r ≃˘⟨ toℚᵘ-homo-* p r ⟩ - toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ - toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ + toℚᵘ p ℚᵘ.* toℚᵘ r ≃⟨ toℚᵘ-homo-* p r ⟨ + toℚᵘ (p * r) ≤⟨ toℚᵘ-mono-≤ pr≤qr ⟩ + toℚᵘ (q * r) ≃⟨ toℚᵘ-homo-* q r ⟩ toℚᵘ q ℚᵘ.* toℚᵘ r ∎)) where open ℚᵘ.≤-Reasoning @@ -1291,7 +1292,7 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i *-monoˡ-<-pos r {p} {q} p q *-cancelˡ-<-nonPos {p} {q} r rp_ *-monoˡ-<-neg r {p} {q} p0}} p0 = positive (neg-mono-< (negative⁻¹ r)) @@ -1328,7 +1329,7 @@ private *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → q < p *-cancelˡ-<-nonPos {p} {q} r rp1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1 1/-antimono-≤-pos : ∀ {p q} .{{_ : Positive p}} .{{_ : Positive q}} → p ≤ q → (1/ q) {{pos⇒nonZero q}} ≤ (1/ p) {{pos⇒nonZero p}} 1/-antimono-≤-pos {p} {q} p≤q = begin - 1/q ≃˘⟨ *-identityˡ 1/q ⟩ - 1ℚᵘ * 1/q ≃˘⟨ *-congʳ (*-inverseˡ p) ⟩ + 1/q ≃⟨ *-identityˡ 1/q ⟨ + 1ℚᵘ * 1/q ≃⟨ *-congʳ (*-inverseˡ p) ⟨ (1/p * p) * 1/q ≤⟨ *-monoˡ-≤-nonNeg 1/q (*-monoʳ-≤-nonNeg 1/p p≤q) ⟩ (1/p * q) * 1/q ≃⟨ *-assoc 1/p q 1/q ⟩ 1/p * (q * 1/q) ≃⟨ *-congˡ {1/p} (*-inverseʳ q) ⟩ diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 38793a9038..a71d854c61 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1015,7 +1015,7 @@ reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin reverse (xs ++ ys) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))) (reverse-++ _ xs ys) ⟩ (reverse ys ++ reverse xs) ∷ʳ x ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩ - reverse ys ++ (reverse xs ∷ʳ x) ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩ + reverse ys ++ (reverse xs ∷ʳ x) ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨ reverse ys ++ (reverse (x ∷ xs)) ∎ where open CastReasoning @@ -1025,7 +1025,7 @@ cast-reverse {n = suc n} eq (x ∷ xs) = begin reverse (x ∷ xs) ≂⟨ reverse-∷ x xs ⟩ reverse xs ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ eq x (reverse xs)) (cast-reverse (cong pred eq) xs) ⟩ - reverse (cast _ xs) ∷ʳ x ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩ + reverse (cast _ xs) ∷ʳ x ≂⟨ reverse-∷ x (cast (cong pred eq) xs) ⟨ reverse (x ∷ cast _ xs) ≈⟨⟩ reverse (cast eq (x ∷ xs)) ∎ where open CastReasoning @@ -1064,7 +1064,7 @@ map-ʳ++ {ys = ys} f xs = begin (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ - reverse xs ++ (a ∷ ys) ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩ + reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ xs ʳ++ (a ∷ ys) ∎ where open CastReasoning @@ -1075,8 +1075,8 @@ map-ʳ++ {ys = ys} f xs = begin reverse (xs ++ ys) ++ zs ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys))) (reverse-++ (+-comm m n) xs ys) ⟩ (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩ - reverse ys ++ (reverse xs ++ zs) ≂˘⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟩ - reverse ys ++ (xs ʳ++ zs) ≂˘⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟩ + reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨ + reverse ys ++ (xs ʳ++ zs) ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨ ys ʳ++ (xs ʳ++ zs) ∎ where open CastReasoning @@ -1089,7 +1089,7 @@ map-ʳ++ {ys = ys} f xs = begin (reverse-++ (+-comm m n) (reverse xs) ys) ⟩ (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩ (reverse ys ++ xs) ++ zs ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩ - reverse ys ++ (xs ++ zs) ≂˘⟨ unfold-ʳ++ ys (xs ++ zs) ⟩ + reverse ys ++ (xs ++ zs) ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨ ys ʳ++ (xs ++ zs) ∎ where open CastReasoning @@ -1315,10 +1315,10 @@ fromList-reverse List.[] = refl fromList-reverse (x List.∷ xs) = begin fromList (List.reverse (x List.∷ xs)) ≈⟨ cast-fromList (Listₚ.ʳ++-defn xs) ⟩ fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩ - fromList (List.reverse xs) ++ [ x ] ≈˘⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟩ + fromList (List.reverse xs) ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨ fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (Listₚ.length-reverse xs)) _ _) (fromList-reverse xs) ⟩ - reverse (fromList xs) ∷ʳ x ≂˘⟨ reverse-∷ x (fromList xs) ⟩ + reverse (fromList xs) ∷ʳ x ≂⟨ reverse-∷ x (fromList xs) ⟨ reverse (x ∷ fromList xs) ≈⟨⟩ reverse (fromList (x List.∷ xs)) ∎ where open CastReasoning diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda index f65981f7a3..21848d2ca3 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -84,18 +84,28 @@ module CastReasoning where xs ≈⟨⟩ xs≈ys = xs≈ys -- composition of _≈[_]_ - step-≈ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → + step-≈-⟩ : ∀ .{m≡n : m ≡ n}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → ys ≈[ trans (sym m≡n) m≡o ] zs → xs ≈[ m≡n ] ys → xs ≈[ m≡o ] zs - step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs + step-≈-⟩ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs + + step-≈-⟨ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → + ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs + step-≈-⟨ xs ys≈zs ys≈xs = step-≈-⟩ xs ys≈zs (≈-sym ys≈xs) -- composition of the equality type on the right-hand side of _≈[_]_, -- or escaping to ordinary _≡_ - step-≃ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs - step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs) + step-≃-⟩ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → xs ≈[ m≡n ] ys → xs ≈[ m≡n ] zs + step-≃-⟩ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs) + + step-≃-⟨ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs + step-≃-⟨ xs ys≡zs ys≈xs = step-≃-⟩ xs ys≡zs (≈-sym ys≈xs) -- composition of the equality type on the left-hand side of _≈[_]_ - step-≂ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs - step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs + step-≂-⟩ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → xs ≡ ys → xs ≈[ m≡n ] zs + step-≂-⟩ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs + + step-≂-⟨ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs + step-≂-⟨ xs ys≈zs ys≡xs = step-≂-⟩ xs ys≈zs (sym ys≡xs) -- `cong` after a `_≈[_]_` step that exposes the `cast` to the `cong` -- operation @@ -103,29 +113,16 @@ module CastReasoning where xs ≈[ m≡n ] f (cast l≡o ys) → ys ≈[ l≡o ] zs → xs ≈[ m≡n ] f zs ≈-cong f xs≈fys ys≈zs = trans xs≈fys (cong f ys≈zs) - - -- symmetric version of each of the operator - step-≈˘ : ∀ .{n≡m : n ≡ m}.{m≡o : m ≡ o} (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → - ys ≈[ trans n≡m m≡o ] zs → ys ≈[ n≡m ] xs → xs ≈[ m≡o ] zs - step-≈˘ xs ys≈zs ys≈xs = step-≈ xs ys≈zs (≈-sym ys≈xs) - - step-≃˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≡ zs → ys ≈[ sym m≡n ] xs → xs ≈[ m≡n ] zs - step-≃˘ xs ys≡zs ys≈xs = step-≃ xs ys≡zs (≈-sym ys≈xs) - - step-≂˘ : ∀ .{m≡n : m ≡ n} (xs : Vec A m) {ys zs} → ys ≈[ m≡n ] zs → ys ≡ xs → xs ≈[ m≡n ] zs - step-≂˘ xs ys≈zs ys≡xs = step-≂ xs ys≈zs (sym ys≡xs) - - ------------------------------------------------------------------------ -- convenient syntax for ‘equational’ reasoning infix 1 begin_ - infixr 2 step-≃ step-≂ step-≃˘ step-≂˘ step-≈ step-≈˘ _≈⟨⟩_ ≈-cong + infixr 2 step-≃-⟩ step-≃-⟨ step-≂-⟩ step-≂-⟨ step-≈-⟩ step-≈-⟨ _≈⟨⟩_ ≈-cong infix 3 _∎ - syntax step-≃ xs ys≡zs xs≈ys = xs ≃⟨ xs≈ys ⟩ ys≡zs - syntax step-≃˘ xs ys≡zs xs≈ys = xs ≃˘⟨ xs≈ys ⟩ ys≡zs - syntax step-≂ xs ys≈zs xs≡ys = xs ≂⟨ xs≡ys ⟩ ys≈zs - syntax step-≂˘ xs ys≈zs ys≡xs = xs ≂˘⟨ ys≡xs ⟩ ys≈zs - syntax step-≈ xs ys≈zs xs≈ys = xs ≈⟨ xs≈ys ⟩ ys≈zs - syntax step-≈˘ xs ys≈zs ys≈xs = xs ≈˘⟨ ys≈xs ⟩ ys≈zs + syntax step-≃-⟩ xs ys≡zs xs≈ys = xs ≃⟨ xs≈ys ⟩ ys≡zs + syntax step-≃-⟨ xs ys≡zs xs≈ys = xs ≃⟨ xs≈ys ⟨ ys≡zs + syntax step-≂-⟩ xs ys≈zs xs≡ys = xs ≂⟨ xs≡ys ⟩ ys≈zs + syntax step-≂-⟨ xs ys≈zs ys≡xs = xs ≂⟨ ys≡xs ⟨ ys≈zs + syntax step-≈-⟩ xs ys≈zs xs≈ys = xs ≈⟨ xs≈ys ⟩ ys≈zs + syntax step-≈-⟨ xs ys≈zs ys≈xs = xs ≈⟨ ys≈xs ⟨ ys≈zs diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda index 58b2ee198a..a78d14938b 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda @@ -116,7 +116,7 @@ module StarReasoning {i t} {I : Set i} (T : Rel I t) where private module Base = PreorderReasoning (preorder T) open Base public - hiding (step-≈; step-∼; step-≲) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) renaming (≲-go to ⟶-go) open ⟶-syntax _IsRelatedTo_ _IsRelatedTo_ (⟶-go ∘ (_◅ ε)) public diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda index 4581514feb..9181229eec 100644 --- a/src/Relation/Binary/HeterogeneousEquality.agda +++ b/src/Relation/Binary/HeterogeneousEquality.agda @@ -255,15 +255,23 @@ module ≅-Reasoning where -- Can't create syntax in the standard `Syntax` module for -- heterogeneous steps because it would force that module to use -- the `--with-k` option. - infixr 2 _≅⟨_⟩_ _≅˘⟨_⟩_ + infixr 2 _≅⟨_⟩_ _≅⟨_⟨_ _≅⟨_⟩_ : ∀ (x : A) {y : B} {z : C} → x ≅ y → y IsRelatedTo z → x IsRelatedTo z _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z) - _≅˘⟨_⟩_ : ∀ (x : A) {y : B} {z : C} → + _≅⟨_⟨_ : ∀ (x : A) {y : B} {z : C} → y ≅ x → y IsRelatedTo z → x IsRelatedTo z - _ ≅˘⟨ y≅x ⟩ relTo y≅z = relTo (trans (sym y≅x) y≅z) + _ ≅⟨ y≅x ⟨ relTo y≅z = relTo (trans (sym y≅x) y≅z) + + -- Deprecated + infixr 2 _≅˘⟨_⟩_ + _≅˘⟨_⟩_ = _≅⟨_⟨_ + {-# WARNING_ON_USAGE _≅˘⟨_⟩_ + "Warning: _≅˘⟨_⟩_ was deprecated in v2.0. + Please use _≅⟨_⟨_ instead." + #-} ------------------------------------------------------------------------ -- Inspect diff --git a/src/Relation/Binary/Reasoning/Syntax.agda b/src/Relation/Binary/Reasoning/Syntax.agda index e8286bee30..4806512296 100644 --- a/src/Relation/Binary/Reasoning/Syntax.agda +++ b/src/Relation/Binary/Reasoning/Syntax.agda @@ -23,7 +23,6 @@ open import Relation.Binary.PropositionalEquality.Core as P -- Effect/Monad/Partiality -- Effect/Monad/Partiality/All -- Codata/Guarded/Stream/Relation/Binary/Pointwise --- Codata/Sized/Stream/Bisimilarity -- Function/Reasoning module Relation.Binary.Reasoning.Syntax where @@ -259,37 +258,80 @@ module _ -- Setoid equality syntax module ≈-syntax where + infixr 2 step-≈-⟩ step-≈-⟨ + step-≈-⟩ = forward + step-≈-⟨ = backward + syntax step-≈-⟩ x yRz x≈y = x ≈⟨ x≈y ⟩ yRz + syntax step-≈-⟨ x yRz y≈x = x ≈⟨ y≈x ⟨ yRz + + -- Deprecated infixr 2 step-≈ step-≈˘ - step-≈ = forward - step-≈˘ = backward - syntax step-≈ x yRz x≈y = x ≈⟨ x≈y ⟩ yRz + step-≈ = step-≈-⟩ + {-# WARNING_ON_USAGE step-≈ + "Warning: step-≈ was deprecated in v2.0. + Please use step-≈-⟩ instead." + #-} + step-≈˘ = step-≈-⟨ + {-# WARNING_ON_USAGE step-≈˘ + "Warning: step-≈˘ and _≈˘⟨_⟩_ was deprecated in v2.0. + Please use step-≈-⟨ and _≈⟨_⟨_ instead." + #-} syntax step-≈˘ x yRz y≈x = x ≈˘⟨ y≈x ⟩ yRz -- Container equality syntax module ≋-syntax where + infixr 2 step-≋-⟩ step-≋-⟨ + step-≋-⟩ = forward + step-≋-⟨ = backward + syntax step-≋-⟩ x yRz x≋y = x ≋⟨ x≋y ⟩ yRz + syntax step-≋-⟨ x yRz y≋x = x ≋⟨ y≋x ⟨ yRz + + + -- Don't remove until https://github.com/agda/agda/issues/5617 fixed. infixr 2 step-≋ step-≋˘ - step-≋ = forward - step-≋˘ = backward - syntax step-≋ x yRz x≋y = x ≋⟨ x≋y ⟩ yRz + step-≋ = step-≋-⟩ + {-# WARNING_ON_USAGE step-≋ + "Warning: step-≋ was deprecated in v2.0. + Please use step-≋-⟩ instead." + #-} + step-≋˘ = step-≋-⟨ + {-# WARNING_ON_USAGE step-≋˘ + "Warning: step-≋˘ and _≋˘⟨_⟩_ was deprecated in v2.0. + Please use step-≋-⟨ and _≋⟨_⟨_ instead." + #-} syntax step-≋˘ x yRz y≋x = x ≋˘⟨ y≋x ⟩ yRz -- Other equality syntax module ≃-syntax where - infixr 2 step-≃ step-≃˘ - step-≃ = forward - step-≃˘ = backward - syntax step-≃ x yRz x≃y = x ≃⟨ x≃y ⟩ yRz - syntax step-≃˘ x yRz y≃x = x ≃˘⟨ y≃x ⟩ yRz + infixr 2 step-≃-⟩ step-≃-⟨ + step-≃-⟩ = forward + step-≃-⟨ = backward + syntax step-≃-⟩ x yRz x≃y = x ≃⟨ x≃y ⟩ yRz + syntax step-≃-⟨ x yRz y≃x = x ≃⟨ y≃x ⟨ yRz -- Apartness relation syntax module #-syntax where + infixr 2 step-#-⟩ step-#-⟨ + step-#-⟩ = forward + step-#-⟨ = backward + syntax step-#-⟩ x yRz x#y = x #⟨ x#y ⟩ yRz + syntax step-#-⟨ x yRz y#x = x #⟨ y#x ⟨ yRz + + -- Don't remove until https://github.com/agda/agda/issues/5617 fixed. infixr 2 step-# step-#˘ - step-# = forward - step-#˘ = backward - syntax step-# x yRz x#y = x #⟨ x#y ⟩ yRz + step-# = step-#-⟩ + {-# WARNING_ON_USAGE step-# + "Warning: step-# was deprecated in v2.0. + Please use step-#-⟩ instead." + #-} + step-#˘ = step-#-⟨ + {-# WARNING_ON_USAGE step-#˘ + "Warning: step-#˘ and _#˘⟨_⟩_ was deprecated in v2.0. + Please use step-#-⟨ and _#⟨_⟨_ instead." + #-} syntax step-#˘ x yRz y#x = x #˘⟨ y#x ⟩ yRz @@ -304,20 +346,35 @@ module _ -- Inverse syntax module ↔-syntax where - infixr 2 step-↔ step-↔-sym - step-↔ = forward - step-↔-sym = backward - syntax step-↔ x yRz x↔y = x ↔⟨ x↔y ⟩ yRz - syntax step-↔-sym x yRz y↔x = x ↔˘⟨ y↔x ⟩ yRz + infixr 2 step-↔-⟩ step-↔-⟨ + step-↔-⟩ = forward + step-↔-⟨ = backward + syntax step-↔-⟩ x yRz x↔y = x ↔⟨ x↔y ⟩ yRz + syntax step-↔-⟨ x yRz y↔x = x ↔⟨ y↔x ⟨ yRz -- Inverse syntax module ↭-syntax where - infixr 2 step-↭ step-↭-sym + infixr 2 step-↭-⟩ step-↭-⟨ + step-↭-⟩ = forward + step-↭-⟨ = backward + syntax step-↭-⟩ x yRz x↭y = x ↭⟨ x↭y ⟩ yRz + syntax step-↭-⟨ x yRz y↭x = x ↭⟨ y↭x ⟨ yRz + + + -- Don't remove until https://github.com/agda/agda/issues/5617 fixed. + infixr 2 step-↭ step-↭˘ step-↭ = forward - step-↭-sym = backward - syntax step-↭ x yRz x↭y = x ↭⟨ x↭y ⟩ yRz - syntax step-↭-sym x yRz y↭x = x ↭˘⟨ y↭x ⟩ yRz + {-# WARNING_ON_USAGE step-↭ + "Warning: step-↭ was deprecated in v2.0. + Please use step-↭-⟩ instead." + #-} + step-↭˘ = backward + {-# WARNING_ON_USAGE step-↭˘ + "Warning: step-↭˘ and _↭˘⟨_⟩_ was deprecated in v2.0. + Please use step-↭-⟨ and _↭⟨_⟨_ instead." + #-} + syntax step-↭˘ x yRz y↭x = x ↭˘⟨ y↭x ⟩ yRz ------------------------------------------------------------------------ -- Propositional equality @@ -332,16 +389,32 @@ module ≡-syntax (step : Trans _≡_ R R) where - infixr 2 step-≡ step-≡-refl step-≡˘ - step-≡ = forward R R step - step-≡˘ = backward R R step P.sym + infixr 2 step-≡-⟩ step-≡-∣ step-≡-⟨ + step-≡-⟩ = forward R R step + + step-≡-∣ : ∀ x {y} → R x y → R x y + step-≡-∣ x xRy = xRy + + step-≡-⟨ = backward R R step P.sym + + syntax step-≡-⟩ x yRz x≡y = x ≡⟨ x≡y ⟩ yRz + syntax step-≡-∣ x xRy = x ≡⟨⟩ xRy + syntax step-≡-⟨ x yRz y≡x = x ≡⟨ y≡x ⟨ yRz - step-≡-refl : ∀ x {y} → R x y → R x y - step-≡-refl x xRy = xRy - syntax step-≡-refl x xRy = x ≡⟨⟩ xRy - syntax step-≡˘ x yRz y≡x = x ≡˘⟨ y≡x ⟩ yRz - syntax step-≡ x yRz x≡y = x ≡⟨ x≡y ⟩ yRz + -- Don't remove until https://github.com/agda/agda/issues/5617 fixed. + infixr 2 step-≡ step-≡˘ + step-≡ = step-≡-⟩ + {-# WARNING_ON_USAGE step-≡ + "Warning: step-≡ was deprecated in v2.0. + Please use step-≡-⟩ instead." + #-} + step-≡˘ = step-≡-⟨ + {-# WARNING_ON_USAGE step-≡˘ + "Warning: step-≡˘ and _≡˘⟨_⟩_ was deprecated in v2.0. + Please use step-≡-⟨ and _≡⟨_⟨_ instead." + #-} + syntax step-≡˘ x yRz y≡x = x ≡˘⟨ y≡x ⟩ yRz -- Unlike ≡-syntax above, chains of reasoning using this syntax will not From 4236d090ae6a5f33ba8604d5bab19cc4663f1b9c Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 17 Oct 2023 16:46:58 +0900 Subject: [PATCH 3/3] Migrate to new combinators --- CHANGELOG.md | 14 +++ README/Data/Fin/Relation/Unary/Top.agda | 4 +- .../Vec/Relation/Binary/Equality/Cast.agda | 8 +- README/Tactic/Cong.agda | 6 +- .../Properties/HeytingCommutativeRing.agda | 16 +-- src/Algebra/Consequences/Setoid.agda | 10 +- src/Algebra/Construct/LexProduct/Inner.agda | 36 +++---- src/Algebra/Construct/LiftedChoice.agda | 6 +- .../Construct/NaturalChoice/MinMaxOp.agda | 16 +-- .../Construct/NaturalChoice/MinOp.agda | 22 ++-- .../Lattice/Morphism/LatticeMonomorphism.agda | 4 +- .../Lattice/Properties/BooleanAlgebra.agda | 96 ++++++++--------- src/Algebra/Lattice/Properties/Lattice.agda | 4 +- src/Algebra/Module/Consequences.agda | 8 +- src/Algebra/Morphism/Consequences.agda | 8 +- src/Algebra/Morphism/GroupMonomorphism.agda | 6 +- src/Algebra/Morphism/MagmaMonomorphism.agda | 12 +-- src/Algebra/Morphism/MonoidMonomorphism.agda | 4 +- src/Algebra/Morphism/RingMonomorphism.agda | 12 +-- src/Algebra/Properties/AbelianGroup.agda | 2 +- .../CommutativeMonoid/Mult/TCOptimised.agda | 2 +- .../Properties/CommutativeMonoid/Sum.agda | 4 +- .../Properties/CommutativeSemigroup.agda | 4 +- src/Algebra/Properties/Group.agda | 16 +-- src/Algebra/Properties/Monoid/Mult.agda | 2 +- .../Properties/Monoid/Mult/TCOptimised.agda | 8 +- src/Algebra/Properties/Monoid/Sum.agda | 4 +- src/Algebra/Properties/Semiring/Binomial.agda | 34 +++--- src/Algebra/Properties/Semiring/Exp.agda | 8 +- .../Semiring/Exp/TailRecursiveOptimised.agda | 2 +- src/Algebra/Properties/Semiring/Mult.agda | 4 +- .../Properties/Semiring/Mult/TCOptimised.agda | 2 +- .../Solver/Ring/NaturalCoefficients.agda | 2 +- src/Codata/Sized/Colist/Properties.agda | 4 +- src/Data/Fin/Properties.agda | 16 +-- src/Data/Fin/Subset/Properties.agda | 2 +- src/Data/Integer/DivMod.agda | 2 +- src/Data/Integer/Properties.agda | 100 +++++++++--------- src/Data/List/Effectful.agda | 14 +-- src/Data/List/Properties.agda | 4 +- .../Relation/Binary/BagAndSetEquality.agda | 6 +- .../Binary/Permutation/Propositional.agda | 2 +- .../Permutation/Propositional/Properties.agda | 10 +- .../Relation/Binary/Permutation/Setoid.agda | 2 +- .../Binary/Permutation/Setoid/Properties.agda | 20 ++-- .../List/Relation/Unary/Any/Properties.agda | 4 +- src/Data/Nat/Binary/Properties.agda | 6 +- src/Data/Nat/Combinatorics.agda | 30 +++--- src/Data/Nat/Combinatorics/Specification.agda | 8 +- src/Data/Nat/DivMod.agda | 50 ++++----- src/Data/Nat/DivMod/WithK.agda | 2 +- src/Data/Nat/Divisibility.agda | 4 +- src/Data/Nat/LCM.agda | 6 +- src/Data/Nat/Primality.agda | 6 +- src/Data/Nat/Properties.agda | 16 +-- src/Data/Rational/Properties.agda | 20 ++-- .../Rational/Unnormalised/Properties.agda | 86 +++++++-------- src/Data/Tree/Binary/Zipper/Properties.agda | 12 +-- src/Data/Tree/Rose/Properties.agda | 4 +- src/Data/Vec/Functional/Properties.agda | 8 +- src/Data/Vec/Properties.agda | 14 +-- .../Vec/Relation/Binary/Equality/Cast.agda | 4 +- src/Function/Properties/Surjection.agda | 2 +- .../Binary/Construct/NaturalOrder/Right.agda | 2 +- .../Binary/Reasoning/PartialOrder.agda | 4 +- src/Relation/Binary/Reasoning/Preorder.agda | 2 +- src/Relation/Binary/Reasoning/Setoid.agda | 6 +- .../Binary/Reasoning/StrictPartialOrder.agda | 4 +- src/Tactic/Cong.agda | 2 +- src/Tactic/MonoidSolver.agda | 4 +- .../Core/Polynomial/Homomorphism/Lemmas.agda | 8 +- src/Text/Pretty/Core.agda | 2 +- 72 files changed, 450 insertions(+), 434 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 728f892002..fde6ec3527 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1023,6 +1023,20 @@ Non-backwards compatible changes don't fire correctly. We will not remove the old combinators before the above issue is addressed. However, we still encourage migrating to the new combinators! +* On a Linux-based system, the following command was used to globally migrate all uses of the + old combinators to the new ones in the standard library itself. + It *may* be useful when trying to migrate your own code: + ```bash + find . -type f -name "*.agda" -print0 | xargs -0 sed -i -e 's/˘⟨\(.*\)⟩/⟨\1⟨/g' + ``` + USUAL CAVEATS: It has not been widely tested and the standard library developers are not + responsible for the results of this command. It is strongly recommended you back up your + work before you attempt to run it. + +* NOTE: this refactoring may require some extra bracketing around the operator `_⟨_⟩_` from + `Function.Base` if the `_⟨_⟩_` operator is used within the reasoning proof. The symptom + for this is a `Don't know how to parse` error. + ### Other * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index e602932827..390a48d58f 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -76,8 +76,8 @@ opposite-prop {suc n} i with view i ... | ‵fromℕ rewrite toℕ-fromℕ n | n∸n≡0 n = refl ... | ‵inject₁ j = begin suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩ - suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 (toℕ ⊖-monoʳ-≥-≤ (suc n) {suc m} {suc o} (s≤s m≤o) = begin suc n ⊖ suc m ≡⟨ [1+m]⊖[1+n]≡m⊖n n m ⟩ n ⊖ m ≤⟨ ⊖-monoʳ-≥-≤ n m≤o ⟩ - n ⊖ o ≡˘⟨ [1+m]⊖[1+n]≡m⊖n n o ⟩ + n ⊖ o ≡⟨ [1+m]⊖[1+n]≡m⊖n n o ⟨ suc n ⊖ suc o ∎ where open ≤-Reasoning ⊖-monoˡ-≤ : ∀ n → (_⊖ n) Preserves ℕ._≤_ ⟶ _≤_ @@ -759,12 +759,12 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> ⊖-monoˡ-≤ (suc n) {_} {suc o} z≤n = begin zero ⊖ suc n ≤⟨ ⊖-monoʳ-≥-≤ 0 (ℕ.n≤1+n n) ⟩ zero ⊖ n ≤⟨ ⊖-monoˡ-≤ n z≤n ⟩ - o ⊖ n ≡˘⟨ [1+m]⊖[1+n]≡m⊖n o n ⟩ + o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨ suc o ⊖ suc n ∎ where open ≤-Reasoning ⊖-monoˡ-≤ (suc n) {suc m} {suc o} (s≤s m≤o) = begin suc m ⊖ suc n ≡⟨ [1+m]⊖[1+n]≡m⊖n m n ⟩ m ⊖ n ≤⟨ ⊖-monoˡ-≤ n m≤o ⟩ - o ⊖ n ≡˘⟨ [1+m]⊖[1+n]≡m⊖n o n ⟩ + o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨ suc o ⊖ suc n ∎ where open ≤-Reasoning ⊖-monoʳ->-< : ∀ p → (p ⊖_) Preserves ℕ._>_ ⟶ _<_ @@ -777,19 +777,19 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> ⊖-monoʳ->-< (suc p) {suc m} {suc n} (s-< p m_ *-monoˡ-<-neg i@(-[1+ _ ]) {j} {k} j j *-cancelˡ-<-nonPos {i} {j} +0 (+<+ ()) *-cancelˡ-<-nonPos {i} {j} k@(-[1+ _ ]) ki>= pam as) unfold-⊛ fs as = begin fs ⊛ as - ≡˘⟨ concatMap-cong (λ f → P.cong (map f) (concatMap-pure as)) fs ⟩ + ≡⟨ concatMap-cong (λ f → P.cong (map f) (concatMap-pure as)) fs ⟨ concatMap (λ f → map f (concatMap pure as)) fs ≡⟨ concatMap-cong (λ f → map-concatMap f pure as) fs ⟩ concatMap (λ f → concatMap (λ x → pure (f x)) as) fs @@ -224,7 +224,7 @@ module Applicative where right-distributive fs₁ fs₂ xs = begin (fs₁ ∣ fs₂) ⊛ xs ≡⟨ unfold-⊛ (fs₁ ∣ fs₂) xs ⟩ (fs₁ ∣ fs₂ >>= pam xs) ≡⟨ MonadProperties.right-distributive fs₁ fs₂ (pam xs) ⟩ - (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs) ≡˘⟨ P.cong₂ _∣_ (unfold-⊛ fs₁ xs) (unfold-⊛ fs₂ xs) ⟩ + (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs) ≡⟨ P.cong₂ _∣_ (unfold-⊛ fs₁ xs) (unfold-⊛ fs₂ xs) ⟨ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs) ∎ -- _⊛_ does not distribute over _∣_ from the left. @@ -251,7 +251,7 @@ module Applicative where (xs : List A) (f : A → B) (fs : B → List C) → (pam xs f >>= fs) ≡ (xs >>= λ x → fs (f x)) pam-lemma xs f fs = begin - (pam xs f >>= fs) ≡˘⟨ MP.associative xs (pure ∘ f) fs ⟩ + (pam xs f >>= fs) ≡⟨ MP.associative xs (pure ∘ f) fs ⟨ (xs >>= λ x → pure (f x) >>= fs) ≡⟨ MP.cong (refl {x = xs}) (λ x → MP.left-identity (f x) fs) ⟩ (xs >>= λ x → fs (f x)) ∎ @@ -272,7 +272,7 @@ module Applicative where (pam fs _∘′_ >>= pam gs >>= pam xs) ≡⟨ MP.cong (pam-lemma fs _∘′_ (pam gs)) (λ _ → refl) ⟩ ((fs >>= λ f → pam gs (f ∘′_)) >>= pam xs) - ≡˘⟨ MP.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟩ + ≡⟨ MP.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟨ (fs >>= λ f → pam gs (f ∘′_) >>= pam xs) ≡⟨ MP.cong (refl {x = fs}) (λ f → pam-lemma gs (f ∘′_) (pam xs)) ⟩ (fs >>= λ f → gs >>= λ g → pam xs (f ∘′ g)) @@ -282,9 +282,9 @@ module Applicative where (fs >>= λ f → gs >>= λ g → pam (pam xs g) f) ≡⟨ MP.cong (refl {x = fs}) (λ f → MP.associative gs (pam xs) (pure ∘ f)) ⟩ (fs >>= pam (gs >>= pam xs)) - ≡˘⟨ unfold-⊛ fs (gs >>= pam xs) ⟩ + ≡⟨ unfold-⊛ fs (gs >>= pam xs) ⟨ fs ⊛ (gs >>= pam xs) - ≡˘⟨ P.cong (fs ⊛_) (unfold-⊛ gs xs) ⟩ + ≡⟨ P.cong (fs ⊛_) (unfold-⊛ gs xs) ⟨ fs ⊛ (gs ⊛ xs) ∎ @@ -304,5 +304,5 @@ module Applicative where MP.left-identity x (pure ∘ f)) ⟩ (fs >>= λ f → pure (f x)) ≡⟨⟩ (pam fs (_$′ x)) ≡⟨ P.sym $ MP.left-identity (_$′ x) (pam fs) ⟩ - (pure (_$′ x) >>= pam fs) ≡˘⟨ unfold-⊛ (pure (_$′ x)) fs ⟩ + (pure (_$′ x) >>= pam fs) ≡⟨ unfold-⊛ (pure (_$′ x)) fs ⟨ pure (_$′ x) ⊛ fs ∎ diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 78fc03f865..5bd47dc763 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -280,7 +280,7 @@ module _ (f : A → B → C) where cartesianProductWith-distribʳ-++ (x ∷ xs) ys zs = begin prod (x ∷ xs ++ ys) zs ≡⟨⟩ map (f x) zs ++ prod (xs ++ ys) zs ≡⟨ cong (map (f x) zs ++_) (cartesianProductWith-distribʳ-++ xs ys zs) ⟩ - map (f x) zs ++ prod xs zs ++ prod ys zs ≡˘⟨ ++-assoc (map (f x) zs) (prod xs zs) (prod ys zs) ⟩ + map (f x) zs ++ prod xs zs ++ prod ys zs ≡⟨ ++-assoc (map (f x) zs) (prod xs zs) (prod ys zs) ⟨ (map (f x) zs ++ prod xs zs) ++ prod ys zs ≡⟨⟩ prod (x ∷ xs) zs ++ prod ys zs ∎ @@ -590,7 +590,7 @@ map-concatMap f g xs = begin map f (concatMap g xs) ≡⟨⟩ map f (concat (map g xs)) - ≡˘⟨ concat-map (map g xs) ⟩ + ≡⟨ concat-map (map g xs) ⟨ concat (map (map f) (map g xs)) ≡⟨ cong concat {x = map (map f) (map g xs)} diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index a5f6fbec14..31ab6941ac 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -199,7 +199,7 @@ module _ {k} {A B : Set a} {fs gs : List (A → B)} {xs ys} where x ∈ (fs >>= λ f → xs >>= λ x → pure (f x)) ∼⟨ >>=-cong fs≈gs (λ f → >>=-cong xs≈ys λ x → K-refl) ⟩ x ∈ (gs >>= λ g → ys >>= λ y → pure (g y)) - ≡˘⟨ P.cong (x ∈_) (Applicative.unfold-⊛ gs ys) ⟩ + ≡⟨ P.cong (x ∈_) (Applicative.unfold-⊛ gs ys) ⟨ x ∈ (gs ⊛ ys) ∎ where open Related.EquationalReasoning @@ -284,7 +284,7 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl) (xs₂ >>= pure ∘ f)) ≈⟨ >>=-left-distributive fs ⟩ (fs >>= λ f → xs₁ >>= pure ∘ f) ++ - (fs >>= λ f → xs₂ >>= pure ∘ f) ≡˘⟨ P.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟩ + (fs >>= λ f → xs₂ >>= pure ∘ f) ≡⟨ P.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨ (fs ⊛ xs₁) ++ (fs ⊛ xs₂) ∎ where open EqR ([ bag ]-Equality B) @@ -592,7 +592,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ... | zs₁ , zs₂ , p rewrite p = begin x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ - x ∷ (zs₁ ++ zs₂) ↭˘⟨ shift x zs₁ zs₂ ⟩ + x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨ zs₁ ++ x ∷ zs₂ ∎ where open CommutativeMonoid (commutativeMonoid bag A) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index 382b4f4520..c41793d28a 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -78,7 +78,7 @@ module PermutationReasoning where open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) - renaming (∼-go to ↭-go) + renaming (≈-go to ↭-go) open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 1b33a771a0..781de1cc36 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -243,7 +243,7 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl ++-comm [] ys = ↭-sym (++-identityʳ ys) ++-comm (x ∷ xs) ys = begin x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ - x ∷ ys ++ xs ↭˘⟨ shift x ys xs ⟩ + x ∷ ys ++ xs ↭⟨ shift x ys xs ⟨ ys ++ (x ∷ xs) ∎ ++-isMagma : IsMagma {A = List A} _↭_ _++_ @@ -296,7 +296,7 @@ module _ {a} {A : Set a} where shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs shifts xs ys {zs} = begin - xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩ + xs ++ ys ++ zs ↭⟨ ++-assoc xs ys zs ⟨ (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩ (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩ ys ++ xs ++ zs ∎ @@ -330,7 +330,7 @@ drop-∷ = drop-mid [] [] ↭-reverse [] = ↭-refl ↭-reverse (x ∷ xs) = begin reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩ - reverse xs ∷ʳ x ↭˘⟨ ∷↭∷ʳ x (reverse xs) ⟩ + reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨ x ∷ reverse xs ↭⟨ prep x (↭-reverse xs) ⟩ x ∷ xs ∎ where open PermutationReasoning @@ -349,7 +349,7 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where ... | true | rec | _ = prep x rec ... | false | _ | rec = begin y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩ - y ∷ x ∷ xs ++ ys ↭˘⟨ shift y (x ∷ xs) ys ⟩ - (x ∷ xs) ++ y ∷ ys ≡˘⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟩ + y ∷ x ∷ xs ++ ys ↭⟨ shift y (x ∷ xs) ys ⟨ + (x ∷ xs) ++ y ∷ ys ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨ x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index 234993113a..edcf62b6da 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -92,7 +92,7 @@ module PermutationReasoning where open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) - renaming (∼-go to ↭-go) + renaming (≈-go to ↭-go) open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index e09251caf5..3af753e826 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -200,7 +200,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin ++-comm [] ys = ↭-sym (++-identityʳ ys) ++-comm (x ∷ xs) ys = begin x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ - x ∷ ys ++ xs ↭˘⟨ ↭-shift ys xs ⟩ + x ∷ ys ++ xs ↭⟨ ↭-shift ys xs ⟨ ys ++ (x ∷ xs) ∎ -- Structures @@ -262,7 +262,7 @@ inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs shifts xs ys {zs} = begin - xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩ + xs ++ ys ++ zs ↭⟨ ++-assoc xs ys zs ⟨ (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩ (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩ ys ++ xs ++ zs ∎ @@ -297,19 +297,19 @@ dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin ys ≋⟨ ys≋as ⟩ as ↭⟨ as↭bs ⟩ - bs ≋˘⟨ zs≋bs ⟩ + bs ≋⟨ zs≋bs ⟨ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep a≈b as↭bs) [] (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ as ↭⟨ as↭bs ⟩ - bs ≋˘⟨ ≋₂ ⟩ + bs ≋⟨ ≋₂ ⟨ xs ++ v ∷ zs ↭⟨ shift (lemma ≈₁ a≈b ≈₂) xs zs ⟩ x ∷ xs ++ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep v≈w p) (w ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ ws ++ ys ↭⟨ ↭-sym (shift (lemma ≈₂ (≈-sym v≈w) ≈₁) ws ys) ⟩ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩ as ↭⟨ p ⟩ - bs ≋˘⟨ ≋₂ ⟩ + bs ≋⟨ ≋₂ ⟨ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep w≈x p) (w ∷ ws) (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ ws ++ ys ↭⟨ prep (lemma ≈₁ w≈x ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩ @@ -317,12 +317,12 @@ dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈x y≈v p) [] [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ a ∷ as ↭⟨ prep (≈-trans (≈-trans (≈-trans y≈v (≈-sym ≈₂)) ≈₁) v≈x) p ⟩ - b ∷ bs ≋˘⟨ ≋₂ ⟩ + b ∷ bs ≋⟨ ≋₂ ⟨ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ a ∷ as ↭⟨ prep y≈w p ⟩ - _ ∷ bs ≋˘⟨ ≈₂ ∷ tail ≋₂ ⟩ + _ ∷ bs ≋⟨ ≈₂ ∷ tail ≋₂ ⟨ x ∷ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ @@ -455,8 +455,8 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where ... | true | rec | _ = ↭-prep x rec ... | false | _ | rec = begin y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩ - y ∷ x ∷ xs ++ ys ↭˘⟨ ↭-shift (x ∷ xs) ys ⟩ - (x ∷ xs) ++ y ∷ ys ≡˘⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟩ + y ∷ x ∷ xs ++ ys ↭⟨ ↭-shift (x ∷ xs) ys ⟨ + (x ∷ xs) ++ y ∷ ys ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨ x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning @@ -497,7 +497,7 @@ module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin x ∙ (y ∙ foldr _∙_ ε xs) S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ foldr _∙_ ε ys) S.≈˘⟨ assoc x y (foldr _∙_ ε ys) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) S.≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ (x ∙ y) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (comm x y) ⟩ (y ∙ x) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index b88bdfbe95..e356e9eca1 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -686,7 +686,7 @@ module _ {A B : Set ℓ} {P : B → Set p} {f : A → List B} where Any (λ f → Any (P ∘ f) xs) fs ↔⟨ Any-cong (λ _ → Any-cong (λ _ → pure↔) (_ ∎)) (_ ∎) ⟩ Any (λ f → Any (Any P ∘ pure ∘ f) xs) fs ↔⟨ Any-cong (λ _ → >>=↔ ) (_ ∎) ⟩ Any (λ f → Any P (xs >>= pure ∘ f)) fs ↔⟨ >>=↔ ⟩ - Any P (fs >>= λ f → xs >>= λ x → pure (f x)) ≡˘⟨ P.cong (Any P) (Listₑ.Applicative.unfold-⊛ fs xs) ⟩ + Any P (fs >>= λ f → xs >>= λ x → pure (f x)) ≡⟨ P.cong (Any P) (Listₑ.Applicative.unfold-⊛ fs xs) ⟨ Any P (fs ⊛ xs) ∎ where open Related.EquationalReasoning @@ -706,7 +706,7 @@ module _ {A B : Set ℓ} {P : B → Set p} {f : A → List B} where Any (λ x → Any (λ y → P (x , y)) ys) xs ↔⟨ pure↔ ⟩ Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (pure _,_) ↔⟨ ⊛↔ ⟩ Any (λ x, → Any (P ∘ x,) ys) (pure _,_ ⊛ xs) ↔⟨ ⊛↔ ⟩ - Any P (pure _,_ ⊛ xs ⊛ ys) ≡˘⟨ P.cong (Any P ∘′ (_⊛ ys)) (Listₑ.Applicative.unfold-<$> _,_ xs) ⟩ + Any P (pure _,_ ⊛ xs ⊛ ys) ≡⟨ P.cong (Any P ∘′ (_⊛ ys)) (Listₑ.Applicative.unfold-<$> _,_ xs) ⟨ Any P (xs ⊗ ys) ∎ where open Related.EquationalReasoning diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 65ac8005fd..f83bbfc12c 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -156,9 +156,9 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl tail-homo ℕ.zero = refl tail-homo (ℕ.suc ℕ.zero) = refl tail-homo (ℕ.suc (ℕ.suc n)) = begin - tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡˘⟨ tail-suc (fromℕ' n) ⟩ + tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡⟨ tail-suc (fromℕ' n) ⟨ suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩ - fromℕ' (ℕ.suc (n / 2)) ≡˘⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟩ + fromℕ' (ℕ.suc (n / 2)) ≡⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟨ fromℕ' (ℕ.suc (ℕ.suc n) / 2) ∎ fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n @@ -167,7 +167,7 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl split-injective (begin split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ just (n % 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n / 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ - just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ + just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟨ head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ split (fromℕ' (ℕ.suc n)) ∎) where rec-n/2 = fromℕ-helper≡fromℕ' (n / 2) w (ℕₚ.≤-trans (m/n≤m n 2) n≤w) diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index fc6ef422b4..d07d22db47 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -66,9 +66,9 @@ open Specification public nCk≡nC[n∸k] : k ≤ n → n C k ≡ n C (n ∸ k) nCk≡nC[n∸k] {k} {n} k≤n = begin-equality n C k ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟩ - n ! / ((n ∸ k) ! * k !) ≡˘⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟩ - n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡˘⟨ nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟩ + n ! / (k ! * (n ∸ k) !) ≡⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟨ + n ! / ((n ∸ k) ! * k !) ≡⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟨ + n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡⟨ nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟨ n C (n ∸ k) ∎ where instance _ = (n ∸ k) !* k !≢0 @@ -78,9 +78,9 @@ nCk≡nC[n∸k] {k} {n} k≤n = begin-equality nCk≡nPk/k! : k ≤ n → n C k ≡ ((n P k) / k !) {{k !≢0}} nCk≡nPk/k! {k} {n} k≤n = begin-equality n C k ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟩ - n ! / ((n ∸ k) ! * k !) ≡˘⟨ m/n/o≡m/[n*o] (n !) ((n ∸ k) !) (k !) ⟩ - (n ! / (n ∸ k) !) / k ! ≡˘⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟩ + n ! / (k ! * (n ∸ k) !) ≡⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟨ + n ! / ((n ∸ k) ! * k !) ≡⟨ m/n/o≡m/[n*o] (n !) ((n ∸ k) !) (k !) ⟨ + (n ! / (n ∸ k) !) / k ! ≡⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟨ (n P k) / k ! ∎ where instance _ = k !≢0 @@ -128,7 +128,7 @@ module _ {n k} (kn⇒nCk≡0 k>n) ⟩ 0 + n C (suc k) ≡⟨⟩ n C (suc k) ≡⟨ k>n⇒nCk≡0 (mn) ⟩ - 0 ≡˘⟨ k>n⇒nCk≡0 (sn) ⟩ + 0 ≡⟨ k>n⇒nCk≡0 (sn) ⟨ suc n C suc k ∎ {- case k≡n, in which case 1+k≡1+n>n -} ... | tri≈ _ k≡n _ rewrite k≡n = begin-equality n C n + n C (suc n) ≡⟨ cong (n C n +_) (k>n⇒nCk≡0 (n<1+n n)) ⟩ n C n + 0 ≡⟨ +-identityʳ (n C n) ⟩ n C n ≡⟨ nCn≡1 n ⟩ - 1 ≡˘⟨ nCn≡1 (suc n) ⟩ + 1 ≡⟨ nCn≡1 (suc n) ⟨ suc n C suc n ∎ {- case k0 (≢-nonZero⁻¹ o)) (≮⇒≥ n≮o) @@ -333,19 +333,19 @@ m p≮q p≡r p>q = begin f (p ⊓ q) ≡⟨ cong f (p≥q⇒p⊓q≡q (<⇒≤ p>q)) ⟩ - f q ≡˘⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟩ + f q ≡⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟨ f p ⊓ f q ∎ where open ≡-Reasoning @@ -1508,17 +1508,17 @@ mono-<-distrib-⊔ : ∀ {f} → f Preserves _<_ ⟶ _<_ → mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q ... | tri< p p≮q p≡r p>q = begin f (p ⊔ q) ≡⟨ cong f (p≥q⇒p⊔q≡p (<⇒≤ p>q)) ⟩ - f p ≡˘⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟩ + f p ≡⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟨ f p ⊔ f q ∎ where open ≡-Reasoning @@ -1606,7 +1606,7 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl 0≤∣p∣ p@record{} = *≤* (begin (↥ 0ℚ) ℤ.* (↧ ∣ p ∣) ≡⟨ ℤ.*-zeroˡ (↧ ∣ p ∣) ⟩ 0ℤ ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩ - ↥ ∣ p ∣ ≡˘⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟩ + ↥ ∣ p ∣ ≡⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟨ ↥ ∣ p ∣ ℤ.* 1ℤ ∎) where open ℤ.≤-Reasoning diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 9fa358863f..dce11c3f21 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -160,7 +160,7 @@ module ≃-Reasoning = SetoidReasoning ≃-setoid p≃0⇒↥p≡0 : ∀ p → p ≃ 0ℚᵘ → ↥ p ≡ 0ℤ p≃0⇒↥p≡0 p (*≡* eq) = begin - ↥ p ≡˘⟨ ℤ.*-identityʳ (↥ p) ⟩ + ↥ p ≡⟨ ℤ.*-identityʳ (↥ p) ⟨ ↥ p ℤ.* 1ℤ ≡⟨ eq ⟩ 0ℤ ∎ where open ≡-Reasoning @@ -180,14 +180,14 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl -‿cong : Congruent₁ _≃_ (-_) -‿cong {p@record{}} {q@record{}} (*≡* p≡q) = *≡* (begin - ↥(- p) ℤ.* ↧ q ≡˘⟨ ℤ.*-identityˡ (ℤ.- (↥ p) ℤ.* ↧ q) ⟩ - 1ℤ ℤ.* (↥(- p) ℤ.* ↧ q) ≡˘⟨ ℤ.*-assoc 1ℤ (↥ (- p)) (↧ q) ⟩ - (1ℤ ℤ.* ℤ.-(↥ p)) ℤ.* ↧ q ≡˘⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribʳ-* 1ℤ (↥ p)) ⟩ + ↥(- p) ℤ.* ↧ q ≡⟨ ℤ.*-identityˡ (ℤ.- (↥ p) ℤ.* ↧ q) ⟨ + 1ℤ ℤ.* (↥(- p) ℤ.* ↧ q) ≡⟨ ℤ.*-assoc 1ℤ (↥ (- p)) (↧ q) ⟨ + (1ℤ ℤ.* ℤ.-(↥ p)) ℤ.* ↧ q ≡⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribʳ-* 1ℤ (↥ p)) ⟨ ℤ.-(1ℤ ℤ.* ↥ p) ℤ.* ↧ q ≡⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribˡ-* 1ℤ (↥ p)) ⟩ (-1ℤ ℤ.* ↥ p) ℤ.* ↧ q ≡⟨ ℤ.*-assoc ℤ.-1ℤ (↥ p) (↧ q) ⟩ -1ℤ ℤ.* (↥ p ℤ.* ↧ q) ≡⟨ cong (ℤ.-1ℤ ℤ.*_) p≡q ⟩ - -1ℤ ℤ.* (↥ q ℤ.* ↧ p) ≡˘⟨ ℤ.*-assoc ℤ.-1ℤ (↥ q) (↧ p) ⟩ - (-1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡˘⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribˡ-* 1ℤ (↥ q)) ⟩ + -1ℤ ℤ.* (↥ q ℤ.* ↧ p) ≡⟨ ℤ.*-assoc ℤ.-1ℤ (↥ q) (↧ p) ⟨ + (-1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribˡ-* 1ℤ (↥ q)) ⟨ ℤ.-(1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribʳ-* 1ℤ (↥ q)) ⟩ (1ℤ ℤ.* ↥(- q)) ℤ.* ↧ p ≡⟨ ℤ.*-assoc 1ℤ (ℤ.- (↥ q)) (↧ p) ⟩ 1ℤ ℤ.* (↥(- q) ℤ.* ↧ p) ≡⟨ ℤ.*-identityˡ (↥ (- q) ℤ.* ↧ p) ⟩ @@ -196,7 +196,7 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl neg-mono-< : -_ Preserves _<_ ⟶ _>_ neg-mono-< {p@record{}} {q@record{}} (*<* p?_ = flip _