Adds Relation.Nullary.Recomputable plus consequences (#2243)

* prototype for fixing #2199

* delegate to `Relation.Nullary.Negation.Core.weak-contradiction`

* refactoring: lift out `Recomputable` in its own right

* forgot to add this module

* refactoring: tweak

* tidying up; added `CHANGELOG`

* more tidying up

* streamlined `import`s

* removed `Recomputable` from `Relation.Nullary`

* fixed multiple definitions in `Relation.Unary`

* reorder `CHANGELOG` entries after merge

* `contradiciton` via `weak-contradiction`

* irrefutable `with`

* use `of`

* only use *irrelevant* `⊥-elim-irr`

* tightened `import`s

* removed `irr-contradiction`

* inspired by #2329

* conjecture: all uses of `contradiction` can be made weak

* second thoughts: reverted last round of chnages

* lazier pattern analysis cf. #2055

* dependencies: uncoupled from `Recomputable`

* moved `⊥` and `¬ A` properties to this one place

* removed `contradictionᵒ` and rephrased everything in terms of `weak-contradiction`

* knock-on consequences; simplified `import`s

* narrow `import`s

* narrow `import`s; irrefutable `with`

* narrow `import`s; `CHANGELOG`

* narrow `import`s

* response to review comments

* irrelevance of `recompute`

* knock-on, plus proof of `UIP` from #2149

* knock-ons from renaming

* knock-on from renaming

* pushed proof `recompute-constant` to `Recomputable`

CHANGELOG.md

@@ -118,25 +118,9 @@ New modules
  Algebra.Module.Bundles.Raw
  ```
 
-* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
- ```
- Data.List.Relation.Binary.Equality.Setoid.Properties
- ```
-
-* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
- ```
- Data.List.Scans.Base
- Data.List.Scans.Properties
- ```
-
-* Prime factorisation of natural numbers.
- ```
- Data.Nat.Primality.Factorisation
- ```
-
-* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+* Nagata's construction of the "idealization of a module":
  ```agda
- Induction.InfiniteDescent
+ Algebra.Module.Construct.Idealization
  ```
 
 * The unique morphism from the initial, resp. terminal, algebra:
@@ -145,16 +129,35 @@ New modules
  Algebra.Morphism.Construct.Terminal
  ```
 
-* Nagata's construction of the "idealization of a module":
+* Pointwise and equality relations over indexed containers:
  ```agda
- Algebra.Module.Construct.Idealization
+ Data.Container.Indexed.Relation.Binary.Pointwise
+ Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+ Data.Container.Indexed.Relation.Binary.Equality.Setoid
+ ```
+
+* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties:
+ ```
+ Data.List.Scans.Base
+ Data.List.Scans.Properties
+ ```
+
+* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid):
+ ```
+ Data.List.Relation.Binary.Equality.Setoid.Properties
  ```
 
 * `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
@@ -180,6 +183,11 @@ 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
@@ -190,12 +198,11 @@ New modules
  Relation.Binary.Properties.DecSetoid
  ```
 
-* 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`.
 
 * New IO primitives to handle buffering
  ```agda
@@ -372,6 +379,11 @@ Additions to existing modules
  Subtrees o c = (r : Response c) → X (next c r)
  ```
 
+* In `Data.Empty`:
+ ```agda
+ ⊥-elim-irr : .⊥ → Whatever
+ ```
+
 * In `Data.Fin.Properties`:
  ```agda
  nonZeroIndex : Fin n → ℕ.NonZero n
@@ -674,7 +686,7 @@ Additions to existing modules
 * Added new definitions in `Relation.Binary.Definitions`
  ```
  Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
- Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+ Empty _∼_ = ∀ {x y} → ¬ (x ∼ y)
  ```
 
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
@@ -690,11 +702,27 @@ Additions to existing modules
  WeaklyDecidable : Set _
  ```
 
+* Added new proof in `Relation.Nullary.Decidable.Core`:
+ ```agda
+ recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+ ```
+
 * Added new proof in `Relation.Nullary.Decidable`:
  ```agda
  ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
  ```
 
+* Added new definitions in `Relation.Nullary.Negation.Core`:
+ ```agda
+ contradiction-irr : .A → ¬ A → Whatever
+ ```
+
+* Added new definitions in `Relation.Nullary.Reflects`:
+ ```agda
+ recompute : Reflects A b → Recomputable A
+ recompute-constant : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+ ```
+
 * Added new definitions in `Relation.Unary`
  ```
  Stable : Pred A ℓ → Set _

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -8,23 +8,27 @@
 
 module Axiom.UniquenessOfIdentityProofs where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Empty
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary hiding (Irrelevant)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core using (recompute; recompute-constant)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 
+private
+ variable
+ a : Level
+ A : Set a
+ x y : A
+
 ------------------------------------------------------------------------
 -- Definition
 --
 -- Uniqueness of Identity Proofs (UIP) states that all proofs of
 -- equality are themselves equal. In other words, the equality relation
 -- is irrelevant. Here we define UIP relative to a given type.
 
