Adds Relation.Nullary.Recomputable plus consequences

CHANGELOG.md

@@ -62,16 +62,6 @@ New modules
   Algebra.Module.Bundles.Raw
   ```
 
-* Prime factorisation of natural numbers.
-  ```
-  Data.Nat.Primality.Factorisation
-  ```
-
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
-  ```agda
-  Induction.InfiniteDescent
-  ```
-
 * The unique morphism from the initial, resp. terminal, algebra:
   ```agda
   Algebra.Morphism.Construct.Initial
@@ -83,11 +73,24 @@ New modules
   Algebra.Module.Construct.Idealization
   ```
 
+* Pointwise and equality relations over indexed containers:
+  ```agda
+  Data.Container.Indexed.Relation.Binary.Pointwise
+  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  ```
+
 * `Data.List.Relation.Binary.Sublist.Propositional.Slice`
   replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
   and adding new functions:
   - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
   - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
+  ```
+
+* Prime factorisation of natural numbers.
+  ```
+  Data.Nat.Primality.Factorisation
+  ```
 
 * `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
   ```agda
@@ -113,17 +116,22 @@ New modules
   _⇨_ = setoid
   ```
 
+* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+  ```agda
+  Induction.InfiniteDescent
+  ```
+
 * Symmetric interior of a binary relation
   ```
   Relation.Binary.Construct.Interior.Symmetric
   ```
 
-* Pointwise and equality relations over indexed containers:
+* Systematise the use of `Recomputable A = .A → A`:
   ```agda
-  Data.Container.Indexed.Relation.Binary.Pointwise
-  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
-  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  Relation.Nullary.Recomputable
   ```
+  with `Recomputable` exported publicly from `Relation.Nullary`.
+
 
 Additions to existing modules
 -----------------------------
@@ -233,6 +241,12 @@ Additions to existing modules
   Subtrees o c = (r : Response c) → X (next c r)
   ```
 
+* In `Data.Empty`:
+  ```agda
+  ⊥-recompute : Recomputable ⊥
+  ⊥-elim-irr  : .⊥ → Whatever
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n
@@ -394,6 +408,14 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new definitions in `Relation.Nullary.Negation.Core`:
+  ```agda
+  contradictionᵒ     : ¬ A → A → Whatever
+  weak-contradiction : .A → ¬ A → Whatever
+  irr-contradiction  : .A → .(¬ A) → Whatever
+  ¬-recompute        : Recomputable (¬ A)
+  ```
+
 * Added new proof in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
@@ -405,5 +427,11 @@ Additions to existing modules
   WeaklyDecidable : Pred A ℓ → Set _
   ```
 
