[ refactor ] make contradiction and friends entirely definitionally proof-irrelevant

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,97 +9,25 @@ 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
 ------------------
 
 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
-  ```

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.

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ᴹ

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

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
 

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!)
 
 ------------------------------------------------------------------------
 -- ++

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<s z<s = inj₂ refl
 
 irreducible⇒nonZero : Irreducible n → NonZero n
-irreducible⇒nonZero {zero}    = flip contradiction ¬irreducible[0]
-irreducible⇒nonZero {suc _} _ = _
+irreducible⇒nonZero {zero}  irreducible[0] =
+  contradiction′ ¬irreducible[0] irreducible[0]
+irreducible⇒nonZero {suc _} _      = _
 
 irreducible? : Decidable Irreducible
 irreducible? zero      = no ¬irreducible[0]

src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda

@@ -39,7 +39,7 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
 
   map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
          ∀ {n xs} → Unique S {n} xs → Unique R {n} (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!)
 
 ------------------------------------------------------------------------
 -- take & drop

src/Relation/Nullary/Negation.agda

@@ -72,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (flip contradiction ¬a) ¬a
+call/cc hyp ¬a = hyp (λ a → contradiction a ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -81,17 +81,17 @@ independence-of-premise : A → (B → Σ A P) → DoubleNegation (Σ[ x ∈ A ]
 independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
-  helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , flip contradiction ¬p)
+  helper (yes b) = Product.map₂ const (f b)
+  helper (no ¬b) = (q , λ b → contradiction b ¬b)
 
 -- The independence of premise rule for binary sums.
 
 independence-of-premise-⊎ : (A → B ⊎ C) → DoubleNegation ((A → B) ⊎ (A → C))
 independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-excluded-middle
   where
   helper : Dec A → (A → B) ⊎ (A → C)
-  helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (flip contradiction ¬p)
+  helper (yes a) = Sum.map const const (f a)
+  helper (no ¬a) = inj₁ λ a → contradiction a ¬a
 
 private
 

src/Relation/Nullary/Negation/Core.agda

@@ -26,6 +26,18 @@ infix 3 ¬_
 ¬_ : Set a → Set a
 ¬ A = A → ⊥
 
+-- Note the following use of flip:
+private
+  note : (A → ¬ B) → B → ¬ A
+  note = flip
+
+------------------------------------------------------------------------
+-- Relationship to sum
+
+infixr 1 _¬-⊎_
+_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
+_¬-⊎_ = [_,_]
+
 ------------------------------------------------------------------------
 -- Stability.
 
@@ -42,27 +54,20 @@ DoubleNegation A = ¬ ¬ A
 Stable : Set a → Set a
 Stable A = ¬ ¬ A → A
 
-------------------------------------------------------------------------
--- Relationship to sum
-
-infixr 1 _¬-⊎_
-_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
-_¬-⊎_ = [_,_]
-
 ------------------------------------------------------------------------
 -- Uses of negation
 
-contradiction-irr : .A → .(¬ A) → Whatever
-contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
+contradiction : .A → .(¬ A) → Whatever
+contradiction a ¬a = ⊥-elim-irr (¬a a)
 
-contradiction : A → ¬ A → Whatever
-contradiction a ¬a = contradiction-irr a ¬a
+contradiction′ : .(¬ A) → .A → Whatever
+contradiction′ ¬a a = ⊥-elim-irr (¬a a)
 
-contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
+contradiction₂ : A ⊎ B → .(¬ A) → .(¬ B) → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
 contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b
 
-contraposition : (A → B) → ¬ B → ¬ A
+contraposition : (A → B) → .(¬ B) → ¬ A
 contraposition f ¬b a = contradiction (f a) ¬b
 
 -- Self-contradictory propositions are false by 'diagonalisation'
@@ -72,17 +77,11 @@ contra-diagonal self a = self a a
 
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
-stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
+stable ¬[¬¬a→a] = ¬[¬¬a→a] λ ¬¬a → contradiction (¬[¬¬a→a] ∘ const) ¬¬a
 
 -- Negated predicates are stable.
 negated-stable : Stable (¬ A)
-negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
+negated-stable ¬¬¬a a = ¬¬¬a λ ¬a → contradiction a ¬a
 
 ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
-¬¬-map f = contraposition (contraposition f)
-
--- Note also the following use of flip:
-private
-  note : (A → ¬ B) → B → ¬ A
-  note = flip
-
+¬¬-map f ¬¬a = contraposition (λ ¬b → contraposition f ¬b) ¬¬a

src/Relation/Nullary/Reflects.agda

@@ -18,7 +18,7 @@ open import Data.Empty.Polymorphic using (⊥)
 open import Level using (Level)
 open import Function.Base using (_$_; _∘_; const; id)
 open import Relation.Nullary.Negation.Core
-  using (¬_; contradiction-irr; contradiction; _¬-⊎_)
+  using (¬_; contradiction; _¬-⊎_)
 open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
 
 private
@@ -61,7 +61,7 @@ invert (ofⁿ ¬a) = ¬a
 
 recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
-recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
+recompute (ofⁿ ¬a) a = contradiction a ¬a
 
 recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) →
                      recompute r p ≡ recompute r q