-UIP : ∀ {a} (A : Set a) → Set a
+UIP : (A : Set a) → Set a
 UIP A = Irrelevant {A = A} _≡_
 
 ------------------------------------------------------------------------
@@ -39,11 +43,11 @@ UIP A = Irrelevant {A = A} _≡_
 -- the image of any other proof.
 
 module Constant⇒UIP
- {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_)
- (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q)
+ (f : _≡_ {A = A} ⇒ _≡_)
+ (f-constant : ∀ {x y} (p q : x ≡ y) → f p ≡ f q)
  where
 
- ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p
+ ≡-canonical : (p : x ≡ y) → trans (sym (f refl)) (f p) ≡ p
  ≡-canonical refl = trans-symˡ (f refl)
 
  ≡-irrelevant : UIP A
@@ -59,19 +63,14 @@ module Constant⇒UIP
 -- function over proofs of equality which is constant: it returns the
 -- proof produced by the decision procedure.
 
-module Decidable⇒UIP
- {a} {A : Set a} (_≟_ : DecidableEquality A)
+module Decidable⇒UIP (_≟_ : DecidableEquality A)
  where
 
  ≡-normalise : _≡_ {A = A} ⇒ _≡_
- ≡-normalise {a} {b} a≡b with a ≟ b
- ... | true because [p] = invert [p]
- ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b)
-
- ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
- ≡-normalise-constant {a} {b} p q with a ≟ b
- ... | true because _ = refl
- ... | false because [¬p] = ⊥-elim (invert [¬p] p)
+ ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y
+
+ ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
+ ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≟ y)
 
  ≡-irrelevant : UIP A
  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

src/Data/Empty.agda

@@ -35,3 +35,6 @@ private
 
 ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
 ⊥-elim ()
+
+⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+⊥-elim-irr ()

src/Relation/Binary/Definitions.agda

@@ -12,8 +12,6 @@ module Relation.Binary.Definitions where
 
 open import Agda.Builtin.Equality using (_≡_)
 
-open import Data.Empty using (⊥)
-open import Data.Maybe.Base using (Maybe)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
@@ -248,7 +246,7 @@ Universal _∼_ = ∀ x y → x ∼ y
 -- Empty - no elements are related
 
 Empty : REL A B ℓ → Set _
-Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+Empty _∼_ = ∀ {x y} → ¬ (x ∼ y)
 
 -- Non-emptiness - at least one pair of elements are related.
 

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; recompute-constant)
 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

@@ -9,15 +9,14 @@
 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.Bool.Base using (true; false)
 open import Data.Product.Base using (∃; _,_)
-open import Function.Base
 open import Function.Bundles using
  (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary
+open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym; trans; cong′)
@@ -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,23 +63,20 @@ 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
-dec-yes (yes a′) a | refl = a′ , refl
+dec-yes a? a with yes a′ ← a? | refl ← dec-true a? a = a′ , refl
 
 dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
-dec-no a? ¬a with dec-false a? ¬a
-dec-no (no _) _ | refl = refl
+dec-no a? ¬a with no _ ← a? | refl ← dec-false a? ¬a = refl
 
 dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
-dec-yes-irr a? irr a with dec-yes a? a
-... | a′ , eq rewrite irr a a′ = eq
+dec-yes-irr a? irr a with a′ , eq ← dec-yes a? a rewrite irr a a′ = eq
 
 ⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
 ⌊⌋-map′ t f a? = trans (isYes≗does (map′ t f a?)) (sym (isYes≗does a?))

src/Relation/Nullary/Decidable/Core.agda

@@ -11,17 +11,19 @@
 
 module Relation.Nullary.Decidable.Core where
 
+open import Agda.Builtin.Equality using (_≡_)
 open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base 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 as Recomputable hiding (recompute-constant)
+open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
  using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
 
+
 private
  variable
  a b : Level
@@ -69,9 +71,12 @@ 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
+
+recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+recompute-constant = Recomputable.recompute-constant ∘ recompute
 
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
@@ -161,17 +166,17 @@ from-no (true because _ ) = _
 
 map′ : (A → B) → (B → A) → Dec A → Dec B
 does (map′ A→B B→A a?) = does a?
-proof (map′ A→B B→A (true because [a])) = ofʸ (A→B (invert [a]))
-proof (map′ A→B B→A (false because [¬a])) = ofⁿ (invert [¬a] ∘ B→A)
+proof (map′ A→B B→A (true because [a])) = of (A→B (invert [a]))
+proof (map′ A→B B→A (false because [¬a])) = of (invert [¬a] ∘ B→A)
 
 ------------------------------------------------------------------------
 -- Relationship with double-negation
 
 -- Decidable predicates are stable.
 
 decidable-stable : Dec A → Stable A
-decidable-stable (yes a) ¬¬a = a
-decidable-stable (no ¬a) ¬¬a = contradiction ¬a ¬¬a
+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?)