+* Added new definitions in `Relation.Unary`
+  ```
+  Stable          : Pred A ℓ → Set _
+  WeaklyDecidable : Pred A ℓ → Set _
+  ```
+
 * `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
   anti-unification. See README.Tactic.Cong for details.

src/Data/Empty.agda

@@ -9,6 +9,7 @@
 module Data.Empty where
 
 open import Data.Irrelevant using (Irrelevant)
+open import Relation.Nullary.Recomputable using (Recomputable)
 
 ------------------------------------------------------------------------
 -- Definition
@@ -30,8 +31,17 @@ private
 
 {-# DISPLAY Irrelevant Empty = ⊥ #-}
 
+------------------------------------------------------------------------
+-- ⊥ is Recomputable
+
+⊥-recompute : Recomputable ⊥
+⊥-recompute ()
+
 ------------------------------------------------------------------------
 -- Functions
 
 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
 ⊥-elim ()
+
+⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+⊥-elim-irr ()

src/Relation/Nullary.agda

@@ -23,8 +23,9 @@ private
 ------------------------------------------------------------------------
 -- Re-exports
 
+open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
-open import Relation.Nullary.Reflects public
+open import Relation.Nullary.Reflects public hiding (recompute)
 open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
@@ -33,13 +34,6 @@ open import Relation.Nullary.Decidable.Core public
 Irrelevant : Set p → Set p
 Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
 
-------------------------------------------------------------------------
--- Recomputability - we can rebuild a relevant proof given an
--- irrelevant one.
-
-Recomputable : Set p → Set p
-Recomputable P = .P → P
-
 ------------------------------------------------------------------------
 -- Weak decidability
 -- `nothing` is 'don't know'/'give up'; `just` is `yes`/`definitely`

src/Relation/Nullary/Decidable.agda

@@ -10,7 +10,6 @@ module Relation.Nullary.Decidable where
 
 open import Level using (Level)
 open import Data.Bool.Base using (true; false; if_then_else_)
-open import Data.Empty using (⊥-elim)
 open import Data.Product.Base using (∃; _,_)
 open import Function.Base
 open import Function.Bundles using
@@ -52,8 +51,8 @@ via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
 -- A lemma relating True and Dec
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
-True-↔ (true  because [a]) irr = mk↔ₛ′ (λ _ → invert [a]) _ (irr (invert [a])) cong′
-True-↔ (false because ofⁿ ¬a) _ = mk↔ₛ′ (λ ()) (invert (ofⁿ ¬a)) (⊥-elim ∘ ¬a) λ ()
+True-↔ (true  because [a]) irr = let a = invert [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
+True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
 
 ------------------------------------------------------------------------
 -- Result of decidability
@@ -64,11 +63,11 @@ isYes≗does (false because _) = refl
 
 dec-true : (a? : Dec A) → A → does a? ≡ true
 dec-true (true  because   _ ) a = refl
-dec-true (false because [¬a]) a = ⊥-elim (invert [¬a] a)
+dec-true (false because [¬a]) a = contradiction a (invert [¬a])
 
 dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
 dec-false (false because  _ ) ¬a = refl
-dec-false (true  because [a]) ¬a = ⊥-elim (¬a (invert [a]))
+dec-false (true  because [a]) ¬a = contradiction (invert [a]) ¬a
 
 dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
 dec-yes a? a with dec-true a? a

src/Relation/Nullary/Decidable/Core.agda

@@ -14,12 +14,11 @@ module Relation.Nullary.Decidable.Core where
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
-open import Data.Empty using (⊥)
-open import Data.Empty.Irrelevant using (⊥-elim)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Reflects
+open import Relation.Nullary.Recomputable
+open import Relation.Nullary.Reflects as Reflects hiding (recompute)
 open import Relation.Nullary.Negation.Core
 
 private
@@ -69,9 +68,8 @@ module _ {A : Set a} where
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.
-recompute : Dec A → .A → A
-recompute (yes a) _ = a
-recompute (no ¬a) a = ⊥-elim (¬a a)
+recompute : Dec A → Recomputable A
+recompute = Reflects.recompute ∘ proof
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -171,7 +169,7 @@ proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A
 
 decidable-stable : Dec A → Stable A
 decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = ⊥-elim (¬¬a ¬a)
+decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a
 
 ¬-drop-Dec : Dec (¬ ¬ A) → Dec (¬ A)
 ¬-drop-Dec ¬¬a? = map′ negated-stable contradiction (¬? ¬¬a?)

src/Relation/Nullary/Negation.agda

@@ -10,7 +10,6 @@ module Relation.Nullary.Negation where
 
 open import Effect.Monad using (RawMonad; mkRawMonad)
 open import Data.Bool.Base using (Bool; false; true; if_then_else_; not)
-open import Data.Empty using (⊥-elim)
 open import Data.Product.Base as Product using (_,_; Σ; Σ-syntax; ∃; curry; uncurry)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (flip; _∘_; const; _∘′_)
@@ -73,7 +72,7 @@ open import Relation.Nullary.Negation.Core public
 -- ⊥).
 
 call/cc : ((A → Whatever) → DoubleNegation A) → DoubleNegation A
-call/cc hyp ¬a = hyp (λ a → ⊥-elim (¬a a)) ¬a
+call/cc hyp ¬a = hyp (contradictionᵒ ¬a) ¬a
 
 -- The "independence of premise" rule, in the double-negation monad.
 -- It is assumed that the index set (A) is inhabited.
@@ -83,7 +82,7 @@ independence-of-premise {A = A} {B = B} {P = P} q f = ¬¬-map helper ¬¬-exclu
   where
   helper : Dec B → Σ[ x ∈ A ] (B → P x)
   helper (yes p) = Product.map₂ const (f p)
-  helper (no ¬p) = (q , ⊥-elim ∘′ ¬p)
+  helper (no ¬p) = (q , contradictionᵒ ¬p)
 
 -- The independence of premise rule for binary sums.
 
@@ -92,7 +91,7 @@ independence-of-premise-⊎ {A = A} {B = B} {C = C} f = ¬¬-map helper ¬¬-exc
   where
   helper : Dec A → (A → B) ⊎ (A → C)
   helper (yes p) = Sum.map const const (f p)
-  helper (no ¬p) = inj₁ (⊥-elim ∘′ ¬p)
+  helper (no ¬p) = inj₁ (contradictionᵒ ¬p)
 
 private
 

src/Relation/Nullary/Negation/Core.agda

@@ -9,10 +9,11 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Empty using (⊥; ⊥-elim; ⊥-recompute; ⊥-elim-irr)
 open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
+open import Relation.Nullary.Recomputable
 
 private
   variable
@@ -51,13 +52,22 @@ _¬-⊎_ = [_,_]
 contradiction : A → ¬ A → Whatever
 contradiction a ¬a = ⊥-elim (¬a a)
 
+contradictionᵒ : ¬ A → A → Whatever
+contradictionᵒ = flip contradiction
+
 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 f ¬b a = contradiction (f a) ¬b
 
+weak-contradiction : .A → ¬ A → Whatever
+weak-contradiction a ¬a = ⊥-elim-irr (¬a a)
+
+irr-contradiction : .A → .(¬ A) → Whatever
+irr-contradiction a ¬a = ⊥-elim-irr (¬a a)
+
 -- Everything is stable in the double-negation monad.
 stable : ¬ ¬ Stable A
 stable ¬[¬¬a→a] = ¬[¬¬a→a] (λ ¬¬a → ⊥-elim (¬¬a (¬[¬¬a→a] ∘ const)))
@@ -73,3 +83,10 @@ negated-stable ¬¬¬a a = ¬¬¬a (_$ a)
 private
   note : (A → ¬ B) → B → ¬ A
   note = flip
+
+------------------------------------------------------------------------
+-- recompute: negated propositions are Recomputable
+
+¬-recompute : Recomputable (¬ A)
+¬-recompute {A = A} = A →-recompute ⊥-recompute
+

src/Relation/Nullary/Recomputable.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Recomputable where
+
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+-- Definition
+
+Recomputable : (A : Set a) → Set a
+Recomputable A = .A → A
+
+------------------------------------------------------------------------
+-- Constructions
+
+_×-recompute_ : Recomputable A → Recomputable B → Recomputable (A × B)
+(rA ×-recompute rB) p = rA (p .proj₁) , rB (p .proj₂)
+
+_→-recompute_ : (A : Set a) → Recomputable B → Recomputable (A → B)
+(A →-recompute rB) f a = rB (f a)
+
+Π-recompute : (B : A → Set b) → (∀ x → Recomputable (B x)) → Recomputable (∀ x → B x)
+Π-recompute B rB f a = rB a (f a)
+
+∀-recompute : (B : A → Set b) → (∀ {x} → Recomputable (B x)) → Recomputable (∀ {x} → B x)
+∀-recompute B rB f = rB f