Add Recomputable types (#762)

Author: strake

CHANGELOG.md

@@ -496,21 +496,27 @@ Other minor additions
   <±-isStrictTotalOrder-≡      : IsStrictTotalOrder _≡_ _<_ → IsStrictTotalOrder _≡_ _<±_
   ```
 
-* Added new definition in `Relation.Binary.Core`:
+* Added new definitions in `Relation.Binary.Core`:
   ```agda
-  Universal _∼_ = ∀ x y → x ∼ y
+  Universal _∼_    = ∀ x y → x ∼ y
+  Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
   ```
 
-* The relation `_≅_` in `Relation.Binary.HeterogeneousEquality` has
-  been generalised so that the types of the two equal elements need not
-  be at the same universe level.
+* Added new proof to `Relation.Binary.Consequences`:
+  ```agda
+  dec⟶recomput : Decidable R → Recomputable R
+  ```
 
 * Added new proofs to `Relation.Nullary.Construct.Add.Point`:
   ```agda
   ≡-dec        : Decidable {A = A} _≡_ → Decidable {A = Pointed A} _≡_
   []-injective : [ x ] ≡ [ y ] → x ≡ y
   ```
 
+* The relation `_≅_` in `Relation.Binary.HeterogeneousEquality` has
+  been generalised so that the types of the two equal elements need not
+  be at the same universe level.
+
 * Added new proof to `Relation.Binary.PropositionalEquality.Core`:
   ```agda
   ≢-sym : Symmetric _≢_
@@ -520,3 +526,18 @@ Other minor additions
   ```agda
   syntax Satisfiable P = ∃⟨ P ⟩
   ```
+
+* Defined a notion of recomputability for unary and binary relations:
+  ```agda
+  Recomputable : Pred A ℓ → Set _
+  Recomputable P = ∀ {x} → .(P x) → P x
+
+  dec⟶recomputable : Decidable P → Recomputable P
+  ```
+
+  ```agda
+  Recomputable : REL A B ℓ → Set _
+  Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
+
+  dec⟶recomputable : Decidable R → Recomputable R
+  ```

src/Relation/Binary/Consequences.agda

@@ -11,11 +11,11 @@ module Relation.Binary.Consequences where
 open import Data.Maybe.Base using (just; nothing)
 open import Data.Sum as Sum using (inj₁; inj₂)
 open import Data.Product using (_,_)
-open import Data.Empty using (⊥-elim)
-open import Function using (_∘_; flip)
+open import Data.Empty.Irrelevant using (⊥-elim)
+open import Function using (_∘_; _$_; flip)
 open import Level using (Level)
 open import Relation.Binary.Core
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (yes; no; recompute)
 open import Relation.Unary using (∁)
 
 private
@@ -164,3 +164,8 @@ module _ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} where
 
   flip-Connex : Connex P Q → Connex Q P
   flip-Connex f x y = Sum.swap (f y x)
+
+module _ {r} {R : REL A B r} where
+
+     dec⟶recomputable : Decidable R → Recomputable R
+     dec⟶recomputable dec {a} {b} = recompute $ dec a b

src/Relation/Binary/Core.agda

@@ -217,6 +217,12 @@ WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)
 Irrelevant : REL A B ℓ → Set _
 Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b
 
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : REL A B ℓ → Set _
+Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
+
 -- Universal - all pairs of elements are related
 
 Universal : REL A B ℓ → Set _

src/Relation/Unary.agda

@@ -167,6 +167,12 @@ Decidable P = ∀ x → Dec (P x)
 Irrelevant : Pred A ℓ → Set _
 Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
 
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : Pred A ℓ → Set _
+Recomputable P = ∀ {x} → .(P x) → P x
+
 ------------------------------------------------------------------------
 -- Operations on sets
 

src/Relation/Unary/Consequences.agda

@@ -0,0 +1,15 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some properties imply others
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Unary.Consequences where
+
+open import Relation.Unary
+open import Relation.Nullary using (recompute)
+
+dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
+dec⟶recomputable P-dec = recompute (P-dec _)