Skip to content

Commit b3bfbb2

Browse files
jamesmckinnajamesmckinna
authored
Qualified import of reasoning modules fixing #2280 (#2282)
* `Data.List.Relation.Relation.Binary.BagAndSetEquality` * `Relation.Binary.Reasoning.*` * preorder reasoning * setoid reasoning * alignment
1 parent c8496d0 commit b3bfbb2

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+177
-180
lines changed

‎src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
2121
open import Algebra.Properties.Ring ring
2222
using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
2323
open import Relation.Binary.Definitions using (Symmetric)
24-
import Relation.Binary.Reasoning.Setoid as ReasonSetoid
24+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2525
open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
2626

2727
private variable
@@ -50,7 +50,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
5050
helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
5151
= invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
5252
where
53-
open ReasonSetoid setoid
53+
open ≈-Reasoning setoid
5454

5555
y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
5656
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)
6767
#-sym : Symmetric _#_
6868
#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
6969
where
70-
open ReasonSetoid setoid
70+
open ≈-Reasoning setoid
7171
InvX-Y : Invertible _≈_ 1# _*_ (x - y)
7272
InvX-Y = #⇒invertible x#y
7373

@@ -96,7 +96,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
9696
helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
9797
= invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
9898
where
99-
open ReasonSetoid setoid
99+
open ≈-Reasoning setoid
100100

101101
x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
102102
x-z⁻¹*y-z≈1 = begin

‎src/Algebra/Construct/LexProduct.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel)
1616
open import Relation.Binary.Definitions using (Decidable)
1717
open import Relation.Nullary using (¬_; does; yes; no)
1818
open import Relation.Nullary.Negation using (contradiction; contradiction₂)
19-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
19+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2020

2121
module Algebra.Construct.LexProduct
2222
{ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)

‎src/Algebra/Construct/LiftedChoice.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Level using (Level; _⊔_)
2020
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
2121
open import Relation.Unary using (Pred)
2222

23-
import Relation.Binary.Reasoning.Setoid as EqReasoning
23+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2424

2525
private
2626
variable
@@ -46,7 +46,7 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
4646

4747
private module M = IsSelectiveMagma ∙-isSelectiveMagma
4848
open M hiding (sel; isMagma)
49-
open EqReasoning setoid
49+
open ≈-Reasoning setoid
5050

5151
module _ (f : A → B) where
5252

‎src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ import Algebra.Lattice.Properties.Lattice as LatticeProperties
1818
open import Data.Product.Base using (_,_; map)
1919
open import Relation.Binary.Bundles using (Setoid)
2020
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
21-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
21+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2222

2323
module Algebra.Lattice.Morphism.LatticeMonomorphism
2424
{a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
@@ -73,7 +73,7 @@ module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where
7373
setoid : Setoid b ℓ₂
7474
setoid = record { isEquivalence = isEquivalence }
7575

76-
open SetoidReasoning setoid
76+
open ≈-Reasoning setoid
7777

7878
∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_
7979
∨-absorbs-∧ x y = injective (begin

‎src/Algebra/Module/Bundles.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ open import Function.Base
3737
open import Level
3838
open import Relation.Binary.Core using (Rel)
3939
open import Relation.Nullary using (¬_)
40-
import Relation.Binary.Reasoning.Setoid as SetR
40+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
4141

4242
private
4343
variable
@@ -364,7 +364,7 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
364364
; rawBisemimodule; _≉ᴹ_
365365
)
366366

367-
open SetR ≈ᴹ-setoid
367+
open ≈-Reasoning ≈ᴹ-setoid
368368

369369
*ₗ-comm : L.Commutative _*ₗ_
370370
*ₗ-comm x y m = begin

‎src/Algebra/Module/Consequences.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Function.Base using (flip)
1616
open import Level using (Level)
1717
open import Relation.Binary.Core using (Rel)
1818
open import Relation.Binary.Bundles using (Setoid)
19-
import Relation.Binary.Reasoning.Setoid as Rea
19+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2020

2121
private
2222
variable
@@ -27,7 +27,7 @@ private
2727
module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where
2828

2929
open Setoid S
30-
open Rea S
30+
open ≈-Reasoning S
3131
open Defs _≈ᴬ_
3232

3333
private

‎src/Algebra/Morphism.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ import Algebra.Properties.Group as GroupP
1414
open import Function.Base
1515
open import Level
1616
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
17-
import Relation.Binary.Reasoning.Setoid as EqR
17+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
1818

1919
private
2020
variable
@@ -137,7 +137,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
137137
open IsMonoidMorphism mn-homo public
138138

139139
⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
140-
⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
140+
⁻¹-homo x = let open ≈-Reasoning T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
141141
⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
142142
⟦ x F.⁻¹ F.∙ x ⟧ ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
143143
⟦ F.ε ⟧ ≈⟨ ε-homo ⟩

‎src/Algebra/Morphism/Consequences.agda

+3-3
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open import Algebra.Morphism.Definitions
1313
open import Data.Product.Base using (_,_)
1414
open import Function.Base using (id; _∘_)
1515
open import Function.Definitions
16-
import Relation.Binary.Reasoning.Setoid as EqR
16+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
1717

1818
------------------------------------------------------------------------
1919
-- 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
3434
g (f (g x) ∙₂ f (g y)) ≈⟨ g-cong (homo (g x) (g y)) ⟨
3535
g (f (g x ∙₁ g y)) ≈⟨ invʳ M₂.refl ⟩
3636
g x ∙₁ g y ∎
37-
where open EqR M₁.setoid
37+
where open ≈-Reasoning M₁.setoid
3838

3939
homomorphic₂-inj : ∀ {f g} → Injective _≈₁_ _≈₂_ f →
4040
Inverseˡ _≈₁_ _≈₂_ f g →
@@ -45,4 +45,4 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
4545
x ∙₂ y ≈⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟨
4646
f (g x) ∙₂ f (g y) ≈⟨ homo (g x) (g y) ⟨
4747
f (g x ∙₁ g y) ∎)
48-
where open EqR M₂.setoid
48+
where open ≈-Reasoning M₂.setoid

