diff --git a/CHANGELOG.md b/CHANGELOG.md index 6bfd659aa9..2e2bb5ebc2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,9 @@ Bug-fixes in `Function.Construct.Composition` had their arguments in the wrong order. They have been flipped so they can actually be used as a composition operator. +* The combinators `_≃⟨_⟩_` and `_≃˘⟨_⟩_` in `Data.Rational.Properties.≤-Reasoning` + now correctly accepts proofs of type `_≃_` instead of the previous proofs of type `_≡_`. + * The following operators were missing a fixity declaration, which has now been fixed - ``` @@ -536,6 +539,10 @@ Non-backwards compatible changes 3. Finally, if the above approaches are not viable then you may be forced to explicitly use `cong` combined with a lemma that proves the old reduction behaviour. +* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base` + has been made into a data type with the single constructor `*≡*`. The destructor `drop-*≡*` + has been added to `Data.Rational.Properties`. + ### Change to the definition of `LeftCancellative` and `RightCancellative` * The definitions of the types for cancellativity in `Algebra.Definitions` previously @@ -1182,6 +1189,15 @@ Major improvements * In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_` +### More modular design of equational reasoning. + +* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports + a range of modules containing pre-existing reasoning combinator syntax. + +* This makes it possible to add new or rename existing reasoning combinators to a + pre-existing `Reasoning` module in just a couple of lines + (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`) + Deprecated modules ------------------ @@ -1753,6 +1769,11 @@ Deprecated names sym-↔ ↦ ↔-sym ``` +* In `Function.Related.Propositional.Reasoning`: + ```agda + _↔⟨⟩_ ↦ _≡⟨⟩_ + ``` + * In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`: ``` toForeign ↦ Foreign.Haskell.Coerce.coerce @@ -2640,6 +2661,8 @@ Additions to existing modules toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ + + <-asym : Asymmetric _<_ ``` * Added a new pattern synonym to `Data.Nat.Divisibility.Core`: @@ -2809,6 +2832,7 @@ Additions to existing modules ```agda ↥ᵘ-toℚᵘ : ↥ᵘ (toℚᵘ p) ≡ ↥ p ↧ᵘ-toℚᵘ : ↧ᵘ (toℚᵘ p) ≡ ↧ p + ↥p≡↥q≡0⇒p≡q : ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≡ q _≥?_ : Decidable _≥_ _>?_ : Decidable _>_ @@ -2833,6 +2857,10 @@ Additions to existing modules * Added new definitions in `Data.Rational.Unnormalised.Properties`: ```agda + ↥p≡0⇒p≃0 : ↥ p ≡ 0ℤ → p ≃ 0ℚᵘ + p≃0⇒↥p≡0 : p ≃ 0ℚᵘ → ↥ p ≡ 0ℤ + ↥p≡↥q≡0⇒p≃q : ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≃ q + +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ +-*-rawSemiring : RawSemiring 0ℓ 0ℓ diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda index acc7153f52..9f573cc711 100644 --- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda +++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda @@ -127,10 +127,14 @@ module _ {A : Set a} where ------------------------------------------------------------------------ -- Pointwise DSL +-- -- A guardedness check does not play well with compositional proofs. -- Luckily we can learn from Nils Anders Danielsson's -- Beating the Productivity Checker Using Embedded Languages -- and design a little compositional DSL to define such proofs +-- +-- NOTE: also because of the guardedness check we can't use the standard +-- `Relation.Binary.Reasoning.Syntax` approach. module pw-Reasoning (S : Setoid a ℓ) where private module S = Setoid S diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index 2f59082e22..aeff3076dc 100644 --- a/src/Codata/Musical/Colist.agda +++ b/src/Codata/Musical/Colist.agda @@ -34,6 +34,7 @@ import Relation.Binary.Construct.FromRel as Ind import Relation.Binary.Reasoning.Preorder as PreR import Relation.Binary.Reasoning.PartialOrder as POR open import Relation.Binary.PropositionalEquality as P using (_≡_) +open import Relation.Binary.Reasoning.Syntax open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary open import Relation.Nullary.Negation @@ -165,12 +166,11 @@ Any-∈ {P = P} = mk↔ₛ′ module ⊑-Reasoning {a} {A : Set a} where private module Base = POR (⊑-Poset A) - open Base public - hiding (step-<; begin-strict_; step-≤) + open Base public hiding (step-<; step-≤) + + open ⊑-syntax _IsRelatedTo_ _IsRelatedTo_ Base.≤-go public + open ⊏-syntax _IsRelatedTo_ _IsRelatedTo_ Base.<-go public - infixr 2 step-⊑ - step-⊑ = Base.step-≤ - syntax step-⊑ x ys⊑zs xs⊑ys = x ⊑⟨ xs⊑ys ⟩ ys⊑zs -- The subset relation forms a preorder. @@ -179,22 +179,22 @@ module ⊑-Reasoning {a} {A : Set a} where (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys)) where module ⊑P = Poset (⊑-Poset A) +-- Example uses: +-- +-- x∈zs : x ∈ zs +-- x∈zs = +-- x ∈⟨ x∈xs ⟩ +-- xs ⊆⟨ xs⊆ys ⟩ +-- ys ≡⟨ ys≡zs ⟩ +-- zs ∎ module ⊆-Reasoning {A : Set a} where private module Base = PreR (⊆-Preorder A) - open Base public - hiding (step-∼) - - infixr 2 step-⊆ - infix 1 step-∈ - - step-⊆ = Base.step-∼ + open Base public hiding (step-∼) - step-∈ : ∀ (x : A) {xs ys} → xs IsRelatedTo ys → x ∈ xs → x ∈ ys - step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs + open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) + open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public - syntax step-⊆ xs ys⊆zs xs⊆ys = xs ⊆⟨ xs⊆ys ⟩ ys⊆zs - syntax step-∈ x xs⊆ys x∈xs = x ∈⟨ x∈xs ⟩ xs⊆ys -- take returns a prefix. take-⊑ : ∀ n (xs : Colist A) → diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda index d3265acefb..0a4340fa7b 100644 --- a/src/Data/Container/Relation/Unary/Any/Properties.agda +++ b/src/Data/Container/Relation/Unary/Any/Properties.agda @@ -26,7 +26,6 @@ open import Relation.Binary.Core using (REL) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl) -open Related.EquationalReasoning hiding (_≡⟨_⟩_) private module ×⊎ {k ℓ} = CommutativeSemiring (×-⊎-commutativeSemiring k ℓ) @@ -71,6 +70,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x} (∃ λ x → x ∈ xs₁ × P₁ x) ∼⟨ Σ.cong ↔-refl (xs₁≈xs₂ ×-cong P₁↔P₂ _) ⟩ (∃ λ x → x ∈ xs₂ × P₂ x) ↔⟨ SK-sym (↔∈ C) ⟩ ◇ C P₂ xs₂ ∎ + where open Related.EquationalReasoning -- Nested occurrences of ◇ can sometimes be swapped. @@ -95,6 +95,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s (∃ λ y → y ∈ ys × ∃ λ x → x ∈ xs × P x y) ↔⟨ Σ.cong ↔-refl (Σ.cong ↔-refl (SK-sym (↔∈ C₁))) ⟩ (∃ λ y → y ∈ ys × ◇ _ (flip P y) xs) ↔⟨ SK-sym (↔∈ C₂) ⟩ ◇ _ (λ y → ◇ _ (flip P y) xs) ys ∎ + where open Related.EquationalReasoning -- Nested occurrences of ◇ can sometimes be flattened. @@ -162,9 +163,10 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y} map↔∘ : ∀ {xs : ⟦ C ⟧ X} (f : X → Y) → ◇ C P (map f xs) ↔ ◇ C (P ∘′ f) xs map↔∘ {xs} f = ◇ C P (map f xs) ↔⟨ ↔Σ C ⟩ - ∃ (P ∘′ proj₂ (map f xs)) ↔⟨⟩ + ∃ (P ∘′ proj₂ (map f xs)) ≡⟨⟩ ∃ (P ∘′ f ∘′ proj₂ xs) ↔⟨ SK-sym (↔Σ C) ⟩ ◇ C (P ∘′ f) xs ∎ + where open Related.EquationalReasoning -- Membership in a mapped container can be expressed without reference -- to map. @@ -178,6 +180,7 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y} y ∈ map f xs ↔⟨ map↔∘ C (y ≡_) f ⟩ ◇ C (λ x → y ≡ f x) xs ↔⟨ ↔∈ C ⟩ ∃ (λ x → x ∈ xs × y ≡ f x) ∎ + where open Related.EquationalReasoning -- map is a congruence for bag and set equality and related preorders. @@ -193,6 +196,7 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y} ◇ C (λ y → x ≡ f₂ y) xs₂ ↔⟨ SK-sym (map↔∘ C (_≡_ x) f₂) ⟩ x ∈ map f₂ xs₂ ∎ where + open Related.EquationalReasoning helper : ∀ y → (x ≡ f₁ y) ↔ (x ≡ f₂ y) helper y rewrite f₁≗f₂ y = ↔-refl @@ -205,7 +209,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s remove-linear {xs} m = mk↔ₛ′ t f t∘f f∘t where open _≃_ - open P.≡-Reasoning renaming (_∎ to _∎′) + open P.≡-Reasoning position⊸m : ∀ {s} → Position C₂ (shape⊸ m s) ≃ Position C₁ s position⊸m = ↔⇒≃ (position⊸ m) @@ -259,7 +263,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s P.subst (P ∘ proj₂ xs) P.refl p ≡⟨⟩ - p ∎′) + p ∎) ) t∘f : t ∘ f ≗ id @@ -279,7 +283,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s (P.trans-symˡ (right-inverse-of position⊸m _)) ⟩ P.subst (P ∘ proj₂ xs) P.refl p ≡⟨⟩ - p ∎′) + p ∎) ) -- Linear endomorphisms are identity functions if bag equality is used. @@ -290,6 +294,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x} where linear-identity {xs} m {x} = x ∈ ⟪ m ⟫⊸ xs ↔⟨ remove-linear (_≡_ x) m ⟩ x ∈ xs ∎ + where open Related.EquationalReasoning -- If join can be expressed using a linear morphism (in a certain -- way), then it can be absorbed by the predicate. @@ -307,4 +312,6 @@ module _ {s₁ s₂ s₃ p₁ p₂ p₃} ◇ C₃ P (⟪ join ⟫⊸ xss′) ↔⟨ remove-linear P join ⟩ ◇ (C₁ C.∘ C₂) P xss′ ↔⟨ SK-sym $ flatten P xss ⟩ ◇ C₁ (◇ C₂ P) xss ∎ - where xss′ = Inverse.from (Composition.correct C₁ C₂) xss + where + open Related.EquationalReasoning + xss′ = Inverse.from (Composition.correct C₁ C₂) xss diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda index af06d57486..9a4b938950 100644 --- a/src/Data/Integer/Divisibility/Signed.agda +++ b/src/Data/Integer/Divisibility/Signed.agda @@ -30,6 +30,7 @@ open import Relation.Binary.PropositionalEquality import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Nullary.Decidable using (yes; no) import Relation.Nullary.Decidable as DEC +open import Relation.Binary.Reasoning.Syntax ------------------------------------------------------------------------ -- Type @@ -118,15 +119,11 @@ open _∣_ using (quotient) public -- Divisibility reasoning module ∣-Reasoning where - private - module Base = PreorderReasoning ∣-preorder + private module Base = PreorderReasoning ∣-preorder - open Base public - hiding (step-∼; step-≈; step-≈˘) + open Base public hiding (step-∼; step-≈; step-≈˘) - infixr 2 step-∣ - step-∣ = Base.step-∼ - syntax step-∣ x y∣z x∣y = x ∣⟨ x∣y ⟩ y∣z + open ∣-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public ------------------------------------------------------------------------ -- Other properties of _∣_ diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 21b3f3d71c..28b3bc3414 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -365,7 +365,7 @@ i≮i = <-irrefl refl module ≤-Reasoning where open import Relation.Binary.Reasoning.Base.Triple ≤-isPreorder - <-irrefl + <-asym <-trans (resp₂ _<_) <⇒≤ diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index 889efe96d9..0acef52dcb 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -37,11 +37,13 @@ open import Function.Related.TypeIsomorphisms open import Function.Properties.Inverse using (↔-sym; ↔-trans; to-from) open import Level using (Level) open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions using (Trans) open import Relation.Binary.Bundles using (Preorder; Setoid) import Relation.Binary.Reasoning.Setoid as EqR import Relation.Binary.Reasoning.Preorder as PreorderReasoning open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; _≗_; refl) +open import Relation.Binary.Reasoning.Syntax open import Relation.Nullary open import Data.List.Membership.Propositional.Properties @@ -90,29 +92,22 @@ bag-=⇒ xs≈ys = ↔⇒ xs≈ys ------------------------------------------------------------------------ -- "Equational" reasoning for _⊆_ along with an additional relatedness -module ⊆-Reasoning where - private - module PreOrder {a} {A : Set a} = PreorderReasoning (⊆-preorder A) +module ⊆-Reasoning {A : Set a} where + private module Base = PreorderReasoning (⊆-preorder A) - open PreOrder public + open Base public hiding (step-≈; step-≈˘; step-∼) + renaming (∼-go to ⊆-go) - infixr 2 step-∼ step-⊆ - infix 1 step-∈ + open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) public + open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ⊆-go public - step-⊆ = PreOrder.step-∼ + module _ {k : Related.ForwardKind} where + ∼-go : Trans _∼[ ⌊ k ⌋→ ]_ _IsRelatedTo_ _IsRelatedTo_ + ∼-go eq = ⊆-go (⇒→ eq) - step-∈ : ∀ x {xs ys : List A} → - xs IsRelatedTo ys → x ∈ xs → x ∈ ys - step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs + open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public - step-∼ : ∀ {k} xs {ys zs : List A} → - ys IsRelatedTo zs → xs ∼[ ⌊ k ⌋→ ] ys → xs IsRelatedTo zs - step-∼ xs ys⊆zs xs≈ys = step-⊆ xs ys⊆zs (⇒→ xs≈ys) - - syntax step-∈ x xs⊆ys x∈xs = x ∈⟨ x∈xs ⟩ xs⊆ys - syntax step-∼ xs ys⊆zs xs≈ys = xs ∼⟨ xs≈ys ⟩ ys⊆zs - syntax step-⊆ xs ys⊆zs xs⊆ys = xs ⊆⟨ xs⊆ys ⟩ ys⊆zs ------------------------------------------------------------------------ -- Congruence lemmas diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index aaea103279..28cf25d9ed 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -16,6 +16,7 @@ open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Transitive) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) import Relation.Binary.Reasoning.Setoid as EqReasoning +open import Relation.Binary.Reasoning.Syntax ------------------------------------------------------------------------ -- An inductive definition of permutation @@ -73,16 +74,15 @@ data _↭_ : Rel (List A) a where module PermutationReasoning where - private - module Base = EqReasoning ↭-setoid + private module Base = EqReasoning ↭-setoid - open EqReasoning ↭-setoid public - hiding (step-≈; step-≈˘) + open Base public hiding (step-≈; step-≈˘) - infixr 2 step-↭ step-↭˘ step-swap step-prep + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public - step-↭ = Base.step-≈ - step-↭˘ = Base.step-≈˘ + -- Some extra combinators that allow us to skip certain elements + + infixr 2 step-swap step-prep -- Skip reasoning on the first element step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs → @@ -94,7 +94,5 @@ module PermutationReasoning where xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel)) - syntax step-↭ x y↭z x↭y = x ↭⟨ x↭y ⟩ y↭z - syntax step-↭˘ x y↭z y↭x = x ↭˘⟨ y↭x ⟩ y↭z syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index fe3f095ee5..0d375226db 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -6,11 +6,13 @@ {-# OPTIONS --cubical-compatible --safe #-} +open import Function.Base using (_∘′_) 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.Definitions using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Reasoning.Syntax module Data.List.Relation.Binary.Permutation.Setoid {a ℓ} (S : Setoid a ℓ) where @@ -86,24 +88,16 @@ steps (trans xs↭ys ys↭zs) = steps xs↭ys + steps ys↭zs module PermutationReasoning where - private - module Base = SetoidReasoning ↭-setoid + private module Base = SetoidReasoning ↭-setoid - open SetoidReasoning ↭-setoid public - hiding (step-≈; step-≈˘) + open Base public hiding (step-≈; step-≈˘) - infixr 2 step-↭ step-↭˘ step-≋ step-≋˘ step-swap step-prep + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (Base.∼-go ∘′ refl) ≋-sym public - step-↭ = Base.step-≈ - step-↭˘ = Base.step-≈˘ + -- Some extra combinators that allow us to skip certain elements - -- Step with pointwise list equality - step-≋ : ∀ x {y z} → y IsRelatedTo z → x ≋ y → x IsRelatedTo z - step-≋ x (relTo y↔z) x≋y = relTo (trans (refl x≋y) y↔z) - - -- Step with flipped pointwise list equality - step-≋˘ : ∀ x {y z} → y IsRelatedTo z → y ≋ x → x IsRelatedTo z - step-≋˘ x y↭z y≋x = x ≋⟨ ≋-sym y≋x ⟩ y↭z + infixr 2 step-swap step-prep -- Skip reasoning on the first element step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs → @@ -115,9 +109,5 @@ module PermutationReasoning where xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs step-swap x y xs rel xs↭ys = relTo (trans (swap Eq.refl Eq.refl xs↭ys) (begin rel)) - syntax step-↭ x y↭z x↭y = x ↭⟨ x↭y ⟩ y↭z - syntax step-↭˘ x y↭z y↭x = x ↭˘⟨ y↭x ⟩ y↭z - syntax step-≋ x y↭z x≋y = x ≋⟨ x≋y ⟩ y↭z - syntax step-≋˘ x y↭z y≋x = x ≋˘⟨ y≋x ⟩ y↭z syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index abf5bdc86f..0d11079ad0 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -32,6 +32,7 @@ open import Relation.Binary.Definitions open import Relation.Binary.Bundles using (Setoid; Preorder) open import Relation.Binary.Structures using (IsPreorder) import Relation.Binary.Reasoning.Preorder as PreorderReasoning +open import Relation.Binary.Reasoning.Syntax open Setoid using (Carrier) @@ -112,31 +113,15 @@ module _ (S : Setoid a ℓ) where ------------------------------------------------------------------------ module ⊆-Reasoning (S : Setoid a ℓ) where + open Membership S using (_∈_) - open Setoid S renaming (Carrier to A) - open Subset S - open Membership S - - private - module Base = PreorderReasoning (⊆-preorder S) - - open Base public - hiding (step-∼; step-≈; step-≈˘) - - infixr 2 step-⊆ step-≋ step-≋˘ - infix 1 step-∈ - - step-∈ : ∀ x {xs ys} → xs IsRelatedTo ys → x ∈ xs → x ∈ ys - step-∈ x xs⊆ys x∈xs = (begin xs⊆ys) x∈xs + private module Base = PreorderReasoning (⊆-preorder S) - step-⊆ = Base.step-∼ - step-≋ = Base.step-≈ - step-≋˘ = Base.step-≈˘ + open Base public hiding (step-∼; step-≈; step-≈˘) - syntax step-∈ x xs⊆ys x∈xs = x ∈⟨ x∈xs ⟩ xs⊆ys - syntax step-⊆ xs ys⊆zs xs⊆ys = xs ⊆⟨ xs⊆ys ⟩ ys⊆zs - syntax step-≋ xs ys⊆zs xs≋ys = xs ≋⟨ xs≋ys ⟩ ys⊆zs - syntax step-≋˘ xs ys⊆zs xs≋ys = xs ≋˘⟨ xs≋ys ⟩ ys⊆zs + open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → Base.begin x) public + open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ Base.≈-go public ------------------------------------------------------------------------ -- Relationship with other binary relations diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 6109106b26..de9587d22c 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -27,13 +27,7 @@ open import Function.Base using (_∘_; _$_; id) open import Function.Definitions open import Function.Consequences.Propositional open import Level using (0ℓ) -open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Binary.Bundles - using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; TotalOrder; DecTotalOrder) -open import Relation.Binary.Definitions - using (Decidable; Irreflexive; Transitive; Reflexive; Antisymmetric; Total; Trichotomous; tri≈; tri<; tri>) -open import Relation.Binary.Structures - using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder) +open import Relation.Binary open import Relation.Binary.Consequences open import Relation.Binary.Morphism import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism @@ -371,6 +365,9 @@ toℕ-isMonomorphism-< = record <-trans (odd; tri≈; _Respectsʳ_; _Respectsˡ_; _Respects₂_) +open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Binary.Morphism.Structures import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms open import Relation.Nullary.Decidable.Core as Dec using (yes; no; recompute; map′; _×-dec_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Binary.Reasoning.Syntax open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ @@ -136,11 +131,14 @@ mkℚ+-pos (suc n) (suc d) = _ -- Numerator and denominator equality ------------------------------------------------------------------------ +drop-*≡* : p ≃ q → ↥ p ℤ.* ↧ q ≡ ↥ q ℤ.* ↧ p +drop-*≡* (*≡* eq) = eq + ≡⇒≃ : _≡_ ⇒ _≃_ -≡⇒≃ refl = refl +≡⇒≃ refl = *≡* refl ≃⇒≡ : _≃_ ⇒ _≡_ -≃⇒≡ {x = mkℚ n₁ d₁ c₁} {y = mkℚ n₂ d₂ c₂} eq = helper +≃⇒≡ {x = mkℚ n₁ d₁ c₁} {y = mkℚ n₂ d₂ c₂} (*≡* eq) = helper where open ≡-Reasoning @@ -165,6 +163,9 @@ mkℚ+-pos (suc n) (suc d) = _ ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq ... | refl = refl +≃-sym : Symmetric _≃_ +≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡ + ------------------------------------------------------------------------ -- Properties of ↥ ------------------------------------------------------------------------ @@ -176,6 +177,9 @@ mkℚ+-pos (suc n) (suc d) = _ p≡0⇒↥p≡0 : ∀ p → p ≡ 0ℚ → ↥ p ≡ 0ℤ p≡0⇒↥p≡0 p refl = refl +↥p≡↥q≡0⇒p≡q : ∀ p q → ↥ p ≡ 0ℤ → ↥ q ≡ 0ℤ → p ≡ q +↥p≡↥q≡0⇒p≡q p q ↥p≡0 ↥q≡0 = trans (↥p≡0⇒p≡0 p ↥p≡0) (sym (↥p≡0⇒p≡0 q ↥q≡0)) + ------------------------------------------------------------------------ -- Basic properties of sign predicates ------------------------------------------------------------------------ @@ -418,7 +422,7 @@ private ↧ᵘ-toℚᵘ p@record{} = refl toℚᵘ-injective : Injective _≡_ _≃ᵘ_ toℚᵘ -toℚᵘ-injective {x@record{}} {y@record{}} (*≡* eq) = ≃⇒≡ eq +toℚᵘ-injective {x@record{}} {y@record{}} (*≡* eq) = ≃⇒≡ (*≡* eq) fromℚᵘ-injective : Injective _≃ᵘ_ _≡_ fromℚᵘ fromℚᵘ-injective {p@record{}} {q@record{}} = /-injective-≃ p q @@ -497,7 +501,7 @@ private ≤-trans = ≤-Monomorphism.trans ℚᵘ.≤-trans ≤-antisym : Antisymmetric _≡_ _≤_ -≤-antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (ℤ.≤-antisym le₁ le₂) +≤-antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (*≡* (ℤ.≤-antisym le₁ le₂)) ≤-total : Total _≤_ ≤-total p q = [ inj₁ ∘ *≤* , inj₂ ∘ *≤* ]′ (ℤ.≤-total (↥ p ℤ.* ↧ q) (↥ q ℤ.* ↧ p)) @@ -606,7 +610,7 @@ toℚᵘ-isOrderMonomorphism-< = record ≰⇒> {p} {q} p≰q = *<* (ℤ.≰⇒> (p≰q ∘ *≤*)) <⇒≢ : _<_ ⇒ _≢_ -<⇒≢ {p} {q} (*<* p?_ = flip _ ≮ ≢ > = tri> (≮ ∘ drop-*<*) (≢ ∘ ≡⇒≃) (*<* >) +... | tri< < ≢ ≯ = tri< (*<* <) (≢ ∘ drop-*≡* ∘ ≡⇒≃) (≯ ∘ drop-*<*) +... | tri≈ ≮ ≡ ≯ = tri≈ (≮ ∘ drop-*<*) (≃⇒≡ (*≡* ≡)) (≯ ∘ drop-*<*) +... | tri> ≮ ≢ > = tri> (≮ ∘ drop-*<*) (≢ ∘ drop-*≡* ∘ ≡⇒≃) (*<* >) <-irrelevant : Irrelevant _<_ <-irrelevant (*<* p?_ = flip _?_ = flip _