diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dcdb3d924..0889f2da79 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -849,6 +849,7 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` + ### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder` * Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its @@ -989,6 +990,53 @@ Non-backwards compatible changes Relation.Binary.Reasoning.PartialOrder ``` +### More modular design of equational reasoning. + +* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports + a range of modules containing pre-existing reasoning combinator syntax. + +* This makes it possible to add new or rename existing reasoning combinators to a + pre-existing `Reasoning` module in just a couple of lines + (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`) + +* One pre-requisite for that is that `≡-Reasoning` has been moved from + `Relation.Binary.PropositionalEquality.Core` (which shouldn't be + imported anyway as it's a `Core` module) to + `Relation.Binary.PropositionalEquality.Properties`. + It is still exported by `Relation.Binary.PropositionalEquality`. + +### Renaming of symmetric combinators for equational reasoning + +* We've had various complaints about the symmetric version of reasoning combinators + that use the syntax `_R˘⟨_⟩_` for some relation `R`, (e.g. `_≡˘⟨_⟩_` and `_≃˘⟨_⟩_`) + introduced in `v1.0`. In particular: + 1. The symbol `˘` is hard to type. + 2. The symbol `˘` doesn't convey the direction of the equality + 3. The left brackets aren't vertically aligned with the left brackets of the non-symmetric version. + +* To address these problems we have renamed all the symmetric versions of the + combinators from `_R˘⟨_⟩_` to `_R⟨_⟨_` (the direction of the last bracket is flipped + to indicate the quality goes from right to left). + +* The old combinators still exist but have been deprecated. However due to + [Agda issue #5617](https://github.com/agda/agda/issues/5617), the deprecation warnings + don't fire correctly. We will not remove the old combinators before the above issue is + addressed. However, we still encourage migrating to the new combinators! + +* On a Linux-based system, the following command was used to globally migrate all uses of the + old combinators to the new ones in the standard library itself. + It *may* be useful when trying to migrate your own code: + ```bash + find . -type f -name "*.agda" -print0 | xargs -0 sed -i -e 's/˘⟨\(.*\)⟩/⟨\1⟨/g' + ``` + USUAL CAVEATS: It has not been widely tested and the standard library developers are not + responsible for the results of this command. It is strongly recommended you back up your + work before you attempt to run it. + +* NOTE: this refactoring may require some extra bracketing around the operator `_⟨_⟩_` from + `Function.Base` if the `_⟨_⟩_` operator is used within the reasoning proof. The symptom + for this is a `Don't know how to parse` error. + ### Other * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used @@ -1228,21 +1276,6 @@ Major improvements * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module. * In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_` - -### More modular design of equational reasoning. - -* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports - a range of modules containing pre-existing reasoning combinator syntax. - -* This makes it possible to add new or rename existing reasoning combinators to a - pre-existing `Reasoning` module in just a couple of lines - (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`) - -* One pre-requisite for that is that `≡-Reasoning` has been moved from - `Relation.Binary.PropositionalEquality.Core` (which shouldn't be - imported anyway as it's a `Core` module) to - `Relation.Binary.PropositionalEquality.Properties`. - It is still exported by `Relation.Binary.PropositionalEquality`. Deprecated modules ------------------ diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda index e602932827..390a48d58f 100644 --- a/README/Data/Fin/Relation/Unary/Top.agda +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -76,8 +76,8 @@ opposite-prop {suc n} i with view i ... | ‵fromℕ rewrite toℕ-fromℕ n | n∸n≡0 n = refl ... | ‵inject₁ j = begin suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩ - suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 (toℕ ⊖-monoʳ-≥-≤ (suc n) {suc m} {suc o} (s≤s m≤o) = begin suc n ⊖ suc m ≡⟨ [1+m]⊖[1+n]≡m⊖n n m ⟩ n ⊖ m ≤⟨ ⊖-monoʳ-≥-≤ n m≤o ⟩ - n ⊖ o ≡˘⟨ [1+m]⊖[1+n]≡m⊖n n o ⟩ + n ⊖ o ≡⟨ [1+m]⊖[1+n]≡m⊖n n o ⟨ suc n ⊖ suc o ∎ where open ≤-Reasoning ⊖-monoˡ-≤ : ∀ n → (_⊖ n) Preserves ℕ._≤_ ⟶ _≤_ @@ -759,12 +759,12 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> ⊖-monoˡ-≤ (suc n) {_} {suc o} z≤n = begin zero ⊖ suc n ≤⟨ ⊖-monoʳ-≥-≤ 0 (ℕ.n≤1+n n) ⟩ zero ⊖ n ≤⟨ ⊖-monoˡ-≤ n z≤n ⟩ - o ⊖ n ≡˘⟨ [1+m]⊖[1+n]≡m⊖n o n ⟩ + o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨ suc o ⊖ suc n ∎ where open ≤-Reasoning ⊖-monoˡ-≤ (suc n) {suc m} {suc o} (s≤s m≤o) = begin suc m ⊖ suc n ≡⟨ [1+m]⊖[1+n]≡m⊖n m n ⟩ m ⊖ n ≤⟨ ⊖-monoˡ-≤ n m≤o ⟩ - o ⊖ n ≡˘⟨ [1+m]⊖[1+n]≡m⊖n o n ⟩ + o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨ suc o ⊖ suc n ∎ where open ≤-Reasoning ⊖-monoʳ->-< : ∀ p → (p ⊖_) Preserves ℕ._>_ ⟶ _<_ @@ -777,19 +777,19 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> ⊖-monoʳ->-< (suc p) {suc m} {suc n} (s-< p m_ *-monoˡ-<-neg i@(-[1+ _ ]) {j} {k} j j *-cancelˡ-<-nonPos {i} {j} +0 (+<+ ()) *-cancelˡ-<-nonPos {i} {j} k@(-[1+ _ ]) ki>= pam as) unfold-⊛ fs as = begin fs ⊛ as - ≡˘⟨ concatMap-cong (λ f → P.cong (map f) (concatMap-pure as)) fs ⟩ + ≡⟨ concatMap-cong (λ f → P.cong (map f) (concatMap-pure as)) fs ⟨ concatMap (λ f → map f (concatMap pure as)) fs ≡⟨ concatMap-cong (λ f → map-concatMap f pure as) fs ⟩ concatMap (λ f → concatMap (λ x → pure (f x)) as) fs @@ -224,7 +224,7 @@ module Applicative where right-distributive fs₁ fs₂ xs = begin (fs₁ ∣ fs₂) ⊛ xs ≡⟨ unfold-⊛ (fs₁ ∣ fs₂) xs ⟩ (fs₁ ∣ fs₂ >>= pam xs) ≡⟨ MonadProperties.right-distributive fs₁ fs₂ (pam xs) ⟩ - (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs) ≡˘⟨ P.cong₂ _∣_ (unfold-⊛ fs₁ xs) (unfold-⊛ fs₂ xs) ⟩ + (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs) ≡⟨ P.cong₂ _∣_ (unfold-⊛ fs₁ xs) (unfold-⊛ fs₂ xs) ⟨ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs) ∎ -- _⊛_ does not distribute over _∣_ from the left. @@ -251,7 +251,7 @@ module Applicative where (xs : List A) (f : A → B) (fs : B → List C) → (pam xs f >>= fs) ≡ (xs >>= λ x → fs (f x)) pam-lemma xs f fs = begin - (pam xs f >>= fs) ≡˘⟨ MP.associative xs (pure ∘ f) fs ⟩ + (pam xs f >>= fs) ≡⟨ MP.associative xs (pure ∘ f) fs ⟨ (xs >>= λ x → pure (f x) >>= fs) ≡⟨ MP.cong (refl {x = xs}) (λ x → MP.left-identity (f x) fs) ⟩ (xs >>= λ x → fs (f x)) ∎ @@ -272,7 +272,7 @@ module Applicative where (pam fs _∘′_ >>= pam gs >>= pam xs) ≡⟨ MP.cong (pam-lemma fs _∘′_ (pam gs)) (λ _ → refl) ⟩ ((fs >>= λ f → pam gs (f ∘′_)) >>= pam xs) - ≡˘⟨ MP.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟩ + ≡⟨ MP.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟨ (fs >>= λ f → pam gs (f ∘′_) >>= pam xs) ≡⟨ MP.cong (refl {x = fs}) (λ f → pam-lemma gs (f ∘′_) (pam xs)) ⟩ (fs >>= λ f → gs >>= λ g → pam xs (f ∘′ g)) @@ -282,9 +282,9 @@ module Applicative where (fs >>= λ f → gs >>= λ g → pam (pam xs g) f) ≡⟨ MP.cong (refl {x = fs}) (λ f → MP.associative gs (pam xs) (pure ∘ f)) ⟩ (fs >>= pam (gs >>= pam xs)) - ≡˘⟨ unfold-⊛ fs (gs >>= pam xs) ⟩ + ≡⟨ unfold-⊛ fs (gs >>= pam xs) ⟨ fs ⊛ (gs >>= pam xs) - ≡˘⟨ P.cong (fs ⊛_) (unfold-⊛ gs xs) ⟩ + ≡⟨ P.cong (fs ⊛_) (unfold-⊛ gs xs) ⟨ fs ⊛ (gs ⊛ xs) ∎ @@ -304,5 +304,5 @@ module Applicative where MP.left-identity x (pure ∘ f)) ⟩ (fs >>= λ f → pure (f x)) ≡⟨⟩ (pam fs (_$′ x)) ≡⟨ P.sym $ MP.left-identity (_$′ x) (pam fs) ⟩ - (pure (_$′ x) >>= pam fs) ≡˘⟨ unfold-⊛ (pure (_$′ x)) fs ⟩ + (pure (_$′ x) >>= pam fs) ≡⟨ unfold-⊛ (pure (_$′ x)) fs ⟨ pure (_$′ x) ⊛ fs ∎ diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 78fc03f865..5bd47dc763 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -280,7 +280,7 @@ module _ (f : A → B → C) where cartesianProductWith-distribʳ-++ (x ∷ xs) ys zs = begin prod (x ∷ xs ++ ys) zs ≡⟨⟩ map (f x) zs ++ prod (xs ++ ys) zs ≡⟨ cong (map (f x) zs ++_) (cartesianProductWith-distribʳ-++ xs ys zs) ⟩ - map (f x) zs ++ prod xs zs ++ prod ys zs ≡˘⟨ ++-assoc (map (f x) zs) (prod xs zs) (prod ys zs) ⟩ + map (f x) zs ++ prod xs zs ++ prod ys zs ≡⟨ ++-assoc (map (f x) zs) (prod xs zs) (prod ys zs) ⟨ (map (f x) zs ++ prod xs zs) ++ prod ys zs ≡⟨⟩ prod (x ∷ xs) zs ++ prod ys zs ∎ @@ -590,7 +590,7 @@ map-concatMap f g xs = begin map f (concatMap g xs) ≡⟨⟩ map f (concat (map g xs)) - ≡˘⟨ concat-map (map g xs) ⟩ + ≡⟨ concat-map (map g xs) ⟨ concat (map (map f) (map g xs)) ≡⟨ cong concat {x = map (map f) (map g xs)} diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda index f842ae8087..31ab6941ac 100644 --- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda +++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda @@ -96,7 +96,7 @@ module ⊆-Reasoning {A : Set a} where private module Base = PreorderReasoning (⊆-preorder A) open Base public - hiding (step-≈; step-≈˘; step-∼; step-≲) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-∼; step-≲) renaming (≲-go to ⊆-go) open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → begin x) public @@ -199,7 +199,7 @@ module _ {k} {A B : Set a} {fs gs : List (A → B)} {xs ys} where x ∈ (fs >>= λ f → xs >>= λ x → pure (f x)) ∼⟨ >>=-cong fs≈gs (λ f → >>=-cong xs≈ys λ x → K-refl) ⟩ x ∈ (gs >>= λ g → ys >>= λ y → pure (g y)) - ≡˘⟨ P.cong (x ∈_) (Applicative.unfold-⊛ gs ys) ⟩ + ≡⟨ P.cong (x ∈_) (Applicative.unfold-⊛ gs ys) ⟨ x ∈ (gs ⊛ ys) ∎ where open Related.EquationalReasoning @@ -284,7 +284,7 @@ empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here refl) (xs₂ >>= pure ∘ f)) ≈⟨ >>=-left-distributive fs ⟩ (fs >>= λ f → xs₁ >>= pure ∘ f) ++ - (fs >>= λ f → xs₂ >>= pure ∘ f) ≡˘⟨ P.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟩ + (fs >>= λ f → xs₂ >>= pure ∘ f) ≡⟨ P.cong₂ _++_ (Applicative.unfold-⊛ fs xs₁) (Applicative.unfold-⊛ fs xs₂) ⟨ (fs ⊛ xs₁) ++ (fs ⊛ xs₂) ∎ where open EqR ([ bag ]-Equality B) @@ -592,7 +592,7 @@ drop-cons {x = x} {xs} {ys} x∷xs≈x∷ys = ... | zs₁ , zs₂ , p rewrite p = begin x ∷ xs <⟨ ∼bag⇒↭ (drop-cons (↔-trans eq (comm zs₁ (x ∷ zs₂)))) ⟩ x ∷ (zs₂ ++ zs₁) <⟨ ++-comm zs₂ zs₁ ⟩ - x ∷ (zs₁ ++ zs₂) ↭˘⟨ shift x zs₁ zs₂ ⟩ + x ∷ (zs₁ ++ zs₂) ↭⟨ shift x zs₁ zs₂ ⟨ zs₁ ++ x ∷ zs₂ ∎ where open CommutativeMonoid (commutativeMonoid bag A) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda index 28cf25d9ed..c41793d28a 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda @@ -76,9 +76,11 @@ module PermutationReasoning where private module Base = EqReasoning ↭-setoid - open Base public hiding (step-≈; step-≈˘) + open Base public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) + renaming (≈-go to ↭-go) - open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public -- Some extra combinators that allow us to skip certain elements diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 1b33a771a0..781de1cc36 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -243,7 +243,7 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl ++-comm [] ys = ↭-sym (++-identityʳ ys) ++-comm (x ∷ xs) ys = begin x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ - x ∷ ys ++ xs ↭˘⟨ shift x ys xs ⟩ + x ∷ ys ++ xs ↭⟨ shift x ys xs ⟨ ys ++ (x ∷ xs) ∎ ++-isMagma : IsMagma {A = List A} _↭_ _++_ @@ -296,7 +296,7 @@ module _ {a} {A : Set a} where shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs shifts xs ys {zs} = begin - xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩ + xs ++ ys ++ zs ↭⟨ ++-assoc xs ys zs ⟨ (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩ (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩ ys ++ xs ++ zs ∎ @@ -330,7 +330,7 @@ drop-∷ = drop-mid [] [] ↭-reverse [] = ↭-refl ↭-reverse (x ∷ xs) = begin reverse (x ∷ xs) ≡⟨ Lₚ.unfold-reverse x xs ⟩ - reverse xs ∷ʳ x ↭˘⟨ ∷↭∷ʳ x (reverse xs) ⟩ + reverse xs ∷ʳ x ↭⟨ ∷↭∷ʳ x (reverse xs) ⟨ x ∷ reverse xs ↭⟨ prep x (↭-reverse xs) ⟩ x ∷ xs ∎ where open PermutationReasoning @@ -349,7 +349,7 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where ... | true | rec | _ = prep x rec ... | false | _ | rec = begin y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩ - y ∷ x ∷ xs ++ ys ↭˘⟨ shift y (x ∷ xs) ys ⟩ - (x ∷ xs) ++ y ∷ ys ≡˘⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟩ + y ∷ x ∷ xs ++ ys ↭⟨ shift y (x ∷ xs) ys ⟨ + (x ∷ xs) ++ y ∷ ys ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨ x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda index 0d375226db..edcf62b6da 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda @@ -90,10 +90,12 @@ module PermutationReasoning where private module Base = SetoidReasoning ↭-setoid - open Base public hiding (step-≈; step-≈˘) + open Base public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) + renaming (≈-go to ↭-go) - open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ Base.∼-go ↭-sym public - open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (Base.∼-go ∘′ refl) ≋-sym public + open ↭-syntax _IsRelatedTo_ _IsRelatedTo_ ↭-go ↭-sym public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ (↭-go ∘′ refl) ≋-sym public -- Some extra combinators that allow us to skip certain elements diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index e09251caf5..3af753e826 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -200,7 +200,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin ++-comm [] ys = ↭-sym (++-identityʳ ys) ++-comm (x ∷ xs) ys = begin x ∷ xs ++ ys <⟨ ++-comm xs ys ⟩ - x ∷ ys ++ xs ↭˘⟨ ↭-shift ys xs ⟩ + x ∷ ys ++ xs ↭⟨ ↭-shift ys xs ⟨ ys ++ (x ∷ xs) ∎ -- Structures @@ -262,7 +262,7 @@ inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (↭-prep _ xs↭zs)) (++⁺ʳ _ ws shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs shifts xs ys {zs} = begin - xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩ + xs ++ ys ++ zs ↭⟨ ++-assoc xs ys zs ⟨ (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩ (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩ ys ++ xs ++ zs ∎ @@ -297,19 +297,19 @@ dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl helper {_ ∷ as} {_ ∷ bs} (prep _ as↭bs) [] [] {ys} {zs} (_ ∷ ys≋as) (_ ∷ zs≋bs) = begin ys ≋⟨ ys≋as ⟩ as ↭⟨ as↭bs ⟩ - bs ≋˘⟨ zs≋bs ⟩ + bs ≋⟨ zs≋bs ⟨ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep a≈b as↭bs) [] (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ as ↭⟨ as↭bs ⟩ - bs ≋˘⟨ ≋₂ ⟩ + bs ≋⟨ ≋₂ ⟨ xs ++ v ∷ zs ↭⟨ shift (lemma ≈₁ a≈b ≈₂) xs zs ⟩ x ∷ xs ++ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep v≈w p) (w ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ ws ++ ys ↭⟨ ↭-sym (shift (lemma ≈₂ (≈-sym v≈w) ≈₁) ws ys) ⟩ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩ as ↭⟨ p ⟩ - bs ≋˘⟨ ≋₂ ⟩ + bs ≋⟨ ≋₂ ⟨ zs ∎ helper {_ ∷ as} {_ ∷ bs} (prep w≈x p) (w ∷ ws) (x ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin w ∷ ws ++ ys ↭⟨ prep (lemma ≈₁ w≈x ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩ @@ -317,12 +317,12 @@ dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈x y≈v p) [] [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ a ∷ as ↭⟨ prep (≈-trans (≈-trans (≈-trans y≈v (≈-sym ≈₂)) ≈₁) v≈x) p ⟩ - b ∷ bs ≋˘⟨ ≋₂ ⟩ + b ∷ bs ≋⟨ ≋₂ ⟨ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ a ∷ as ↭⟨ prep y≈w p ⟩ - _ ∷ bs ≋˘⟨ ≈₂ ∷ tail ≋₂ ⟩ + _ ∷ bs ≋⟨ ≈₂ ∷ tail ≋₂ ⟨ x ∷ zs ∎ helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin ys ≋⟨ ≋₁ ⟩ @@ -455,8 +455,8 @@ module _ {ℓ} {R : Rel A ℓ} (R? : B.Decidable R) where ... | true | rec | _ = ↭-prep x rec ... | false | _ | rec = begin y ∷ merge R? (x ∷ xs) ys <⟨ rec ⟩ - y ∷ x ∷ xs ++ ys ↭˘⟨ ↭-shift (x ∷ xs) ys ⟩ - (x ∷ xs) ++ y ∷ ys ≡˘⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟩ + y ∷ x ∷ xs ++ ys ↭⟨ ↭-shift (x ∷ xs) ys ⟨ + (x ∷ xs) ++ y ∷ ys ≡⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟨ x ∷ xs ++ y ∷ ys ∎ where open PermutationReasoning @@ -497,7 +497,7 @@ module _ {_∙_ : Op₂ A} {ε : A} (isCmonoid : IsCommutativeMonoid _≈_ _∙_ foldr-commMonoid (prep x≈y xs↭ys) = ∙-cong x≈y (foldr-commMonoid xs↭ys) foldr-commMonoid (swap {xs} {ys} {x} {y} {x′} {y′} x≈x′ y≈y′ xs↭ys) = S.begin x ∙ (y ∙ foldr _∙_ ε xs) S.≈⟨ ∙-congˡ (∙-congˡ (foldr-commMonoid xs↭ys)) ⟩ - x ∙ (y ∙ foldr _∙_ ε ys) S.≈˘⟨ assoc x y (foldr _∙_ ε ys) ⟩ + x ∙ (y ∙ foldr _∙_ ε ys) S.≈⟨ assoc x y (foldr _∙_ ε ys) ⟨ (x ∙ y) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (comm x y) ⟩ (y ∙ x) ∙ foldr _∙_ ε ys S.≈⟨ ∙-congʳ (∙-cong y≈y′ x≈x′) ⟩ (y′ ∙ x′) ∙ foldr _∙_ ε ys S.≈⟨ assoc y′ x′ (foldr _∙_ ε ys) ⟩ diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index bb20fd417f..0c344758b7 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -118,7 +118,7 @@ module ⊆-Reasoning (S : Setoid a ℓ) where private module Base = PreorderReasoning (⊆-preorder S) open Base public - hiding (step-≲; step-≈; step-≈˘; step-∼) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼) renaming (≲-go to ⊆-go; ≈-go to ≋-go) open begin-membership-syntax _IsRelatedTo_ _∈_ (λ x → Base.begin x) public diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index b88bdfbe95..e356e9eca1 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -686,7 +686,7 @@ module _ {A B : Set ℓ} {P : B → Set p} {f : A → List B} where Any (λ f → Any (P ∘ f) xs) fs ↔⟨ Any-cong (λ _ → Any-cong (λ _ → pure↔) (_ ∎)) (_ ∎) ⟩ Any (λ f → Any (Any P ∘ pure ∘ f) xs) fs ↔⟨ Any-cong (λ _ → >>=↔ ) (_ ∎) ⟩ Any (λ f → Any P (xs >>= pure ∘ f)) fs ↔⟨ >>=↔ ⟩ - Any P (fs >>= λ f → xs >>= λ x → pure (f x)) ≡˘⟨ P.cong (Any P) (Listₑ.Applicative.unfold-⊛ fs xs) ⟩ + Any P (fs >>= λ f → xs >>= λ x → pure (f x)) ≡⟨ P.cong (Any P) (Listₑ.Applicative.unfold-⊛ fs xs) ⟨ Any P (fs ⊛ xs) ∎ where open Related.EquationalReasoning @@ -706,7 +706,7 @@ module _ {A B : Set ℓ} {P : B → Set p} {f : A → List B} where Any (λ x → Any (λ y → P (x , y)) ys) xs ↔⟨ pure↔ ⟩ Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (pure _,_) ↔⟨ ⊛↔ ⟩ Any (λ x, → Any (P ∘ x,) ys) (pure _,_ ⊛ xs) ↔⟨ ⊛↔ ⟩ - Any P (pure _,_ ⊛ xs ⊛ ys) ≡˘⟨ P.cong (Any P ∘′ (_⊛ ys)) (Listₑ.Applicative.unfold-<$> _,_ xs) ⟩ + Any P (pure _,_ ⊛ xs ⊛ ys) ≡⟨ P.cong (Any P ∘′ (_⊛ ys)) (Listₑ.Applicative.unfold-<$> _,_ xs) ⟨ Any P (xs ⊗ ys) ∎ where open Related.EquationalReasoning diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 9e8976842e..f83bbfc12c 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -156,9 +156,9 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl tail-homo ℕ.zero = refl tail-homo (ℕ.suc ℕ.zero) = refl tail-homo (ℕ.suc (ℕ.suc n)) = begin - tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡˘⟨ tail-suc (fromℕ' n) ⟩ + tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡⟨ tail-suc (fromℕ' n) ⟨ suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩ - fromℕ' (ℕ.suc (n / 2)) ≡˘⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟩ + fromℕ' (ℕ.suc (n / 2)) ≡⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟨ fromℕ' (ℕ.suc (ℕ.suc n) / 2) ∎ fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n @@ -167,7 +167,7 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl split-injective (begin split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ just (n % 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n / 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ - just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ + just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟨ head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ split (fromℕ' (ℕ.suc n)) ∎) where rec-n/2 = fromℕ-helper≡fromℕ' (n / 2) w (ℕₚ.≤-trans (m/n≤m n 2) n≤w) @@ -613,7 +613,7 @@ module ≤-Reasoning where <-≤-trans ≤-<-trans public - hiding (step-≈; step-≈˘) + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨) ------------------------------------------------------------------------ -- Properties of _<ℕ_ diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index fc6ef422b4..d07d22db47 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -66,9 +66,9 @@ open Specification public nCk≡nC[n∸k] : k ≤ n → n C k ≡ n C (n ∸ k) nCk≡nC[n∸k] {k} {n} k≤n = begin-equality n C k ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟩ - n ! / ((n ∸ k) ! * k !) ≡˘⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟩ - n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡˘⟨ nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟩ + n ! / (k ! * (n ∸ k) !) ≡⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟨ + n ! / ((n ∸ k) ! * k !) ≡⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟨ + n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡⟨ nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟨ n C (n ∸ k) ∎ where instance _ = (n ∸ k) !* k !≢0 @@ -78,9 +78,9 @@ nCk≡nC[n∸k] {k} {n} k≤n = begin-equality nCk≡nPk/k! : k ≤ n → n C k ≡ ((n P k) / k !) {{k !≢0}} nCk≡nPk/k! {k} {n} k≤n = begin-equality n C k ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟩ - n ! / ((n ∸ k) ! * k !) ≡˘⟨ m/n/o≡m/[n*o] (n !) ((n ∸ k) !) (k !) ⟩ - (n ! / (n ∸ k) !) / k ! ≡˘⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟩ + n ! / (k ! * (n ∸ k) !) ≡⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟨ + n ! / ((n ∸ k) ! * k !) ≡⟨ m/n/o≡m/[n*o] (n !) ((n ∸ k) !) (k !) ⟨ + (n ! / (n ∸ k) !) / k ! ≡⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟨ (n P k) / k ! ∎ where instance _ = k !≢0 @@ -128,7 +128,7 @@ module _ {n k} (kn⇒nCk≡0 k>n) ⟩ 0 + n C (suc k) ≡⟨⟩ n C (suc k) ≡⟨ k>n⇒nCk≡0 (mn) ⟩ - 0 ≡˘⟨ k>n⇒nCk≡0 (sn) ⟩ + 0 ≡⟨ k>n⇒nCk≡0 (sn) ⟨ suc n C suc k ∎ {- case k≡n, in which case 1+k≡1+n>n -} ... | tri≈ _ k≡n _ rewrite k≡n = begin-equality n C n + n C (suc n) ≡⟨ cong (n C n +_) (k>n⇒nCk≡0 (n<1+n n)) ⟩ n C n + 0 ≡⟨ +-identityʳ (n C n) ⟩ n C n ≡⟨ nCn≡1 n ⟩ - 1 ≡˘⟨ nCn≡1 (suc n) ⟩ + 1 ≡⟨ nCn≡1 (suc n) ⟨ suc n C suc n ∎ {- case k0 (≢-nonZero⁻¹ o)) (≮⇒≥ n≮o) @@ -333,19 +333,19 @@ m q *-cancelˡ-<-nonPos {p} {q} r rp p≮q p≡r p>q = begin f (p ⊓ q) ≡⟨ cong f (p≥q⇒p⊓q≡q (<⇒≤ p>q)) ⟩ - f q ≡˘⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟩ + f q ≡⟨ p≥q⇒p⊓q≡q (<⇒≤ (f-mono-< p>q)) ⟨ f p ⊓ f q ∎ where open ≡-Reasoning @@ -1507,17 +1508,17 @@ mono-<-distrib-⊔ : ∀ {f} → f Preserves _<_ ⟶ _<_ → mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q ... | tri< p p≮q p≡r p>q = begin f (p ⊔ q) ≡⟨ cong f (p≥q⇒p⊔q≡p (<⇒≤ p>q)) ⟩ - f p ≡˘⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟩ + f p ≡⟨ p≥q⇒p⊔q≡p (<⇒≤ (f-mono-< p>q)) ⟨ f p ⊔ f q ∎ where open ≡-Reasoning @@ -1605,7 +1606,7 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl 0≤∣p∣ p@record{} = *≤* (begin (↥ 0ℚ) ℤ.* (↧ ∣ p ∣) ≡⟨ ℤ.*-zeroˡ (↧ ∣ p ∣) ⟩ 0ℤ ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩ - ↥ ∣ p ∣ ≡˘⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟩ + ↥ ∣ p ∣ ≡⟨ ℤ.*-identityʳ (↥ ∣ p ∣) ⟨ ↥ ∣ p ∣ ℤ.* 1ℤ ∎) where open ℤ.≤-Reasoning @@ -1633,8 +1634,8 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl toℚᵘ ∣ p + q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p + q) ⟩ ℚᵘ.∣ toℚᵘ (p + q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-+ p q) ⟩ ℚᵘ.∣ toℚᵘ p ℚᵘ.+ toℚᵘ q ∣ ≤⟨ ℚᵘ.∣p+q∣≤∣p∣+∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ - ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.+ ℚᵘ.∣ toℚᵘ q ∣ ≃˘⟨ ℚᵘ.+-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟩ - toℚᵘ ∣ p ∣ ℚᵘ.+ toℚᵘ ∣ q ∣ ≃˘⟨ toℚᵘ-homo-+ ∣ p ∣ ∣ q ∣ ⟩ + ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.+ ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.+-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ + toℚᵘ ∣ p ∣ ℚᵘ.+ toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-+ ∣ p ∣ ∣ q ∣ ⟨ toℚᵘ (∣ p ∣ + ∣ q ∣) ∎) where open ℚᵘ.≤-Reasoning @@ -1650,8 +1651,8 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl toℚᵘ ∣ p * q ∣ ≃⟨ toℚᵘ-homo-∣-∣ (p * q) ⟩ ℚᵘ.∣ toℚᵘ (p * q) ∣ ≃⟨ ℚᵘ.∣-∣-cong (toℚᵘ-homo-* p q) ⟩ ℚᵘ.∣ toℚᵘ p ℚᵘ.* toℚᵘ q ∣ ≃⟨ ℚᵘ.∣p*q∣≃∣p∣*∣q∣ (toℚᵘ p) (toℚᵘ q) ⟩ - ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.* ℚᵘ.∣ toℚᵘ q ∣ ≃˘⟨ ℚᵘ.*-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟩ - toℚᵘ ∣ p ∣ ℚᵘ.* toℚᵘ ∣ q ∣ ≃˘⟨ toℚᵘ-homo-* ∣ p ∣ ∣ q ∣ ⟩ + ℚᵘ.∣ toℚᵘ p ∣ ℚᵘ.* ℚᵘ.∣ toℚᵘ q ∣ ≃⟨ ℚᵘ.*-cong (toℚᵘ-homo-∣-∣ p) (toℚᵘ-homo-∣-∣ q) ⟨ + toℚᵘ ∣ p ∣ ℚᵘ.* toℚᵘ ∣ q ∣ ≃⟨ toℚᵘ-homo-* ∣ p ∣ ∣ q ∣ ⟨ toℚᵘ (∣ p ∣ * ∣ q ∣) ∎) where open ℚᵘ.≤-Reasoning diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 6348a6ef46..dce11c3f21 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -160,7 +160,7 @@ module ≃-Reasoning = SetoidReasoning ≃-setoid p≃0⇒↥p≡0 : ∀ p → p ≃ 0ℚᵘ → ↥ p ≡ 0ℤ p≃0⇒↥p≡0 p (*≡* eq) = begin - ↥ p ≡˘⟨ ℤ.*-identityʳ (↥ p) ⟩ + ↥ p ≡⟨ ℤ.*-identityʳ (↥ p) ⟨ ↥ p ℤ.* 1ℤ ≡⟨ eq ⟩ 0ℤ ∎ where open ≡-Reasoning @@ -180,14 +180,14 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl -‿cong : Congruent₁ _≃_ (-_) -‿cong {p@record{}} {q@record{}} (*≡* p≡q) = *≡* (begin - ↥(- p) ℤ.* ↧ q ≡˘⟨ ℤ.*-identityˡ (ℤ.- (↥ p) ℤ.* ↧ q) ⟩ - 1ℤ ℤ.* (↥(- p) ℤ.* ↧ q) ≡˘⟨ ℤ.*-assoc 1ℤ (↥ (- p)) (↧ q) ⟩ - (1ℤ ℤ.* ℤ.-(↥ p)) ℤ.* ↧ q ≡˘⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribʳ-* 1ℤ (↥ p)) ⟩ + ↥(- p) ℤ.* ↧ q ≡⟨ ℤ.*-identityˡ (ℤ.- (↥ p) ℤ.* ↧ q) ⟨ + 1ℤ ℤ.* (↥(- p) ℤ.* ↧ q) ≡⟨ ℤ.*-assoc 1ℤ (↥ (- p)) (↧ q) ⟨ + (1ℤ ℤ.* ℤ.-(↥ p)) ℤ.* ↧ q ≡⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribʳ-* 1ℤ (↥ p)) ⟨ ℤ.-(1ℤ ℤ.* ↥ p) ℤ.* ↧ q ≡⟨ cong (ℤ._* ↧ q) (ℤ.neg-distribˡ-* 1ℤ (↥ p)) ⟩ (-1ℤ ℤ.* ↥ p) ℤ.* ↧ q ≡⟨ ℤ.*-assoc ℤ.-1ℤ (↥ p) (↧ q) ⟩ -1ℤ ℤ.* (↥ p ℤ.* ↧ q) ≡⟨ cong (ℤ.-1ℤ ℤ.*_) p≡q ⟩ - -1ℤ ℤ.* (↥ q ℤ.* ↧ p) ≡˘⟨ ℤ.*-assoc ℤ.-1ℤ (↥ q) (↧ p) ⟩ - (-1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡˘⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribˡ-* 1ℤ (↥ q)) ⟩ + -1ℤ ℤ.* (↥ q ℤ.* ↧ p) ≡⟨ ℤ.*-assoc ℤ.-1ℤ (↥ q) (↧ p) ⟨ + (-1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribˡ-* 1ℤ (↥ q)) ⟨ ℤ.-(1ℤ ℤ.* ↥ q) ℤ.* ↧ p ≡⟨ cong (ℤ._* ↧ p) (ℤ.neg-distribʳ-* 1ℤ (↥ q)) ⟩ (1ℤ ℤ.* ↥(- q)) ℤ.* ↧ p ≡⟨ ℤ.*-assoc 1ℤ (ℤ.- (↥ q)) (↧ p) ⟩ 1ℤ ℤ.* (↥(- q) ℤ.* ↧ p) ≡⟨ ℤ.*-identityˡ (↥ (- q) ℤ.* ↧ p) ⟩ @@ -196,7 +196,7 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl neg-mono-< : -_ Preserves _<_ ⟶ _>_ neg-mono-< {p@record{}} {q@record{}} (*<* p?_ = flip __ *-monoˡ-<-neg r {p} {q} p0}} p0 = positive (neg-mono-< (negative⁻¹ r)) @@ -1328,7 +1329,7 @@ private *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → q < p *-cancelˡ-<-nonPos {p} {q} r rp1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1 1/-antimono-≤-pos : ∀ {p q} .{{_ : Positive p}} .{{_ : Positive q}} → p ≤ q → (1/ q) {{pos⇒nonZero q}} ≤ (1/ p) {{pos⇒nonZero p}} 1/-antimono-≤-pos {p} {q} p≤q = begin - 1/q ≃˘⟨ *-identityˡ 1/q ⟩ - 1ℚᵘ * 1/q ≃˘⟨ *-congʳ (*-inverseˡ p) ⟩ + 1/q ≃⟨ *-identityˡ 1/q ⟨ + 1ℚᵘ * 1/q ≃⟨ *-congʳ (*-inverseˡ p) ⟨ (1/p * p) * 1/q ≤⟨ *-monoˡ-≤-nonNeg 1/q (*-monoʳ-≤-nonNeg 1/p p≤q) ⟩ (1/p * q) * 1/q ≃⟨ *-assoc 1/p q 1/q ⟩ 1/p * (q * 1/q) ≃⟨ *-congˡ {1/p} (*-inverseʳ q) ⟩ @@ -1775,7 +1776,7 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ℤ.- ℤ.- (↥ ∣ p ∣ ℤ.* ↧ q) ≡⟨ cong ℤ.-_ (ℤ.neg-distribˡ-* (↥ ∣ p ∣) (↧ q)) ⟩ ℤ.- (↥ p ℤ.* ↧ q) ≡⟨ cong ℤ.-_ ↥p↧q≡↥q↧p ⟩ ℤ.- (↥ q ℤ.* ↧ p) ≡⟨ cong ℤ.-_ (ℤ.neg-distribˡ-* (↥ ∣ q ∣) (↧ p)) ⟩ - ℤ.- ℤ.- (↥ ∣ q ∣ ℤ.* ↧ p) ≡˘⟨ ℤ.neg-involutive _ ⟩ + ℤ.- ℤ.- (↥ ∣ q ∣ ℤ.* ↧ p) ≡⟨ ℤ.neg-involutive _ ⟨ ↥ ∣ q ∣ ℤ.* ↧ p ∎) where open ≡-Reasoning @@ -1807,7 +1808,7 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ∣p∣≡p⇒0≤p {mkℚᵘ (ℤ.+ n) d-1} ∣p∣≡p = *≤* (begin 0ℤ ℤ.* +[1+ d-1 ] ≡⟨ ℤ.*-zeroˡ (ℤ.+ d-1) ⟩ 0ℤ ≤⟨ ℤ.+≤+ ℕ.z≤n ⟩ - ℤ.+ n ≡˘⟨ ℤ.*-identityʳ (ℤ.+ n) ⟩ + ℤ.+ n ≡⟨ ℤ.*-identityʳ (ℤ.+ n) ⟨ ℤ.+ n ℤ.* 1ℤ ∎) where open ℤ.≤-Reasoning @@ -1826,7 +1827,7 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ↥ ∣ (↥p↧q ℤ.+ ↥q↧p) / ↧p↧q ∣ ℤ.* ℤ.+ ↧p↧q ≡⟨⟩ ↥ (ℤ.+ ℤ.∣ ↥p↧q ℤ.+ ↥q↧p ∣ / ↧p↧q) ℤ.* ℤ.+ ↧p↧q ≡⟨ cong (ℤ._* ℤ.+ ↧p↧q) (↥[n/d]≡n (ℤ.+ ℤ.∣ ↥p↧q ℤ.+ ↥q↧p ∣) ↧p↧q) ⟩ ℤ.+ ℤ.∣ ↥p↧q ℤ.+ ↥q↧p ∣ ℤ.* ℤ.+ ↧p↧q ≤⟨ ℤ.*-monoʳ-≤-nonNeg (ℤ.+ ↧p↧q) (ℤ.+≤+ (ℤ.∣i+j∣≤∣i∣+∣j∣ ↥p↧q ↥q↧p)) ⟩ - (ℤ.+ ℤ.∣ ↥p↧q ∣ ℤ.+ ℤ.+ ℤ.∣ ↥q↧p ∣) ℤ.* ℤ.+ ↧p↧q ≡˘⟨ cong₂ (λ h₁ h₂ → (h₁ ℤ.+ h₂) ℤ.* ℤ.+ ↧p↧q) ∣↥p∣↧q≡∣↥p↧q∣ ∣↥q∣↧p≡∣↥q↧p∣ ⟩ + (ℤ.+ ℤ.∣ ↥p↧q ∣ ℤ.+ ℤ.+ ℤ.∣ ↥q↧p ∣) ℤ.* ℤ.+ ↧p↧q ≡⟨ cong₂ (λ h₁ h₂ → (h₁ ℤ.+ h₂) ℤ.* ℤ.+ ↧p↧q) ∣↥p∣↧q≡∣↥p↧q∣ ∣↥q∣↧p≡∣↥q↧p∣ ⟨ (∣↥p∣↧q ℤ.+ ∣↥q∣↧p) ℤ.* ℤ.+ ↧p↧q ≡⟨⟩ (↥∣p∣↧q ℤ.+ ↥∣q∣↧p) ℤ.* ℤ.+ ↧p↧q ≡⟨ cong (ℤ._* ℤ.+ ↧p↧q) (↥[n/d]≡n (↥∣p∣↧q ℤ.+ ↥∣q∣↧p) ↧p↧q) ⟩ ↥ ((↥∣p∣↧q ℤ.+ ↥∣q∣↧p) / ↧p↧q) ℤ.* ℤ.+ ↧p↧q ≡⟨⟩ @@ -1843,9 +1844,9 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) ∣m∣n≡∣mn∣ : ∀ m n → ℤ.+ ℤ.∣ m ∣ ℤ.* ℤ.+ n ≡ ℤ.+ ℤ.∣ m ℤ.* ℤ.+ n ∣ ∣m∣n≡∣mn∣ m n = begin-equality ℤ.+ ℤ.∣ m ∣ ℤ.* ℤ.+ n ≡⟨⟩ - ℤ.+ ℤ.∣ m ∣ ℤ.* ℤ.+ ℤ.∣ ℤ.+ n ∣ ≡˘⟨ ℤ.pos-* ℤ.∣ m ∣ ℤ.∣ ℤ.+ n ∣ ⟩ + ℤ.+ ℤ.∣ m ∣ ℤ.* ℤ.+ ℤ.∣ ℤ.+ n ∣ ≡⟨ ℤ.pos-* ℤ.∣ m ∣ ℤ.∣ ℤ.+ n ∣ ⟨ ℤ.+ (ℤ.∣ m ∣ ℕ.* n) ≡⟨⟩ - ℤ.+ (ℤ.∣ m ∣ ℕ.* ℤ.∣ ℤ.+ n ∣) ≡˘⟨ cong ℤ.+_ (ℤ.∣i*j∣≡∣i∣*∣j∣ m (ℤ.+ n)) ⟩ + ℤ.+ (ℤ.∣ m ∣ ℕ.* ℤ.∣ ℤ.+ n ∣) ≡⟨ cong ℤ.+_ (ℤ.∣i*j∣≡∣i∣*∣j∣ m (ℤ.+ n)) ⟨ ℤ.+ (ℤ.∣ m ℤ.* ℤ.+ n ∣) ∎ ∣↥p∣↧q≡∣↥p↧q∣ : ∣↥p∣↧q ≡ ℤ.+ ℤ.∣ ↥p↧q ∣ ∣↥p∣↧q≡∣↥p↧q∣ = ∣m∣n≡∣mn∣ (↥ p) (↧ₙ q) diff --git a/src/Data/Tree/Binary/Zipper/Properties.agda b/src/Data/Tree/Binary/Zipper/Properties.agda index 107981bcbf..fa2f09c190 100644 --- a/src/Data/Tree/Binary/Zipper/Properties.agda +++ b/src/Data/Tree/Binary/Zipper/Properties.agda @@ -60,9 +60,9 @@ toTree-#nodes (mkZipper c v) = helper c v #ctx = sum (List.map (suc ∘ BT.#nodes ∘ getTree) ctx) #foc = BT.#nodes foc #l = BT.#nodes l in begin - #foc + (1 + (#l + #ctx)) ≡˘⟨ +-assoc #foc 1 (#l + #ctx) ⟩ + #foc + (1 + (#l + #ctx)) ≡⟨ +-assoc #foc 1 (#l + #ctx) ⟨ #foc + 1 + (#l + #ctx) ≡⟨ cong (_+ (#l + #ctx)) (+-comm #foc 1) ⟩ - 1 + #foc + (#l + #ctx) ≡˘⟨ +-assoc (1 + #foc) #l #ctx ⟩ + 1 + #foc + (#l + #ctx) ≡⟨ +-assoc (1 + #foc) #l #ctx ⟨ 1 + #foc + #l + #ctx ≡⟨ cong (_+ #ctx) (+-comm (1 + #foc) #l) ⟩ #nodes (mkZipper ctx (node l m foc)) ≡⟨ helper ctx (node l m foc) ⟩ BT.#nodes (toTree (mkZipper cs foc)) ∎ @@ -70,8 +70,8 @@ toTree-#nodes (mkZipper c v) = helper c v #ctx = sum (List.map (suc ∘ BT.#nodes ∘ getTree) ctx) #foc = BT.#nodes foc #r = BT.#nodes r in begin - #foc + (1 + (#r + #ctx)) ≡˘⟨ cong (#foc +_) (+-assoc 1 #r #ctx) ⟩ - #foc + (1 + #r + #ctx) ≡˘⟨ +-assoc #foc (suc #r) #ctx ⟩ + #foc + (1 + (#r + #ctx)) ≡⟨ cong (#foc +_) (+-assoc 1 #r #ctx) ⟨ + #foc + (1 + #r + #ctx) ≡⟨ +-assoc #foc (suc #r) #ctx ⟨ #nodes (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩ BT.#nodes (toTree (mkZipper cs foc)) ∎ @@ -86,7 +86,7 @@ toTree-#leaves (mkZipper c v) = helper c v #ctx = sum (List.map (BT.#leaves ∘ getTree) ctx) #foc = BT.#leaves foc #l = BT.#leaves l in begin - #foc + (#l + #ctx) ≡˘⟨ +-assoc #foc #l #ctx ⟩ + #foc + (#l + #ctx) ≡⟨ +-assoc #foc #l #ctx ⟨ #foc + #l + #ctx ≡⟨ cong (_+ #ctx) (+-comm #foc #l) ⟩ #leaves (mkZipper ctx (node l m foc)) ≡⟨ helper ctx (node l m foc) ⟩ BT.#leaves (toTree (mkZipper cs foc)) ∎ @@ -94,7 +94,7 @@ toTree-#leaves (mkZipper c v) = helper c v #ctx = sum (List.map (BT.#leaves ∘ getTree) ctx) #foc = BT.#leaves foc #r = BT.#leaves r in begin - #foc + (#r + #ctx) ≡˘⟨ +-assoc #foc #r #ctx ⟩ + #foc + (#r + #ctx) ≡⟨ +-assoc #foc #r #ctx ⟨ #leaves (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩ BT.#leaves (toTree (mkZipper cs foc)) ∎ diff --git a/src/Data/Tree/Rose/Properties.agda b/src/Data/Tree/Rose/Properties.agda index 749bdb5748..054103fdd1 100644 --- a/src/Data/Tree/Rose/Properties.agda +++ b/src/Data/Tree/Rose/Properties.agda @@ -39,7 +39,7 @@ map-∘ f g (node a ts) = cong (node (g (f a))) $ begin depth-map : (f : A → B) (t : Rose A i) → depth {i = i} (map {i = i} f t) ≡ depth {i = i} t depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin - List.map depth (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ + List.map depth (List.map (map f) ts) ≡⟨ Listₚ.map-∘ ts ⟨ List.map (depth ∘′ map f) ts ≡⟨ Listₚ.map-cong (depth-map f) ts ⟩ List.map depth ts ∎ @@ -49,7 +49,7 @@ depth-map f (node a ts) = cong (suc ∘′ max 0) $ begin foldr-map : (f : A → B) (n : B → List C → C) (ts : Rose A i) → foldr {i = i} n (map {i = i} f ts) ≡ foldr {i = i} (n ∘′ f) ts foldr-map f n (node a ts) = cong (n (f a)) $ begin - List.map (foldr n) (List.map (map f) ts) ≡˘⟨ Listₚ.map-∘ ts ⟩ + List.map (foldr n) (List.map (map f) ts) ≡⟨ Listₚ.map-∘ ts ⟨ List.map (foldr n ∘′ map f) ts ≡⟨ Listₚ.map-cong (foldr-map f n) ts ⟩ List.map (foldr (n ∘′ f)) ts ∎ diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda index 93f95b423b..d1d5f8c628 100644 --- a/src/Data/Vec/Functional/Properties.agda +++ b/src/Data/Vec/Functional/Properties.agda @@ -181,20 +181,20 @@ module _ {ys ys′ : Vector A m} where ... | yes i