‎src/Algebra/Morphism/GroupMonomorphism.agda

+3-3
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ open RawGroup G₂ renaming
2727
open import Algebra.Definitions
2828
open import Algebra.Structures
2929
open import Data.Product.Base using (_,_)
30-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
30+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
3131

3232
------------------------------------------------------------------------
3333
-- Re-export all properties of monoid monomorphisms
@@ -41,7 +41,7 @@ open import Algebra.Morphism.MonoidMonomorphism
4141
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
4242

4343
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
44-
open SetoidReasoning setoid
44+
open ≈-Reasoning setoid
4545

4646
inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁ _∙_
4747
inverseˡ invˡ x = injective (begin
@@ -72,7 +72,7 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
7272
module _ (◦-isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂) where
7373

7474
open IsAbelianGroup ◦-isAbelianGroup renaming (∙-cong to ◦-cong; ⁻¹-cong to ⁻¹₂-cong)
75-
open SetoidReasoning setoid
75+
open ≈-Reasoning setoid
7676

7777
⁻¹-distrib-∙ : (∀ x y → (x ◦ y) ⁻¹₂ ≈₂ (x ⁻¹₂) ◦ (y ⁻¹₂)) → (∀ x y → (x ∙ y) ⁻¹₁ ≈₁ (x ⁻¹₁) ∙ (y ⁻¹₁))
7878
⁻¹-distrib-∙ ⁻¹-distrib-∙ x y = injective (begin

‎src/Algebra/Morphism/MagmaMonomorphism.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ open import Algebra.Structures
2727
open import Algebra.Definitions
2828
open import Data.Product.Base using (map)
2929
open import Data.Sum.Base using (inj₁; inj₂)
30-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
30+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
3131
import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
3232

3333
------------------------------------------------------------------------
@@ -36,7 +36,7 @@ import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
3636
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
3737

3838
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
39-
open SetoidReasoning setoid
39+
open ≈-Reasoning setoid
4040

4141
cong : Congruent₂ _≈₁_ _∙_
4242
cong {x} {y} {u} {v} x≈y u≈v = injective (begin

‎src/Algebra/Morphism/MonoidMonomorphism.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_;
2525
open import Algebra.Definitions
2626
open import Algebra.Structures
2727
open import Data.Product.Base using (map)
28-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
28+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2929

3030
------------------------------------------------------------------------
3131
-- Re-export all properties of magma monomorphisms
@@ -39,7 +39,7 @@ open import Algebra.Morphism.MagmaMonomorphism
3939
module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
4040

4141
open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
42-
open SetoidReasoning setoid
42+
open ≈-Reasoning setoid
4343

4444
identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
4545
identityˡ idˡ x = injective (begin

‎src/Algebra/Morphism/RingMonomorphism.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ open RawRing R₂ renaming
2929
open import Algebra.Definitions
3030
open import Algebra.Structures
3131
open import Data.Product.Base using (proj₁; proj₂; _,_)
32-
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
32+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
3333

3434
------------------------------------------------------------------------
3535
-- Re-export all properties of group and monoid monomorphisms
@@ -83,7 +83,7 @@ module _ (+-isGroup : IsGroup _≈₂_ _⊕_ 0#₂ ⊝_)
8383

8484
open IsGroup +-isGroup hiding (setoid; refl; sym)
8585
open IsMagma *-isMagma renaming (∙-cong to ◦-cong)
86-
open SetoidReasoning setoid
86+
open ≈-Reasoning setoid
8787

8888
distribˡ : _DistributesOverˡ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverˡ_ _≈₁_ _*_ _+_
8989
distribˡ distribˡ x y z = injective (begin

‎src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,15 @@
88

99
open import Algebra using (CommutativeSemigroup)
1010
open import Data.Product.Base using (_,_)
11-
import Relation.Binary.Reasoning.Setoid as EqReasoning
11+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
1212

1313
module Algebra.Properties.CommutativeSemigroup.Divisibility
1414
{a ℓ} (CS : CommutativeSemigroup a ℓ)
1515
where
1616

1717
open CommutativeSemigroup CS
1818
open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz)
19-
open EqReasoning setoid
19+
open ≈-Reasoning setoid
2020

2121
------------------------------------------------------------------------
2222
-- Re-export the contents of divisibility over semigroups

‎src/Algebra/Solver/CommutativeMonoid.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -22,16 +22,16 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
2222

2323
open import Function.Base using (_∘_)
2424

25-
import Relation.Binary.Reasoning.Setoid as EqReasoning
25+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2626
import Relation.Binary.Reflection as Reflection
2727
import Relation.Nullary.Decidable as Dec
2828
import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
2929

30-
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
30+
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
3131
open import Relation.Nullary.Decidable using (Dec)
3232

3333
open CommutativeMonoid M
34-
open EqReasoning setoid
34+
open ≈-Reasoning setoid
3535

3636
private
3737
variable
@@ -189,7 +189,7 @@ prove′ e₁ e₂ =
189189
lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
190190
lemma eq ρ =
191191
R.prove ρ e₁ e₂ (begin
192-
⟦ normalise e₁ ⟧⇓ ρ ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
192+
⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
193193
⟦ normalise e₂ ⟧⇓ ρ ∎)
194194

195195
-- This procedure can be combined with from-just.

‎src/Algebra/Solver/IdempotentCommutativeMonoid.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -20,19 +20,19 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
2020

2121
open import Function.Base using (_∘_)
2222

23-
import Relation.Binary.Reasoning.Setoid as EqReasoning
23+
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2424
import Relation.Binary.Reflection as Reflection
2525
import Relation.Nullary.Decidable as Dec
2626
import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
2727

28-
open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
28+
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid)
2929
open import Relation.Nullary.Decidable using (Dec)
3030

3131
module Algebra.Solver.IdempotentCommutativeMonoid
3232
{m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
3333

3434
open IdempotentCommutativeMonoid M
35-
open EqReasoning setoid
35+
open ≈-Reasoning setoid
3636

3737
private
3838
variable
@@ -202,7 +202,7 @@ prove′ e₁ e₂ =
202202
lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
203203
lemma eq ρ =
204204
R.prove ρ e₁ e₂ (begin
205-
⟦ normalise e₁ ⟧⇓ ρ ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
205+
⟦ normalise e₁ ⟧⇓ ρ ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
206206
⟦ normalise e₂ ⟧⇓ ρ ∎)
207207

208208
-- This procedure can be combined with from-just.

‎src/Codata/Musical/Colist.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,8 @@ open import Relation.Binary.Core using (Rel; _⇒_)
3131
open import Relation.Binary.Bundles using (Poset; Setoid; Preorder)
3232
open import Relation.Binary.Definitions using (Transitive; Antisymmetric)
3333
import Relation.Binary.Construct.FromRel as Ind
34-
import Relation.Binary.Reasoning.Preorder as PreR
35-
import Relation.Binary.Reasoning.PartialOrder as POR
34+
import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
35+
import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning
3636
open import Relation.Binary.PropositionalEquality as P using (_≡_)
3737
open import Relation.Binary.Reasoning.Syntax
3838
open import Relation.Nullary.Reflects using (invert)
@@ -164,7 +164,7 @@ Any-∈ {P = P} = mk↔ₛ′
164164
antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂)
165165

166166
module ⊑-Reasoning {a} {A : Set a} where
167-
private module Base = POR (⊑-Poset A)
167+
private module Base = ≤-Reasoning (⊑-Poset A)
168168

169169
open Base public hiding (step-<; step-≤)
170170

@@ -188,7 +188,7 @@ module ⊑-Reasoning {a} {A : Set a} where
188188
-- ys ≡⟨ ys≡zs ⟩
189189
-- zs ∎
190190
module ⊆-Reasoning {A : Set a} where
191-
private module Base = PreR (⊆-Preorder A)
191+
private module Base = ≲-Reasoning (⊆-Preorder A)
192192

193193
open Base public
194194
hiding (step-≲; step-∼)

0 commit comments

Comments
 (0)