From c1cd94d76e4f50346721a3f3887be2f156f9d446 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 6 Feb 2024 18:32:38 +0000 Subject: [PATCH 1/5] `Data.List.Relation.Relation.Binary.BagAndSetEquality` --- .../Relation/Binary/BagAndSetEquality.agda | 70 +++++++++---------- 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 17af3d8955..389721d4c5 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -15,10 +15,11 @@ open import Data.Empty open import Data.Fin.Base open import Data.List.Base open import Data.List.Effectful using (monad; module Applicative; module MonadProperties) -import Data.List.Properties as LP +import Data.List.Properties as List open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.Any.Properties hiding (++-comm) open import Data.List.Membership.Propositional using (_∈_) +open import Data.List.Membership.Propositional.Properties open import Data.List.Relation.Binary.Subset.Propositional.Properties using (⊆-preorder) open import Data.List.Relation.Binary.Permutation.Propositional @@ -39,13 +40,12 @@ 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) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning +open import Relation.Binary.PropositionalEquality as ≡ + using (_≡_; _≢_; _≗_; refl; module ≡-Reasoning) open import Relation.Binary.Reasoning.Syntax open import Relation.Nullary.Negation using (¬_) -open import Data.List.Membership.Propositional.Properties private variable @@ -93,7 +93,7 @@ bag-=⇒ xs≈ys = ↔⇒ xs≈ys -- "Equational" reasoning for _⊆_ along with an additional relatedness module ⊆-Reasoning {A : Set a} where - private module Base = PreorderReasoning (⊆-preorder A) + private module Base = ≲-Reasoning (⊆-preorder A) open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) @@ -140,10 +140,10 @@ module _ {k} {f g : A → B} {xs ys} where helper : ∀ y → x ≡ f y ↔ x ≡ g y helper y = mk↔ₛ′ - (λ x≡fy → P.trans x≡fy ( f≗g y)) - (λ x≡gy → P.trans x≡gy (P.sym $ f≗g y)) - (λ { P.refl → P.trans-symˡ (f≗g y) }) - λ { P.refl → P.trans-symʳ (f≗g y) } + (λ x≡fy → ≡.trans x≡fy ( f≗g y)) + (λ x≡gy → ≡.trans x≡gy (≡.sym $ f≗g y)) + (λ { ≡.refl → ≡.trans-symˡ (f≗g y) }) + λ { ≡.refl → ≡.trans-symʳ (f≗g y) } ------------------------------------------------------------------------ -- _++_ @@ -195,11 +195,11 @@ module _ {k} {A B : Set a} {fs gs : List (A → B)} {xs ys} where ⊛-cong : fs ∼[ k ] gs → xs ∼[ k ] ys → (fs ⊛ xs) ∼[ k ] (gs ⊛ ys) ⊛-cong fs≈gs xs≈ys {x} = begin x ∈ (fs ⊛ xs) - ≡⟨ P.cong (x ∈_) (Applicative.unfold-⊛ fs xs) ⟩ + ≡⟨ ≡.cong (x ∈_) (Applicative.unfold-⊛ fs xs) ⟩ 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) ⟨ + ≡⟨ ≡.cong (x ∈_) (Applicative.unfold-⊛ gs ys) ⟨ x ∈ (gs ⊛ ys) ∎ where open Related.EquationalReasoning @@ -232,7 +232,7 @@ commutativeMonoid {a} k A = record ; ∙-cong = ++-cong } ; assoc = λ xs ys zs → - Eq.reflexive (LP.++-assoc xs ys zs) + Eq.reflexive (List.++-assoc xs ys zs) } ; identityˡ = λ xs → K-refl ; comm = λ xs ys → ↔⇒ (++↔++ xs ys) @@ -284,10 +284,10 @@ 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) ≡⟨ ≡.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨ (fs ⊛ xs₁) ++ (fs ⊛ xs₂) ∎ - where open EqR ([ bag ]-Equality B) + where open ≈-Reasoning ([ bag ]-Equality B) private @@ -397,7 +397,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = to (Fin-length-cong xs≈ys) (index-of p) ∎ where - open P.≡-Reasoning + open ≡-Reasoning open Inverse lemma : @@ -423,11 +423,11 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = index-of (Inverse.to xs≈ys q) index-equality-preserved {p = p} {q} xs≈ys eq = index-of (Inverse.to xs≈ys p) ≡⟨ index-of-commutes xs≈ys p ⟩ - Inverse.to (Fin-length-cong xs≈ys) (index-of p) ≡⟨ P.cong (Inverse.to (Fin-length-cong xs≈ys)) eq ⟩ - Inverse.to (Fin-length-cong xs≈ys) (index-of q) ≡⟨ P.sym $ index-of-commutes xs≈ys q ⟩ + Inverse.to (Fin-length-cong xs≈ys) (index-of p) ≡⟨ ≡.cong (Inverse.to (Fin-length-cong xs≈ys)) eq ⟩ + Inverse.to (Fin-length-cong xs≈ys) (index-of q) ≡⟨ ≡.sym $ index-of-commutes xs≈ys q ⟩ index-of (Inverse.to xs≈ys q) ∎ where - open P.≡-Reasoning + open ≡-Reasoning -- The old inspect idiom. @@ -487,17 +487,17 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ∀ b → g (from f) from-hyp (g (to f) to-hyp b) ≡ b g∘g f to-hyp from-hyp b = g∘g′ where - open P.≡-Reasoning + open ≡-Reasoning g∘g′ : g (from f) from-hyp (g (to f) to-hyp b) ≡ b g∘g′ with inspect (to f (inj₂ b)) g∘g′ | inj₂ c , eq₁ with inspect (from f (inj₂ c)) ... | inj₂ b′ , eq₂ = inj₂-injective ( - inj₂ b′ ≡⟨ P.sym eq₂ ⟩ + inj₂ b′ ≡⟨ ≡.sym eq₂ ⟩ from f (inj₂ c) ≡⟨ to-from f eq₁ ⟩ inj₂ b ∎) ... | inj₁ a , eq₂ with - inj₁ a ≡⟨ P.sym eq₂ ⟩ + inj₁ a ≡⟨ ≡.sym eq₂ ⟩ from f (inj₂ c) ≡⟨ to-from f eq₁ ⟩ inj₂ b ∎ ... | () @@ -505,7 +505,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = g∘g′ | inj₁ a , eq₁ | inj₁ a′ , eq₂ = ⊥-elim $ to-hyp eq₁ eq₂ g∘g′ | inj₁ a , eq₁ | inj₂ c , eq₂ with inspect (from f (inj₂ c)) g∘g′ | inj₁ a , eq₁ | inj₂ c , eq₂ | inj₂ b′ , eq₃ with - inj₁ a ≡⟨ P.sym (to-from f eq₂) ⟩ + inj₁ a ≡⟨ ≡.sym (to-from f eq₂) ⟩ from f (inj₂ c) ≡⟨ eq₃ ⟩ inj₂ b′ ∎ ... | () @@ -513,12 +513,12 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = g∘g′ | inj₁ a , eq₁ | inj₂ c , eq₂ | inj₁ a′ , eq₃ | inj₁ a″ , eq₄ = ⊥-elim $ from-hyp eq₃ eq₄ g∘g′ | inj₁ a , eq₁ | inj₂ c , eq₂ | inj₁ a′ , eq₃ | inj₂ b′ , eq₄ = inj₂-injective ( let lemma = - inj₁ a′ ≡⟨ P.sym eq₃ ⟩ + inj₁ a′ ≡⟨ ≡.sym eq₃ ⟩ from f (inj₂ c) ≡⟨ to-from f eq₂ ⟩ inj₁ a ∎ in - inj₂ b′ ≡⟨ P.sym eq₄ ⟩ - from f (inj₁ a′) ≡⟨ P.cong (from f ∘ inj₁) $ inj₁-injective lemma ⟩ + inj₂ b′ ≡⟨ ≡.sym eq₄ ⟩ + from f (inj₁ a′) ≡⟨ ≡.cong (from f ∘ inj₁) $ inj₁-injective lemma ⟩ from f (inj₁ a) ≡⟨ to-from f eq₁ ⟩ inj₂ b ∎) @@ -541,21 +541,21 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = lemma {xs} inv {b = z∈xs} {a = p} {a′ = q} hyp₁ hyp₂ with zero ≡⟨⟩ index-of {xs = x ∷ xs} (here p) ≡⟨⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p) ≡⟨ P.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ P.sym $ + index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₁ p) ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ ≡.sym $ to-from (∼→⊎↔⊎ inv) {x = inj₁ p} hyp₂ ⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q)) ≡⟨ P.cong index-of $ + index-of {xs = x ∷ xs} (to (∷↔ _) $ (from (∼→⊎↔⊎ inv) $ inj₁ q)) ≡⟨ ≡.cong index-of $ strictlyInverseˡ (∷↔ _) (from inv (here q)) ⟩ index-of {xs = x ∷ xs} (to (SK-sym inv) $ here q) ≡⟨ index-equality-preserved (SK-sym inv) refl ⟩ - index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p) ≡⟨ P.cong index-of $ P.sym $ + index-of {xs = x ∷ xs} (to (SK-sym inv) $ here p) ≡⟨ ≡.cong index-of $ ≡.sym $ strictlyInverseˡ (∷↔ _) (from inv (here p)) ⟩ - index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p)) ≡⟨ P.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ + index-of {xs = x ∷ xs} (to (∷↔ _) (from (∼→⊎↔⊎ inv) $ inj₁ p)) ≡⟨ ≡.cong (index-of ∘ (to (∷↔ (_ ≡_)))) $ to-from (∼→⊎↔⊎ inv) {x = inj₂ z∈xs} hyp₁ ⟩ index-of {xs = x ∷ xs} (to (∷↔ _) $ inj₂ z∈xs) ≡⟨⟩ index-of {xs = x ∷ xs} (there z∈xs) ≡⟨⟩ suc (index-of {xs = xs} z∈xs) ∎ where open Inverse - open P.≡-Reasoning + open ≡-Reasoning ... | () ------------------------------------------------------------------------ @@ -573,10 +573,10 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = from∘to : ∀ {xs ys} (p : xs ↭ ys) (q : v ∈ xs) → from p (to p q) ≡ q from∘to refl v∈xs = refl from∘to (prep _ _) (here refl) = refl - from∘to (prep _ p) (there v∈xs) = P.cong there (from∘to p v∈xs) + from∘to (prep _ p) (there v∈xs) = ≡.cong there (from∘to p v∈xs) from∘to (swap x y p) (here refl) = refl from∘to (swap x y p) (there (here refl)) = refl - from∘to (swap x y p) (there (there v∈xs)) = P.cong (there ∘ there) (from∘to p v∈xs) + from∘to (swap x y p) (there (there v∈xs)) = ≡.cong (there ∘ there) (from∘to p v∈xs) from∘to (trans p₁ p₂) v∈xs rewrite from∘to p₂ (Any-resp-↭ p₁ v∈xs) | from∘to p₁ v∈xs = refl @@ -588,7 +588,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ∼bag⇒↭ : _∼[ bag ]_ ⇒ _↭_ {A = A} ∼bag⇒↭ {A = A} {[]} eq with empty-unique (↔-sym eq) ... | refl = refl -∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here P.refl)) +∼bag⇒↭ {A = A} {x ∷ xs} eq with ∈-∃++ (Inverse.to (eq {x}) (here ≡.refl)) ... | zs₁ , zs₂ , p rewrite p = begin x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ From 3527b2949c840cd320ee358882167a349021ce27 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 6 Feb 2024 18:33:24 +0000 Subject: [PATCH 2/5] `Relation.Binary.Reasoning.*` --- src/Relation/Binary/Reasoning/Base/Apartness.agda | 6 +++--- src/Relation/Binary/Reasoning/Base/Double.agda | 6 +++--- src/Relation/Binary/Reasoning/Base/Partial.agda | 2 +- src/Relation/Binary/Reasoning/Base/Single.agda | 4 ++-- src/Relation/Binary/Reasoning/Base/Triple.agda | 8 ++++---- src/Relation/Binary/Reasoning/MultiSetoid.agda | 4 ++-- src/Relation/Binary/Reasoning/Syntax.agda | 6 +++--- 7 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda index 3d4d72f2c8..22eee2d505 100644 --- a/src/Relation/Binary/Reasoning/Base/Apartness.agda +++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda @@ -13,7 +13,7 @@ open import Relation.Nullary.Decidable using (Dec; yes; no) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Transitive; Symmetric; Trans) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Reasoning.Syntax @@ -38,8 +38,8 @@ data _IsRelatedTo_ (x y : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where ≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_ ≡-go x≡y nothing = nothing -≡-go x≡y (apartness y#z) = apartness (case x≡y of λ where P.refl → y#z) -≡-go x≡y (equals y≈z) = equals (case x≡y of λ where P.refl → y≈z) +≡-go x≡y (apartness y#z) = apartness (case x≡y of λ where ≡.refl → y#z) +≡-go x≡y (equals y≈z) = equals (case x≡y of λ where ≡.refl → y≈z) ≈-go : Trans _≈_ _IsRelatedTo_ _IsRelatedTo_ ≈-go x≈y nothing = nothing diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda index 6fa901d573..b5fd9f66e4 100644 --- a/src/Relation/Binary/Reasoning/Base/Double.agda +++ b/src/Relation/Binary/Reasoning/Base/Double.agda @@ -16,7 +16,7 @@ open import Relation.Nullary.Decidable.Core using (Dec; yes; no) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.Structures using (IsPreorder) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Reasoning.Syntax @@ -40,8 +40,8 @@ start (equals x≈y) = reflexive x≈y start (nonstrict x≲y) = x≲y ≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_ -≡-go x≡y (equals y≈z) = equals (case x≡y of λ where P.refl → y≈z) -≡-go x≡y (nonstrict y≤z) = nonstrict (case x≡y of λ where P.refl → y≤z) +≡-go x≡y (equals y≈z) = equals (case x≡y of λ where ≡.refl → y≈z) +≡-go x≡y (nonstrict y≤z) = nonstrict (case x≡y of λ where ≡.refl → y≤z) ≲-go : Trans _≲_ _IsRelatedTo_ _IsRelatedTo_ ≲-go x≲y (equals y≈z) = nonstrict (∼-respʳ-≈ y≈z x≲y) diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index bd1fcd8693..3d24edf501 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -11,7 +11,7 @@ open import Level using (_⊔_) open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Nullary.Decidable using (Dec; yes; no) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Reasoning.Syntax diff --git a/src/Relation/Binary/Reasoning/Base/Single.agda b/src/Relation/Binary/Reasoning/Base/Single.agda index ccbf63dda3..2f34ee8525 100644 --- a/src/Relation/Binary/Reasoning/Base/Single.agda +++ b/src/Relation/Binary/Reasoning/Base/Single.agda @@ -10,7 +10,7 @@ open import Level using (_⊔_) open import Function.Base using (case_of_) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Definitions using (Reflexive; Transitive; Trans) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Reasoning.Syntax module Relation.Binary.Reasoning.Base.Single @@ -36,7 +36,7 @@ start (relTo x∼y) = x∼y ∼-go x∼y (relTo y∼z) = relTo (trans x∼y y∼z) ≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_ -≡-go x≡y (relTo y∼z) = relTo (case x≡y of λ where P.refl → y∼z) +≡-go x≡y (relTo y∼z) = relTo (case x≡y of λ where ≡.refl → y∼z) stop : Reflexive _IsRelatedTo_ stop = relTo refl diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda index 460115eff9..6afb937497 100644 --- a/src/Relation/Binary/Reasoning/Base/Triple.agda +++ b/src/Relation/Binary/Reasoning/Base/Triple.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Structures using (IsPreorder) open import Relation.Binary.Definitions using (Transitive; _Respects₂_; Reflexive; Trans; Irreflexive; Asymmetric) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Reasoning.Syntax module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} @@ -48,9 +48,9 @@ start (nonstrict x≤y) = x≤y start (strict x Date: Tue, 6 Feb 2024 18:53:16 +0000 Subject: [PATCH 3/5] preorder reasoning --- src/Codata/Musical/Colist.agda | 8 ++--- src/Data/Integer/Divisibility/Signed.agda | 35 +++++++++---------- .../Subset/Propositional/Properties.agda | 2 +- .../Binary/Subset/Setoid/Properties.agda | 4 +-- src/Data/Nat/Divisibility.agda | 4 +-- .../ReflexiveTransitive/Properties.agda | 12 +++---- 6 files changed, 32 insertions(+), 33 deletions(-) diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index 3699ef64be..18d250f566 100644 --- a/src/Codata/Musical/Colist.agda +++ b/src/Codata/Musical/Colist.agda @@ -31,8 +31,8 @@ open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Poset; Setoid; Preorder) open import Relation.Binary.Definitions using (Transitive; Antisymmetric) import Relation.Binary.Construct.FromRel as Ind -import Relation.Binary.Reasoning.Preorder as PreR -import Relation.Binary.Reasoning.PartialOrder as POR +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning +import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning open import Relation.Binary.PropositionalEquality as P using (_≡_) open import Relation.Binary.Reasoning.Syntax open import Relation.Nullary.Reflects using (invert) @@ -164,7 +164,7 @@ Any-∈ {P = P} = mk↔ₛ′ antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂) module ⊑-Reasoning {a} {A : Set a} where - private module Base = POR (⊑-Poset A) + private module Base = ≤-Reasoning (⊑-Poset A) open Base public hiding (step-<; step-≤) @@ -188,7 +188,7 @@ module ⊑-Reasoning {a} {A : Set a} where -- ys ≡⟨ ys≡zs ⟩ -- zs ∎ module ⊆-Reasoning {A : Set a} where - private module Base = PreR (⊆-Preorder A) + private module Base = ≲-Reasoning (⊆-Preorder A) open Base public hiding (step-≲; step-∼) diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda index 5149871534..2861cbf7d8 100644 --- a/src/Data/Integer/Divisibility/Signed.agda +++ b/src/Data/Integer/Divisibility/Signed.agda @@ -18,8 +18,8 @@ import Data.Nat.Base as ℕ import Data.Nat.Divisibility as ℕ import Data.Nat.Coprimality as ℕ import Data.Nat.Properties as ℕ -import Data.Sign as S -import Data.Sign.Properties as SProp +import Data.Sign as Sign +import Data.Sign.Properties as Sign open import Level open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_) open import Relation.Binary.Bundles using (Preorder) @@ -27,9 +27,8 @@ open import Relation.Binary.Structures using (IsPreorder) open import Relation.Binary.Definitions using (Reflexive; Transitive; Decidable) 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 +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning +open import Relation.Nullary.Decidable as Dec using (yes; no) open import Relation.Binary.Reasoning.Syntax ------------------------------------------------------------------------ @@ -50,19 +49,19 @@ open _∣_ using (quotient) public ∣ᵤ⇒∣ {k} {i} (divides 0 eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq) ∣ᵤ⇒∣ {k} {i} (divides q@(ℕ.suc _) eq) with k ≟ +0 ... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q))) -... | no neq = divides (sign i S.* sign k ◃ q) (◃-cong sign-eq abs-eq) +... | no neq = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq) where - ikq = sign i S.* sign k ◃ q + ikq = sign i Sign.* sign k ◃ q *-nonZero : ∀ m n .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} → ℕ.NonZero (m ℕ.* n) *-nonZero (ℕ.suc _) (ℕ.suc _) = _ ◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) - ◃-nonZero S.- (ℕ.suc _) = _ - ◃-nonZero S.+ (ℕ.suc _) = _ + ◃-nonZero Sign.- (ℕ.suc _) = _ + ◃-nonZero Sign.+ (ℕ.suc _) = _ ikq≢0 : NonZero ikq - ikq≢0 = ◃-nonZero (sign i S.* sign k) q + ikq≢0 = ◃-nonZero (sign i Sign.* sign k) q instance ikq*∣k∣≢0 : ℕ.NonZero (∣ ikq ∣ ℕ.* ∣ k ∣) @@ -70,18 +69,18 @@ open _∣_ using (quotient) public sign-eq : sign i ≡ sign (ikq * k) sign-eq = sym $ begin - sign (ikq * k) ≡⟨ sign-◃ (sign ikq S.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩ - sign ikq S.* sign k ≡⟨ cong (S._* sign k) (sign-◃ (sign i S.* sign k) q) ⟩ - (sign i S.* sign k) S.* sign k ≡⟨ SProp.*-assoc (sign i) (sign k) (sign k) ⟩ - sign i S.* (sign k S.* sign k) ≡⟨ cong (sign i S.*_) (SProp.s*s≡+ (sign k)) ⟩ - sign i S.* S.+ ≡⟨ SProp.*-identityʳ (sign i) ⟩ + sign (ikq * k) ≡⟨ sign-◃ (sign ikq Sign.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩ + sign ikq Sign.* sign k ≡⟨ cong (Sign._* sign k) (sign-◃ (sign i Sign.* sign k) q) ⟩ + (sign i Sign.* sign k) Sign.* sign k ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩ + sign i Sign.* (sign k Sign.* sign k) ≡⟨ cong (sign i Sign.*_) (Sign.s*s≡+ (sign k)) ⟩ + sign i Sign.* Sign.+ ≡⟨ Sign.*-identityʳ (sign i) ⟩ sign i ∎ where open ≡-Reasoning abs-eq : ∣ i ∣ ≡ ∣ ikq * k ∣ abs-eq = sym $ begin ∣ ikq * k ∣ ≡⟨ ∣i*j∣≡∣i∣*∣j∣ ikq k ⟩ - ∣ ikq ∣ ℕ.* ∣ k ∣ ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ (sign i S.* sign k) q) ⟩ + ∣ ikq ∣ ℕ.* ∣ k ∣ ≡⟨ cong (ℕ._* ∣ k ∣) (abs-◃ (sign i Sign.* sign k) q) ⟩ q ℕ.* ∣ k ∣ ≡⟨ sym eq ⟩ ∣ i ∣ ∎ where open ≡-Reasoning @@ -119,7 +118,7 @@ open _∣_ using (quotient) public -- Divisibility reasoning module ∣-Reasoning where - private module Base = PreorderReasoning ∣-preorder + private module Base = ≲-Reasoning ∣-preorder open Base public hiding (step-≲; step-∼; step-≈; step-≈˘) @@ -133,7 +132,7 @@ module ∣-Reasoning where infix 4 _∣?_ _∣?_ : Decidable _∣_ -k ∣? m = DEC.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣) +k ∣? m = Dec.map′ ∣ᵤ⇒∣ ∣⇒∣ᵤ (∣ k ∣ ℕ.∣? ∣ m ∣) 0∣⇒≡0 : ∀ {m} → 0ℤ ∣ m → m ≡ 0ℤ 0∣⇒≡0 0|m = ∣i∣≡0⇒i≡0 (ℕ.0∣⇒≡0 (∣⇒∣ᵤ 0|m)) diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index 71313d087e..7b498f2a45 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -38,7 +38,7 @@ open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Bundles using (Preorder) open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning) -import Relation.Binary.Reasoning.Preorder as PreorderReasoning +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning private open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ}) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 0c344758b7..bc1a693a2f 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -31,7 +31,7 @@ open import Relation.Binary.Definitions using (Reflexive; Transitive; _Respectsʳ_; _Respectsˡ_; _Respects_) open import Relation.Binary.Bundles using (Setoid; Preorder) open import Relation.Binary.Structures using (IsPreorder) -import Relation.Binary.Reasoning.Preorder as PreorderReasoning +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning open import Relation.Binary.Reasoning.Syntax open Setoid using (Carrier) @@ -115,7 +115,7 @@ module _ (S : Setoid a ℓ) where module ⊆-Reasoning (S : Setoid a ℓ) where open Membership S using (_∈_) - private module Base = PreorderReasoning (⊆-preorder S) + private module Base = ≲-Reasoning (⊆-preorder S) open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index f980291cc4..c5d42a2c90 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -23,7 +23,7 @@ open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) open import Relation.Binary.Definitions using (Reflexive; Transitive; Antisymmetric; Decidable) -import Relation.Binary.Reasoning.Preorder as PreorderReasoning +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; sym; cong; subst) open import Relation.Binary.Reasoning.Syntax @@ -151,7 +151,7 @@ n@(suc _) ∣? m = Dec.map (m%n≡0⇔n∣m m n) (m % n ≟ 0) -- A reasoning module for the _∣_ relation module ∣-Reasoning where - private module Base = PreorderReasoning ∣-preorder + private module Base = ≲-Reasoning ∣-preorder open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda index a78d14938b..a68071d25e 100644 --- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda @@ -14,10 +14,10 @@ open import Relation.Binary.Bundles using (Preorder) open import Relation.Binary.Structures using (IsPreorder) open import Relation.Binary.Definitions using (Transitive; Reflexive) open import Relation.Binary.Construct.Closure.ReflexiveTransitive -open import Relation.Binary.PropositionalEquality.Core as PropEq +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; sym; cong; cong₂) -import Relation.Binary.PropositionalEquality.Properties as PropEq -import Relation.Binary.Reasoning.Preorder as PreorderReasoning +import Relation.Binary.PropositionalEquality.Properties as ≡ +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning open import Relation.Binary.Reasoning.Syntax ------------------------------------------------------------------------ @@ -82,7 +82,7 @@ fold-◅◅ P _⊕_ ∅ left-unit assoc (x ◅ xs) ys = begin fold-◅◅ P _⊕_ ∅ left-unit assoc xs ys ⟩ (x ⊕ (fold P _⊕_ ∅ xs ⊕ fold P _⊕_ ∅ ys)) ≡⟨ sym (assoc x _ _) ⟩ ((x ⊕ fold P _⊕_ ∅ xs) ⊕ fold P _⊕_ ∅ ys) ∎ - where open PropEq.≡-Reasoning + where open ≡.≡-Reasoning ------------------------------------------------------------------------ -- Relational properties @@ -97,7 +97,7 @@ module _ {i t} {I : Set i} (T : Rel I t) where isPreorder : IsPreorder _≡_ (Star T) isPreorder = record - { isEquivalence = PropEq.isEquivalence + { isEquivalence = ≡.isEquivalence ; reflexive = reflexive ; trans = trans } @@ -113,7 +113,7 @@ module _ {i t} {I : Set i} (T : Rel I t) where -- Preorder reasoning for Star module StarReasoning {i t} {I : Set i} (T : Rel I t) where - private module Base = PreorderReasoning (preorder T) + private module Base = ≲-Reasoning (preorder T) open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) From 8e0a2b4d30280cdd4374ad000614e434ff8bd67f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 6 Feb 2024 19:37:47 +0000 Subject: [PATCH 4/5] setoid reasoning --- .../Properties/HeytingCommutativeRing.agda | 8 ++++---- src/Algebra/Construct/LexProduct.agda | 2 +- src/Algebra/Construct/LiftedChoice.agda | 4 ++-- .../Lattice/Morphism/LatticeMonomorphism.agda | 4 ++-- src/Algebra/Module/Bundles.agda | 4 ++-- src/Algebra/Module/Consequences.agda | 4 ++-- src/Algebra/Morphism.agda | 4 ++-- src/Algebra/Morphism/Consequences.agda | 6 +++--- src/Algebra/Morphism/GroupMonomorphism.agda | 6 +++--- src/Algebra/Morphism/MagmaMonomorphism.agda | 4 ++-- src/Algebra/Morphism/MonoidMonomorphism.agda | 4 ++-- src/Algebra/Morphism/RingMonomorphism.agda | 4 ++-- .../CommutativeSemigroup/Divisibility.agda | 4 ++-- src/Algebra/Solver/CommutativeMonoid.agda | 8 ++++---- .../Solver/IdempotentCommutativeMonoid.agda | 8 ++++---- src/Data/List/Properties.agda | 4 ++-- .../List/Relation/Binary/Permutation/Setoid.agda | 4 ++-- src/Data/Rational/Unnormalised/Properties.agda | 4 ++-- src/Function/Properties/Bijection.agda | 4 ++-- src/Function/Properties/Equivalence.agda | 4 ++-- src/Function/Properties/Injection.agda | 2 -- src/Function/Properties/Inverse.agda | 10 +++++----- src/Function/Properties/Surjection.agda | 8 ++++---- .../Binary/Construct/NaturalOrder/Left.agda | 14 +++++++------- .../Binary/Construct/NaturalOrder/Right.agda | 12 ++++++------ .../Binary/Lattice/Properties/HeytingAlgebra.agda | 14 +++++++------- .../Binary/Lattice/Properties/Lattice.agda | 14 +++++++------- src/Relation/Binary/Reasoning/PartialSetoid.agda | 6 +++--- src/Relation/Binary/Reflection.agda | 8 ++++---- src/Tactic/MonoidSolver.agda | 4 ++-- 30 files changed, 92 insertions(+), 94 deletions(-) diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda index 868224bf0c..d8b3ffcdfd 100644 --- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda +++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda @@ -21,7 +21,7 @@ open CommutativeRing commutativeRing using (ring; *-commutativeMonoid) open import Algebra.Properties.Ring ring using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive) open import Relation.Binary.Definitions using (Symmetric) -import Relation.Binary.Reasoning.Setoid as ReasonSetoid +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid private variable @@ -50,7 +50,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0) helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1) = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1) where - open ReasonSetoid setoid + open ≈-Reasoning setoid y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1# y⁻¹*x⁻¹*x*y≈1 = begin @@ -67,7 +67,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0) #-sym : Symmetric _#_ #-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1) where - open ReasonSetoid setoid + open ≈-Reasoning setoid InvX-Y : Invertible _≈_ 1# _*_ (x - y) InvX-Y = #⇒invertible x#y @@ -96,7 +96,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0) helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#) = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1) where - open ReasonSetoid setoid + open ≈-Reasoning setoid x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1# x-z⁻¹*y-z≈1 = begin diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda index e4d51ff9ed..e2f5825824 100644 --- a/src/Algebra/Construct/LexProduct.agda +++ b/src/Algebra/Construct/LexProduct.agda @@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (¬_; does; yes; no) open import Relation.Nullary.Negation using (contradiction; contradiction₂) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Construct.LexProduct {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄) diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda index f53eecc7f1..9b141f8f7e 100644 --- a/src/Algebra/Construct/LiftedChoice.agda +++ b/src/Algebra/Construct/LiftedChoice.agda @@ -20,7 +20,7 @@ open import Level using (Level; _⊔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) open import Relation.Unary using (Pred) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable @@ -46,7 +46,7 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B} private module M = IsSelectiveMagma ∙-isSelectiveMagma open M hiding (sel; isMagma) - open EqReasoning setoid + open ≈-Reasoning setoid module _ (f : A → B) where diff --git a/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda index 9eb1d4da24..9e16a46c4a 100644 --- a/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda +++ b/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda @@ -18,7 +18,7 @@ import Algebra.Lattice.Properties.Lattice as LatticeProperties open import Data.Product.Base using (_,_; map) open import Relation.Binary.Bundles using (Setoid) import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Lattice.Morphism.LatticeMonomorphism {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧} @@ -73,7 +73,7 @@ module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where setoid : Setoid b ℓ₂ setoid = record { isEquivalence = isEquivalence } - open SetoidReasoning setoid + open ≈-Reasoning setoid ∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_ ∨-absorbs-∧ x y = injective (begin diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index 56b01fcf97..33e6bfa731 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -37,7 +37,7 @@ open import Function.Base open import Level open import Relation.Binary.Core using (Rel) open import Relation.Nullary using (¬_) -import Relation.Binary.Reasoning.Setoid as SetR +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable @@ -364,7 +364,7 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm ; rawBisemimodule; _≉ᴹ_ ) - open SetR ≈ᴹ-setoid + open ≈-Reasoning ≈ᴹ-setoid *ₗ-comm : L.Commutative _*ₗ_ *ₗ-comm x y m = begin diff --git a/src/Algebra/Module/Consequences.agda b/src/Algebra/Module/Consequences.agda index 9acd6d6413..2ee2c98d7e 100644 --- a/src/Algebra/Module/Consequences.agda +++ b/src/Algebra/Module/Consequences.agda @@ -16,7 +16,7 @@ open import Function.Base using (flip) open import Level using (Level) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.Reasoning.Setoid as Rea +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable @@ -27,7 +27,7 @@ private module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where open Setoid S - open Rea S + open ≈-Reasoning S open Defs _≈ᴬ_ private diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda index 1bba00bab2..45b7a46a1d 100644 --- a/src/Algebra/Morphism.agda +++ b/src/Algebra/Morphism.agda @@ -14,7 +14,7 @@ import Algebra.Properties.Group as GroupP open import Function.Base open import Level open import Relation.Binary.Core using (Rel; _Preserves_⟶_) -import Relation.Binary.Reasoning.Setoid as EqR +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable @@ -137,7 +137,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂} open IsMonoidMorphism mn-homo public ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹ - ⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin + ⁻¹-homo x = let open ≈-Reasoning T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩ ⟦ x F.⁻¹ F.∙ x ⟧ ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩ ⟦ F.ε ⟧ ≈⟨ ε-homo ⟩ diff --git a/src/Algebra/Morphism/Consequences.agda b/src/Algebra/Morphism/Consequences.agda index e297a8dbc9..b451a87088 100644 --- a/src/Algebra/Morphism/Consequences.agda +++ b/src/Algebra/Morphism/Consequences.agda @@ -13,7 +13,7 @@ open import Algebra.Morphism.Definitions open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_) open import Function.Definitions -import Relation.Binary.Reasoning.Setoid as EqR +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- If f and g are mutually inverse maps between A and B, g is congruent, @@ -34,7 +34,7 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where g (f (g x) ∙₂ f (g y)) ≈⟨ g-cong (homo (g x) (g y)) ⟨ g (f (g x ∙₁ g y)) ≈⟨ invʳ M₂.refl ⟩ g x ∙₁ g y ∎ - where open EqR M₁.setoid + where open ≈-Reasoning M₁.setoid homomorphic₂-inj : ∀ {f g} → Injective _≈₁_ _≈₂_ f → Inverseˡ _≈₁_ _≈₂_ f g → @@ -45,4 +45,4 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where x ∙₂ y ≈⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟨ f (g x) ∙₂ f (g y) ≈⟨ homo (g x) (g y) ⟨ f (g x ∙₁ g y) ∎) - where open EqR M₂.setoid + where open ≈-Reasoning M₂.setoid diff --git a/src/Algebra/Morphism/GroupMonomorphism.agda b/src/Algebra/Morphism/GroupMonomorphism.agda index 51cdcbafe7..4b3349d141 100644 --- a/src/Algebra/Morphism/GroupMonomorphism.agda +++ b/src/Algebra/Morphism/GroupMonomorphism.agda @@ -27,7 +27,7 @@ open RawGroup G₂ renaming open import Algebra.Definitions open import Algebra.Structures open import Data.Product.Base using (_,_) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- Re-export all properties of monoid monomorphisms @@ -41,7 +41,7 @@ open import Algebra.Morphism.MonoidMonomorphism module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong) - open SetoidReasoning setoid + open ≈-Reasoning setoid inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁ _∙_ inverseˡ invˡ x = injective (begin @@ -72,7 +72,7 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where module _ (◦-isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂) where open IsAbelianGroup ◦-isAbelianGroup renaming (∙-cong to ◦-cong; ⁻¹-cong to ⁻¹₂-cong) - open SetoidReasoning setoid + open ≈-Reasoning setoid ⁻¹-distrib-∙ : (∀ x y → (x ◦ y) ⁻¹₂ ≈₂ (x ⁻¹₂) ◦ (y ⁻¹₂)) → (∀ x y → (x ∙ y) ⁻¹₁ ≈₁ (x ⁻¹₁) ∙ (y ⁻¹₁)) ⁻¹-distrib-∙ ⁻¹-distrib-∙ x y = injective (begin diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda index 87027ba5e1..fbe08a5861 100644 --- a/src/Algebra/Morphism/MagmaMonomorphism.agda +++ b/src/Algebra/Morphism/MagmaMonomorphism.agda @@ -27,7 +27,7 @@ open import Algebra.Structures open import Algebra.Definitions open import Data.Product.Base using (map) open import Data.Sum.Base using (inj₁; inj₂) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism ------------------------------------------------------------------------ @@ -36,7 +36,7 @@ import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong) - open SetoidReasoning setoid + open ≈-Reasoning setoid cong : Congruent₂ _≈₁_ _∙_ cong {x} {y} {u} {v} x≈y u≈v = injective (begin diff --git a/src/Algebra/Morphism/MonoidMonomorphism.agda b/src/Algebra/Morphism/MonoidMonomorphism.agda index bfb412302e..1b918295af 100644 --- a/src/Algebra/Morphism/MonoidMonomorphism.agda +++ b/src/Algebra/Morphism/MonoidMonomorphism.agda @@ -25,7 +25,7 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; open import Algebra.Definitions open import Algebra.Structures open import Data.Product.Base using (map) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- Re-export all properties of magma monomorphisms @@ -39,7 +39,7 @@ open import Algebra.Morphism.MagmaMonomorphism module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong) - open SetoidReasoning setoid + open ≈-Reasoning setoid identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_ identityˡ idˡ x = injective (begin diff --git a/src/Algebra/Morphism/RingMonomorphism.agda b/src/Algebra/Morphism/RingMonomorphism.agda index 35a191a0f8..40e7a80d83 100644 --- a/src/Algebra/Morphism/RingMonomorphism.agda +++ b/src/Algebra/Morphism/RingMonomorphism.agda @@ -29,7 +29,7 @@ open RawRing R₂ renaming open import Algebra.Definitions open import Algebra.Structures open import Data.Product.Base using (proj₁; proj₂; _,_) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- Re-export all properties of group and monoid monomorphisms @@ -83,7 +83,7 @@ module _ (+-isGroup : IsGroup _≈₂_ _⊕_ 0#₂ ⊝_) open IsGroup +-isGroup hiding (setoid; refl; sym) open IsMagma *-isMagma renaming (∙-cong to ◦-cong) - open SetoidReasoning setoid + open ≈-Reasoning setoid distribˡ : _DistributesOverˡ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverˡ_ _≈₁_ _*_ _+_ distribˡ distribˡ x y z = injective (begin diff --git a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda index da8d3abf45..782b094fbe 100644 --- a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda +++ b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda @@ -8,7 +8,7 @@ open import Algebra using (CommutativeSemigroup) open import Data.Product.Base using (_,_) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Properties.CommutativeSemigroup.Divisibility {a ℓ} (CS : CommutativeSemigroup a ℓ) @@ -16,7 +16,7 @@ module Algebra.Properties.CommutativeSemigroup.Divisibility open CommutativeSemigroup CS open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz) -open EqReasoning setoid +open ≈-Reasoning setoid ------------------------------------------------------------------------ -- Re-export the contents of divisibility over semigroups diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda index 8062ff34df..f15f83824f 100644 --- a/src/Algebra/Solver/CommutativeMonoid.agda +++ b/src/Algebra/Solver/CommutativeMonoid.agda @@ -22,16 +22,16 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) open import Function.Base using (_∘_) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reflection as Reflection import Relation.Nullary.Decidable as Dec import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Nullary.Decidable using (Dec) open CommutativeMonoid M -open EqReasoning setoid +open ≈-Reasoning setoid private variable @@ -189,7 +189,7 @@ prove′ e₁ e₂ = lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ lemma eq ρ = R.prove ρ e₁ e₂ (begin - ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ ⟦ normalise e₂ ⟧⇓ ρ ∎) -- This procedure can be combined with from-just. diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda index fc65652787..35cfcc5ea6 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda @@ -20,19 +20,19 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate) open import Function.Base using (_∘_) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Relation.Binary.Reflection as Reflection import Relation.Nullary.Decidable as Dec import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise -open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid) open import Relation.Nullary.Decidable using (Dec) module Algebra.Solver.IdempotentCommutativeMonoid {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where open IdempotentCommutativeMonoid M -open EqReasoning setoid +open ≈-Reasoning setoid private variable @@ -202,7 +202,7 @@ prove′ e₁ e₂ = lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ lemma eq ρ = R.prove ρ e₁ e₂ (begin - ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ + ⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩ ⟦ normalise e₂ ⟧⇓ ρ ∎) -- This procedure can be combined with from-just. diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 5bd47dc763..4188bab92a 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -35,8 +35,8 @@ open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩- open import Function.Definitions using (Injective) open import Level using (Level) open import Relation.Binary.Definitions as B using (DecidableEquality) -import Relation.Binary.Reasoning.Setoid as EqR -open import Relation.Binary.PropositionalEquality as P hiding ([_]) +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +open import Relation.Binary.PropositionalEquality as ≡ hiding ([_]) open import Relation.Binary.Core using (Rel) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index edcf62b6da..4409e78cc4 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -24,7 +24,7 @@ open import Data.List.Relation.Binary.Equality.Setoid S open import Data.Nat.Base using (ℕ; zero; suc; _+_) open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private module Eq = Setoid S @@ -88,7 +88,7 @@ steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs module PermutationReasoning where - private module Base = SetoidReasoning ↭-setoid + private module Base = ≈-Reasoning ↭-setoid open Base public hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 5a18639aae..2174d29c74 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -42,7 +42,7 @@ open import Relation.Binary.Definitions import Relation.Binary.Consequences as BC open import Relation.Binary.PropositionalEquality import Relation.Binary.Properties.Poset as PosetProperties -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Reasoning.Syntax open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup @@ -153,7 +153,7 @@ proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃q { isDecEquivalence = ≃-isDecEquivalence } -module ≃-Reasoning = SetoidReasoning ≃-setoid +module ≃-Reasoning = ≈-Reasoning ≃-setoid ↥p≡0⇒p≃0 : ∀ p → ↥ p ≡ 0ℤ → p ≃ 0ℚᵘ ↥p≡0⇒p≃0 p ↥p≡0 = *≡* (cong (ℤ._* (↧ 0ℚᵘ)) ↥p≡0) diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda index 1028e694e8..50c84ce3c9 100644 --- a/src/Function/Properties/Bijection.agda +++ b/src/Function/Properties/Bijection.agda @@ -13,7 +13,7 @@ open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Trans) -open import Relation.Binary.PropositionalEquality as P using (setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) open import Function.Properties.Surjection using (injective⇒to⁻-cong) @@ -37,7 +37,7 @@ refl = Identity.bijection _ -- Can't prove full symmetry as we have no proof that the witness -- produced by the surjection proof preserves equality -sym-≡ : Bijection S (P.setoid B) → Bijection (P.setoid B) S +sym-≡ : Bijection S (≡.setoid B) → Bijection (≡.setoid B) S sym-≡ = Symmetry.bijection-≡ trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda index ad1264ec7c..5872569945 100644 --- a/src/Function/Properties/Equivalence.agda +++ b/src/Function/Properties/Equivalence.agda @@ -14,7 +14,7 @@ open import Level open import Relation.Binary.Definitions open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) -import Relation.Binary.PropositionalEquality.Properties as Eq +import Relation.Binary.PropositionalEquality.Properties as ≡ import Function.Construct.Identity as Identity import Function.Construct.Symmetry as Symmetry @@ -83,7 +83,7 @@ setoid s₁ s₂ = record ⇔-isEquivalence : IsEquivalence {ℓ = ℓ} _⇔_ ⇔-isEquivalence = record - { refl = λ {x} → Identity.equivalence (Eq.setoid x) + { refl = λ {x} → Identity.equivalence (≡.setoid x) ; sym = Symmetry.equivalence ; trans = Composition.equivalence } diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda index 0e773cf9b8..b191513549 100644 --- a/src/Function/Properties/Injection.agda +++ b/src/Function/Properties/Injection.agda @@ -16,9 +16,7 @@ import Function.Construct.Composition as Compose open import Level using (Level) open import Data.Product.Base using (proj₁; proj₂) open import Relation.Binary.Definitions -open import Relation.Binary.PropositionalEquality using () open import Relation.Binary using (Setoid) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning private variable diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda index 5ade85d843..0579d70a62 100644 --- a/src/Function/Properties/Inverse.agda +++ b/src/Function/Properties/Inverse.agda @@ -16,9 +16,9 @@ open import Level using (Level; _⊔_) open import Relation.Binary.Core using (REL) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) -open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) -import Relation.Binary.PropositionalEquality.Properties as P -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +import Relation.Binary.PropositionalEquality.Properties as ≡ +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning import Function.Consequences.Setoid as Consequences import Function.Construct.Identity as Identity @@ -148,8 +148,8 @@ module _ (ext : ∀ {a b} → Extensionality a b) where ↔-fun A↔B C↔D = mk↔ₛ′ (λ a→c b → to C↔D (a→c (from A↔B b))) (λ b→d a → from C↔D (b→d (to A↔B a))) - (λ b→d → ext λ _ → P.trans (strictlyInverseˡ C↔D _ ) (P.cong b→d (strictlyInverseˡ A↔B _))) - (λ a→c → ext λ _ → P.trans (strictlyInverseʳ C↔D _ ) (P.cong a→c (strictlyInverseʳ A↔B _))) + (λ b→d → ext λ _ → ≡.trans (strictlyInverseˡ C↔D _ ) (≡.cong b→d (strictlyInverseˡ A↔B _))) + (λ a→c → ext λ _ → ≡.trans (strictlyInverseʳ C↔D _ ) (≡.cong a→c (strictlyInverseʳ A↔B _))) where open Inverse module _ (I : Inverse S T) where diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda index 6f0bc11e6b..99e13c218d 100644 --- a/src/Function/Properties/Surjection.agda +++ b/src/Function/Properties/Surjection.agda @@ -15,10 +15,10 @@ import Function.Construct.Identity as Identity import Function.Construct.Composition as Compose open import Level using (Level) open import Data.Product.Base using (proj₁; proj₂) -import Relation.Binary.PropositionalEquality as P +import Relation.Binary.PropositionalEquality as ≡ open import Relation.Binary.Definitions open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private variable @@ -44,7 +44,7 @@ mkSurjection f surjective = record ↠⇒⟶ = Surjection.function ↠⇒↪ : A ↠ B → B ↪ A -↠⇒↪ s = mk↪ {from = to} λ { P.refl → proj₂ (strictlySurjective _)} +↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → proj₂ (strictlySurjective _)} where open Surjection s ↠⇒⇔ : A ↠ B → A ⇔ B @@ -75,6 +75,6 @@ injective⇒to⁻-cong {T = T} surj injective {x} {y} x≈y = injective $ begin y ≈⟨ to∘to⁻ y ⟨ to (to⁻ y) ∎ where - open SetoidReasoning T + open ≈-Reasoning T open Surjection surj diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index c4846142ec..47465e8926 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -18,7 +18,7 @@ open import Relation.Binary.Structures open import Relation.Binary.Definitions using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Decidable) open import Relation.Nullary.Negation using (¬_) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Lattice using (Infimum) module Relation.Binary.Construct.NaturalOrder.Left @@ -44,7 +44,7 @@ reflexive magma idem {x} {y} x≈y = begin x ≈⟨ sym (idem x) ⟩ x ∙ x ≈⟨ ∙-cong refl x≈y ⟩ x ∙ y ∎ - where open IsMagma magma; open EqReasoning setoid + where open IsMagma magma; open ≈-Reasoning setoid refl : Symmetric _≈_ → Idempotent _∙_ → Reflexive _≤_ refl sym idem {x} = sym (idem x) @@ -55,7 +55,7 @@ antisym isEq comm {x} {y} x≤y y≤x = begin x ∙ y ≈⟨ comm x y ⟩ y ∙ x ≈⟨ sym y≤x ⟩ y ∎ - where open IsEquivalence isEq; open EqReasoning (record { isEquivalence = isEq }) + where open IsEquivalence isEq; open ≈-Reasoning (record { isEquivalence = isEq }) total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_ total sym trans sel comm x y with sel x y @@ -69,14 +69,14 @@ trans semi {x} {y} {z} x≤y y≤z = begin x ∙ (y ∙ z) ≈⟨ sym (assoc x y z) ⟩ (x ∙ y) ∙ z ≈⟨ ∙-cong (sym x≤y) S.refl ⟩ x ∙ z ∎ - where open module S = IsSemigroup semi; open EqReasoning S.setoid + where open module S = IsSemigroup semi; open ≈-Reasoning S.setoid respʳ : IsMagma _∙_ → _≤_ Respectsʳ _≈_ respʳ magma {x} {y} {z} y≈z x≤y = begin x ≈⟨ x≤y ⟩ x ∙ y ≈⟨ ∙-cong M.refl y≈z ⟩ x ∙ z ∎ - where open module M = IsMagma magma; open EqReasoning M.setoid + where open module M = IsMagma magma; open ≈-Reasoning M.setoid respˡ : IsMagma _∙_ → _≤_ Respectsˡ _≈_ respˡ magma {x} {y} {z} y≈z y≤x = begin @@ -84,7 +84,7 @@ respˡ magma {x} {y} {z} y≈z y≤x = begin y ≈⟨ y≤x ⟩ y ∙ x ≈⟨ ∙-cong y≈z M.refl ⟩ z ∙ x ∎ - where open module M = IsMagma magma; open EqReasoning M.setoid + where open module M = IsMagma magma; open ≈-Reasoning M.setoid resp₂ : IsMagma _∙_ → _≤_ Respects₂ _≈_ resp₂ magma = respʳ magma , respˡ magma @@ -95,7 +95,7 @@ dec _≟_ x y = x ≟ (x ∙ y) module _ (semi : IsSemilattice _∙_) where private open module S = IsSemilattice semi - open EqReasoning setoid + open ≈-Reasoning setoid x∙y≤x : ∀ x y → (x ∙ y) ≤ x x∙y≤x x y = begin diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index 3c2aa348d6..76529350e2 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -19,7 +19,7 @@ open import Relation.Binary.Definitions using (Symmetric; Transitive; Reflexive; Antisymmetric; Total; _Respectsʳ_; _Respectsˡ_; _Respects₂_; Decidable) open import Relation.Nullary.Negation using (¬_) -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Relation.Binary.Construct.NaturalOrder.Right {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) where @@ -44,7 +44,7 @@ reflexive magma idem {x} {y} x≈y = begin x ≈⟨ sym (idem x) ⟩ x ∙ x ≈⟨ ∙-cong x≈y refl ⟩ y ∙ x ∎ - where open IsMagma magma; open EqReasoning setoid + where open IsMagma magma; open ≈-Reasoning setoid refl : Symmetric _≈_ → Idempotent _∙_ → Reflexive _≤_ refl sym idem {x} = sym (idem x) @@ -55,7 +55,7 @@ antisym isEq comm {x} {y} x≤y y≤x = begin y ∙ x ≈⟨ comm y x ⟩ x ∙ y ≈⟨ y≤x ⟨ y ∎ - where open EqReasoning (record { isEquivalence = isEq }) + where open ≈-Reasoning (record { isEquivalence = isEq }) total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_ total sym trans sel comm x y with sel x y @@ -69,14 +69,14 @@ trans semi {x} {y} {z} x≤y y≤z = begin (z ∙ y) ∙ x ≈⟨ assoc z y x ⟩ z ∙ (y ∙ x) ≈⟨ ∙-cong S.refl (sym x≤y) ⟩ z ∙ x ∎ - where open module S = IsSemigroup semi; open EqReasoning S.setoid + where open module S = IsSemigroup semi; open ≈-Reasoning S.setoid respʳ : IsMagma _∙_ → _≤_ Respectsʳ _≈_ respʳ magma {x} {y} {z} y≈z x≤y = begin x ≈⟨ x≤y ⟩ y ∙ x ≈⟨ ∙-cong y≈z M.refl ⟩ z ∙ x ∎ - where open module M = IsMagma magma; open EqReasoning M.setoid + where open module M = IsMagma magma; open ≈-Reasoning M.setoid respˡ : IsMagma _∙_ → _≤_ Respectsˡ _≈_ respˡ magma {x} {y} {z} y≈z y≤x = begin @@ -84,7 +84,7 @@ respˡ magma {x} {y} {z} y≈z y≤x = begin y ≈⟨ y≤x ⟩ x ∙ y ≈⟨ ∙-cong M.refl y≈z ⟩ x ∙ z ∎ - where open module M = IsMagma magma; open EqReasoning M.setoid + where open module M = IsMagma magma; open ≈-Reasoning M.setoid resp₂ : IsMagma _∙_ → _≤_ Respects₂ _≈_ resp₂ magma = respʳ magma , respˡ magma diff --git a/src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda b/src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda index e7090dc6c5..4727088718 100644 --- a/src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda +++ b/src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda @@ -19,13 +19,13 @@ open import Data.Product.Base using (_,_) open import Function.Base using (_$_; flip; _∘_) open import Level using (_⊔_) open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) -import Relation.Binary.Reasoning.PartialOrder as POR +import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice boundedMeetSemilattice as BM open import Relation.Binary.Lattice.Properties.Lattice lattice open import Relation.Binary.Lattice.Properties.BoundedLattice boundedLattice -import Relation.Binary.Reasoning.Setoid as EqReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- Useful lemmas @@ -62,7 +62,7 @@ y≤x⇨y = transpose-⇨ (x∧y≤x _ _) x ⇨ u ≤⟨ ⇨ʳ-covariant u≤v ⟩ x ⇨ v ≤⟨ ⇨ˡ-contravariant y≤x ⟩ y ⇨ v ∎ - where open POR poset + where open ≤-Reasoning poset ⇨-cong : _⇨_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ ⇨-cong x≈y u≈v = antisym (⇨-relax (reflexive $ Eq.sym x≈y) (reflexive u≈v)) @@ -113,7 +113,7 @@ y≤x⇨y = transpose-⇨ (x∧y≤x _ _) (((x ⇨ y) ∧ x) ∧ (x ⇨ z)) ∧ x ≈⟨ ∧-assoc _ _ _ ⟩ (((x ⇨ y) ∧ x) ∧ (x ⇨ z) ∧ x) ≤⟨ ∧-monotonic ⇨-eval ⇨-eval ⟩ y ∧ z ∎) - where open POR poset + where open ≤-Reasoning poset ⇨-distribˡ-∧ : _⇨_ DistributesOverˡ _∧_ ⇨-distribˡ-∧ x y z = antisym (⇨-distribˡ-∧-≤ x y z) (⇨-distribˡ-∧-≥ x y z) @@ -175,7 +175,7 @@ de-morgan₂-≤ x y = transpose-⇨ $ begin ¬ ¬ y ∧ ¬ y ≤⟨ ⇨-eval ⟩ ⊥ ∎ ⟩ ⊥ ∎ - where open POR poset + where open ≤-Reasoning poset de-morgan₂-≥ : ∀ x y → ¬ ¬ (¬ x ∨ ¬ y) ≤ ¬ (x ∧ y) de-morgan₂-≥ x y = transpose-⇨ $ ⇨-applyˡ $ transpose-⇨ $ begin @@ -184,7 +184,7 @@ de-morgan₂-≥ x y = transpose-⇨ $ ⇨-applyˡ $ transpose-⇨ $ begin (⇨-applyʳ (x∧y≤y _ _)) ⟩ ⊥ ∨ ⊥ ≈⟨ ∨-idempotent _ ⟩ ⊥ ∎ - where open POR poset + where open ≤-Reasoning poset de-morgan₂ : ∀ x y → ¬ (x ∧ y) ≈ ¬ ¬ (¬ x ∨ ¬ y) de-morgan₂ x y = antisym (de-morgan₂-≤ x y) (de-morgan₂-≥ x y) @@ -196,4 +196,4 @@ weak-lem {x} = begin ⊥ ∧ (x ⇨ ⊥) ⇨ ⊥ ≈⟨ ⇨-cong (∧-zeroˡ _) Eq.refl ⟩ ⊥ ⇨ ⊥ ≈⟨ ⇨-unit ⟩ ⊤ ∎ - where open EqReasoning setoid + where open ≈-Reasoning setoid diff --git a/src/Relation/Binary/Lattice/Properties/Lattice.agda b/src/Relation/Binary/Lattice/Properties/Lattice.agda index fd95effaaf..261371a3f0 100644 --- a/src/Relation/Binary/Lattice/Properties/Lattice.agda +++ b/src/Relation/Binary/Lattice/Properties/Lattice.agda @@ -21,8 +21,8 @@ open import Function.Base using (flip) open import Relation.Binary.Properties.Poset poset import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice as J import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice as M -import Relation.Binary.Reasoning.Setoid as EqReasoning -import Relation.Binary.Reasoning.PartialOrder as POR +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning ∨-absorbs-∧ : _∨_ Absorbs _∧_ ∨-absorbs-∧ x y = @@ -44,7 +44,7 @@ absorptive = ∨-absorbs-∧ , ∧-absorbs-∨ x ∧ y ≤⟨ x∧y≤x x y ⟩ x ≤⟨ x≤x∨y x y ⟩ x ∨ y ∎ - where open POR poset + where open ≤-Reasoning poset -- two quadrilateral arguments @@ -55,14 +55,14 @@ quadrilateral₁ {x} {y} x∨y≈x = begin y ∧ (x ∨ y) ≈⟨ M.∧-cong Eq.refl (J.∨-comm _ _) ⟩ y ∧ (y ∨ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩ y ∎ - where open EqReasoning setoid + where open ≈-Reasoning setoid quadrilateral₂ : ∀ {x y} → x ∧ y ≈ y → x ∨ y ≈ x quadrilateral₂ {x} {y} x∧y≈y = begin x ∨ y ≈⟨ J.∨-cong Eq.refl (Eq.sym x∧y≈y) ⟩ x ∨ (x ∧ y) ≈⟨ ∨-absorbs-∧ _ _ ⟩ x ∎ - where open EqReasoning setoid + where open ≈-Reasoning setoid -- collapsing sublattice @@ -75,7 +75,7 @@ collapse₁ {x} {y} x≈y = begin x ∨ y ∎ where y≤x = reflexive (Eq.sym x≈y) - open EqReasoning setoid + open ≈-Reasoning setoid -- this can also be proved by quadrilateral argument, but it's much less symmetric. collapse₂ : ∀ {x y} → x ∨ y ≤ x ∧ y → x ≈ y @@ -88,7 +88,7 @@ collapse₂ {x} {y} ∨≤∧ = antisym x ∨ y ≤⟨ ∨≤∧ ⟩ x ∧ y ≤⟨ x∧y≤x _ _ ⟩ x ∎) - where open POR poset + where open ≤-Reasoning poset ------------------------------------------------------------------------ -- The dual construction is also a lattice. diff --git a/src/Relation/Binary/Reasoning/PartialSetoid.agda b/src/Relation/Binary/Reasoning/PartialSetoid.agda index 1149f1a298..5163c99947 100644 --- a/src/Relation/Binary/Reasoning/PartialSetoid.agda +++ b/src/Relation/Binary/Reasoning/PartialSetoid.agda @@ -15,14 +15,14 @@ module Relation.Binary.Reasoning.PartialSetoid open PartialSetoid S import Relation.Binary.Reasoning.Base.Partial _≈_ trans - as PartialReasoning + as ≈-Reasoning ------------------------------------------------------------------------ -- Reasoning combinators -- Export the combinators for partial relation reasoning, hiding the -- single misnamed combinator. -open PartialReasoning public hiding (step-∼) +open ≈-Reasoning public hiding (step-∼) -- Re-export the equality-based combinators instead -open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ PartialReasoning.∼-go sym public +open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ ≈-Reasoning.∼-go sym public diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda index a21288100a..12665df8cc 100644 --- a/src/Relation/Binary/Reflection.agda +++ b/src/Relation/Binary/Reflection.agda @@ -14,7 +14,7 @@ open import Function.Base using (id; _⟨_⟩_) open import Function.Bundles using (module Equivalence) open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) -import Relation.Binary.PropositionalEquality.Core as P +import Relation.Binary.PropositionalEquality.Core as ≡ -- Think of the parameters as follows: -- @@ -42,10 +42,10 @@ module Relation.Binary.Reflection open import Data.Vec.N-ary open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) -import Relation.Binary.Reasoning.Setoid as Eq +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open Setoid Sem -open Eq Sem +open ≈-Reasoning Sem -- If two normalised expressions are semantically equal, then their -- non-normalised forms are also equal. @@ -91,7 +91,7 @@ solve₁ : ∀ n (f : N-ary n (Expr n) (Expr n × Expr n)) → ⟦ proj₁ (close n f) ⟧ ρ ≈ ⟦ proj₂ (close n f) ⟧ ρ) solve₁ n f = Equivalence.from (uncurry-∀ⁿ n) λ ρ → - P.subst id (P.sym (left-inverse (λ _ → _ ≈ _ → _ ≈ _) ρ)) + ≡.subst id (≡.sym (left-inverse (λ _ → _ ≈ _ → _ ≈ _) ρ)) (prove ρ (proj₁ (close n f)) (proj₂ (close n f))) -- A variant of _,_ which is intended to make uses of solve and solve₁ diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda index c62ea9dccf..4e370bea25 100644 --- a/src/Tactic/MonoidSolver.agda +++ b/src/Tactic/MonoidSolver.agda @@ -88,7 +88,7 @@ import Reflection.AST.Name as Name open import Reflection.TCM open import Reflection.TCM.Syntax -import Relation.Binary.Reasoning.Setoid as SetoidReasoning +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning ------------------------------------------------------------------------ -- The Expr type with homomorphism proofs @@ -103,7 +103,7 @@ data Expr {a} (A : Set a) : Set a where module _ {m₁ m₂} (monoid : Monoid m₁ m₂) where open Monoid monoid - open SetoidReasoning setoid + open ≈-Reasoning setoid -- Convert the AST to an expression (i.e. evaluate it) without -- normalising. From b9f5bd0c9e2cc67c2e7a57abe4154982426f0b89 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 7 Feb 2024 07:25:33 +0000 Subject: [PATCH 5/5] alignment --- src/Data/Integer/Divisibility/Signed.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda index 2861cbf7d8..d171b7015e 100644 --- a/src/Data/Integer/Divisibility/Signed.agda +++ b/src/Data/Integer/Divisibility/Signed.agda @@ -69,8 +69,8 @@ open _∣_ using (quotient) public sign-eq : sign i ≡ sign (ikq * k) sign-eq = sym $ begin - sign (ikq * k) ≡⟨ sign-◃ (sign ikq Sign.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩ - sign ikq Sign.* sign k ≡⟨ cong (Sign._* sign k) (sign-◃ (sign i Sign.* sign k) q) ⟩ + sign (ikq * k) ≡⟨ sign-◃ (sign ikq Sign.* sign k) (∣ ikq ∣ ℕ.* ∣ k ∣) ⟩ + sign ikq Sign.* sign k ≡⟨ cong (Sign._* sign k) (sign-◃ (sign i Sign.* sign k) q) ⟩ (sign i Sign.* sign k) Sign.* sign k ≡⟨ Sign.*-assoc (sign i) (sign k) (sign k) ⟩ sign i Sign.* (sign k Sign.* sign k) ≡⟨ cong (sign i Sign.*_) (Sign.s*s≡+ (sign k)) ⟩ sign i Sign.* Sign.+ ≡⟨ Sign.*-identityʳ (sign i) ⟩