diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..5f2a36a419 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,4 +1,4 @@ -Version 2.4-dev +Version 3.0-dev =============== The library has been tested using Agda 2.8.0. @@ -9,26 +9,16 @@ Highlights Bug-fixes --------- -* Fix a type error in `README.Data.Fin.Relation.Unary.Top` within the definition of `>-weakInduction`. - Non-backwards compatible changes -------------------------------- -Minor improvements ------------------- - -* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further - weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is - safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`. +* In `Relation.Nullary.Negation.Core`, all the various types of `contradiction` + have been weakened as far as possible to make their arguments definitionally + proof-irrelevant. As a consequence, there is no longer any need for the + separate v2.4 `contradiction-irr`. -* Refactored usages of `+-∸-assoc 1` to `∸-suc` in: - ```agda - README.Data.Fin.Relation.Unary.Top - Algebra.Properties.Semiring.Binomial - Data.Fin.Subset.Properties - Data.Nat.Binary.Subtraction - Data.Nat.Combinatorics - ``` +Other major improvements +------------------------ Deprecated modules ------------------ @@ -36,70 +26,8 @@ Deprecated modules Deprecated names ---------------- -* In `Algebra.Properties.CommutativeSemigroup`: - ```agda - interchange ↦ medial - ``` - New modules ----------- -* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below. - -* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition. - Additions to existing modules ----------------------------- - -* In `Algebra.Properties.RingWithoutOne`: - ```agda - [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y - ``` - -* In `Data.Fin.Permutation.Components`: - ```agda - transpose[i,i,j]≡j : (i j : Fin n) → transpose i i j ≡ j - transpose[i,j,j]≡i : (i j : Fin n) → transpose i j j ≡ i - transpose[i,j,i]≡j : (i j : Fin n) → transpose i j i ≡ j - transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k - ``` - -* In `Data.Fin.Properties`: - ```agda - ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq - ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j - ``` - -* In `Data.Nat.Properties`: - ```agda - ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n - ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m) - ``` - -* In `Data.Vec.Properties`: - ```agda - padRight-lookup : (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i - - padRight-map : (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) - - padRight-zipWith : (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) → - zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys) - - padRight-zipWith₁ : (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) → - zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡ - padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys)) - - padRight-take : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs - - padRight-drop : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a - - padRight-updateAt : (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) → - updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f) - ``` - -* In `Relation.Nullary.Negation.Core` - ```agda - ¬¬-η : A → ¬ ¬ A - ``` diff --git a/doc/style-guide.md b/doc/style-guide.md index 7da14eb7f5..36d70af28c 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -717,3 +717,9 @@ used successfully in PR systematic for `Nary` relations in PR [#811](https://github.com/agda/agda-stdlib/pull/811) +## Prefer use of `Relation.Nullary.Negation.Core.contradiction` + +Where possible use `contradiction` between two explicit arguments rather +than appealing to the lower-level `Data.Empty.⊥-elim`. This provides +clearer documentation for readers of the code, but also permits a wider +range of application, thanks to its arguments being made proof-irrelevant. diff --git a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda index 5ed32380de..fe099814be 100644 --- a/src/Algebra/Module/Morphism/ModuleHomomorphism.agda +++ b/src/Algebra/Module/Morphism/ModuleHomomorphism.agda @@ -51,7 +51,7 @@ x≈0⇒fx≈0 {x} x≈0 = begin⟨ B.≈ᴹ-setoid ⟩ B.0ᴹ ∎ fx≉0⇒x≉0 : ∀ {x} → f x B.≉ᴹ B.0ᴹ → x A.≉ᴹ A.0ᴹ -fx≉0⇒x≉0 = contraposition x≈0⇒fx≈0 +fx≉0⇒x≉0 x≈0 = contraposition x≈0⇒fx≈0 x≈0 -- Zero is a unique output of non-trivial (i.e. - ≉ `const 0`) linear map. x≉0⇒f[x]≉0 : ∀ {x} → NonTrivial x → x A.≉ᴹ A.0ᴹ → f x B.≉ᴹ B.0ᴹ diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index d7686b25ef..131b0a3263 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -16,10 +16,13 @@ module Algebra.Module.Properties.Semimodule (semimod : Semimodule semiring m ℓm) where +open import Relation.Nullary.Negation using (contraposition) + open CommutativeSemiring semiring open Semimodule semimod open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid -open import Relation.Nullary.Negation using (contraposition) + +------------------------------------------------------------------------ x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ x≈0⇒x*y≈0 {x} {y} x≈0 = begin @@ -34,7 +37,7 @@ y≈0⇒x*y≈0 {x} {y} y≈0 = begin 0ᴹ ∎ x*y≉0⇒x≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → x ≉ 0# -x*y≉0⇒x≉0 = contraposition x≈0⇒x*y≈0 +x*y≉0⇒x≉0 x≈0 = contraposition x≈0⇒x*y≈0 x≈0 x*y≉0⇒y≉0 : ∀ {x y} → x *ₗ y ≉ᴹ 0ᴹ → y ≉ᴹ 0ᴹ -x*y≉0⇒y≉0 = contraposition y≈0⇒x*y≈0 +x*y≉0⇒y≉0 y≈0 = contraposition y≈0⇒x*y≈0 y≈0 diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda index a80d689ec5..5c9e2c5227 100644 --- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda @@ -409,17 +409,17 @@ module Antisymmetry length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length zs ≤⟨ ℕ.n≤1+n (length zs) ⟩ length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + length ys₁ ∎) (ℕ.<-irrefl ≡.refl) antisym (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss) = contradiction (begin length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩ length ys₁ ≤⟨ length-mono-≤ ss ⟩ - length zs ∎) $ ℕ.<-irrefl ≡.refl + length zs ∎) (ℕ.<-irrefl ≡.refl) antisym (_∷_ {x} {xs} {y} {ys₁} r rs) (_∷ʳ_ {ys₂} {zs} z ss) = contradiction (begin length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩ length xs ≤⟨ length-mono-≤ rs ⟩ - length ys₁ ∎) $ ℕ.<-irrefl ≡.refl + length ys₁ ∎) (ℕ.<-irrefl ≡.refl) open Antisymmetry public diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda index 616247b696..fec3098491 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda @@ -49,11 +49,11 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) → ∀ {xs} → Unique S xs → Unique R (map f xs) - map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!) + map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (λ x≈y → contraposition inj x≈y) xs!) map⁻ : ∀ {f} → Congruent _≈₁_ _≈₂_ f → ∀ {xs} → Unique R (map f xs) → Unique S xs - map⁻ cong fxs! = AllPairs.map (contraposition cong) (AllPairs.map⁻ fxs!) + map⁻ cong fxs! = AllPairs.map (λ fx≉fy → contraposition cong fx≉fy) (AllPairs.map⁻ fxs!) ------------------------------------------------------------------------ -- ++ diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index c70cc5c3bc..d4399c11cb 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -22,7 +22,8 @@ open import Function.Base using (flip; _∘_; _∘′_) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Decidable as Dec using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) -open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂) +open import Relation.Nullary.Negation.Core + using (¬_; contradiction; contradiction′; contradiction₂) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core @@ -347,8 +348,9 @@ irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 ... | s