[ 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,71 +9,30 @@ 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`:
+* In `Relation.Nullary.Negation.Core`
   ```agda
-  ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
-  ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  ¬¬-η : 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,25 +16,28 @@ 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
+x≈0⇒x*y≈0 {x = x} {y = y} x≈0 = begin
   x  *ₗ y ≈⟨ *ₗ-congʳ x≈0 ⟩
   0# *ₗ y ≈⟨ *ₗ-zeroˡ y ⟩
   0ᴹ      ∎
 
 y≈0⇒x*y≈0 : ∀ {x y} → y ≈ᴹ 0ᴹ → x *ₗ y ≈ᴹ 0ᴹ
-y≈0⇒x*y≈0 {x} {y} y≈0 = begin
+y≈0⇒x*y≈0 {x = x} {y = y} y≈0 = begin
   x *ₗ y  ≈⟨ *ₗ-congˡ y≈0 ⟩
   x *ₗ 0ᴹ ≈⟨ *ₗ-zeroʳ x ⟩
   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/First/Properties.agda

@@ -18,7 +18,7 @@ import Data.Sum.Base as Sum
 open import Function.Base using (_∘′_; _∘_; id)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
 open import Relation.Nullary.Decidable.Core as Dec
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core using (¬¬-η; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
 
@@ -54,7 +54,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
-  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = contradiction qx (p⇒¬q px)
+  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = p⇒¬q px qx
   All⇒¬First p⇒¬q (_ ∷ pxs)  (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
 
   First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -97,7 +97,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where
 
   first? : Decidable P → Decidable (First P (∁ P))
   first? P? = Dec.fromSum
-            ∘ Sum.map₂ (All⇒¬First contradiction)
+            ∘ Sum.map₂ (All⇒¬First ¬¬-η)
             ∘ first (Dec.toSum ∘ P?)
 
   cofirst? : Decidable P → Decidable (First (∁ P) P)

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/Decidable/Core.agda

@@ -28,7 +28,7 @@ open import Relation.Nullary.Recomputable.Core as Recomputable
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
-  using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
+  using (¬_; ¬¬-η; Stable; negated-stable; contradiction; DoubleNegation)
 
 
 private
@@ -215,7 +215,7 @@ decidable-stable (true  because  [a]) ¬¬a = invert [a]
 decidable-stable (false because [¬a]) ¬¬a = contradiction (invert [¬a]) ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
-¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)
+¬-drop-Dec ¬¬a? = map′ negated-stable ¬¬-η (¬? ¬¬a?)
 
 -- A double-negation-translated variant of excluded middle (or: every
 -- nullary relation is decidable in the double-negation monad).

src/Relation/Nullary/Negation.agda

@@ -56,7 +56,7 @@ open import Relation.Nullary.Negation.Core public
 ¬¬-Monad : RawMonad {a} DoubleNegation
 ¬¬-Monad = mkRawMonad
   DoubleNegation
-  contradiction
+  ¬¬-η
   (λ x f → negated-stable (¬¬-map f x))
 
 ¬¬-push : DoubleNegation Π[ P ] → Π[ DoubleNegation ∘ P ]
@@ -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,38 +26,48 @@ 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.
 
 -- Double-negation
 DoubleNegation : Set a → Set a
 DoubleNegation A = ¬ ¬ A
 
+-- Eta law for double-negation
+
+¬¬-η : A → ¬ ¬ A
+¬¬-η a ¬a = ¬a a
+
 -- Stability under double-negation.
 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'
@@ -67,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