[ add ] Relation.Nullary.Decidable.dec-yes-recompute (#2738)

* add: new lemma

* add: corollary

* add: sharper corollary; deprecate old version

* fix: knock-ons

* fix: clean-up

* refactor: remove `rewrite` steps

* fix: `CHANGELOG` note

* fix: broken qualified `import`

* fix: module paramater name

* fix: lemma names

* fix: lemma names

* refactor: lift basic definitions and properties out of `Recomputable` into `Core`

* refactor: propagate `import`s

* fix: lemma name

* refactor: remove deprecation; fix `CHANGELOG`

* refactor: remove coupling with `Data.Fin.Permutation`

Author: jamesmckinna

CHANGELOG.md

@@ -174,6 +174,8 @@ New modules
 
 * `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER
 
+* `Relation.Nullary.Recomputable.Core`
+
 Additions to existing modules
 -----------------------------
 
@@ -389,10 +391,17 @@ Additions to existing modules
   <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
   ```
 
+* In `Relation.Nullary.Decidable`:
+  ```agda
+  dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
+  recompute-irrelevant-id : (a? : Decidable A) → Irrelevant A →
+                            (a : A) → recompute a? a ≡ a
   ```
 
 * In `Relation.Unary`:
@@ -418,6 +427,7 @@ Additions to existing modules
   ```agda
   ⊤-reflects : Reflects (⊤ {a}) true
   ⊥-reflects : Reflects (⊥ {a}) false
+  ```
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
   ```agda

src/Relation/Nullary/Decidable.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; trans)
 
 private
@@ -77,15 +77,19 @@ dec-false : (a? : Dec A) → ¬ A → does a? ≡ false
 dec-false (false because  _ ) ¬a = refl
 dec-false (true  because [a]) ¬a = contradiction (invert [a]) ¬a
 
+dec-yes-recompute : (a? : Dec A) → .(a : A) → a? ≡ yes (recompute a? a)
+dec-yes-recompute a? a with yes _ ← a? | refl ← dec-true a? (recompute a? a) = refl
+
+dec-yes-irr : (a? : Dec A) → Irrelevant A → (a : A) → a? ≡ yes a
+dec-yes-irr a? irr a =
+  trans (dec-yes-recompute a? a) (≡.cong yes (recompute-irrelevant-id a? irr a))
+
 dec-yes : (a? : Dec A) → A → ∃ λ a → a? ≡ yes a
-dec-yes a? a with yes a′ ← a? | refl ← dec-true a? a = a′ , refl
+dec-yes a? a = _ , dec-yes-recompute a? a
 
 dec-no : (a? : Dec A) (¬a : ¬ A) → a? ≡ no ¬a
 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 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

@@ -22,8 +22,9 @@ open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
-open import Relation.Nullary.Recomputable as Recomputable
-  hiding (recompute-constant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+open import Relation.Nullary.Recomputable.Core as Recomputable
+  using (Recomputable)
 open import Relation.Nullary.Reflects as Reflects
   hiding (recompute; recompute-constant)
 open import Relation.Nullary.Negation.Core
@@ -84,6 +85,9 @@ recompute = Reflects.recompute ∘ proof
 recompute-constant : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
 recompute-constant = Recomputable.recompute-constant ∘ recompute
 
+recompute-irrelevant-id : (a? : Dec A) → Irrelevant A → (a : A) → recompute a? a ≡ a
+recompute-irrelevant-id = Recomputable.recompute-irrelevant-id ∘ recompute
+
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 

src/Relation/Nullary/Recomputable.agda

@@ -8,7 +8,6 @@
 
 module Relation.Nullary.Recomputable where
 
-open import Agda.Builtin.Equality using (_≡_; refl)
 open import Data.Empty using (⊥)
 open import Data.Irrelevant using (Irrelevant; irrelevant; [_])
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
@@ -22,22 +21,10 @@ private
     B : Set b
 
 ------------------------------------------------------------------------
--- Definition
---
--- The idea of being 'recomputable' is that, given an *irrelevant* proof
--- of a proposition `A` (signalled by being a value of type `.A`, all of
--- whose inhabitants are identified up to definitional equality, and hence
--- do *not* admit pattern-matching), one may 'promote' such a value to a
--- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
-
-Recomputable : (A : Set a) → Set a
-Recomputable A = .A → A
+-- Re-export
 
-------------------------------------------------------------------------
--- Fundamental property: 'promotion' is a constant function
+open import Relation.Nullary.Recomputable.Core public
 
-recompute-constant : (r : Recomputable A) (p q : A) → r p ≡ r q
-recompute-constant r p q = refl
 
 ------------------------------------------------------------------------
 -- Constructions

src/Relation/Nullary/Recomputable/Core.agda

@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Recomputable types and their algebra as Harrop formulas
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Recomputable.Core where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Level using (Level)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+
+------------------------------------------------------------------------
+-- Definition
+--
+-- The idea of being 'recomputable' is that, given an *irrelevant* proof
+-- of a proposition `A` (signalled by being a value of type `.A`, all of
+-- whose inhabitants are identified up to definitional equality, and hence
+-- do *not* admit pattern-matching), one may 'promote' such a value to a
+-- 'genuine' value of `A`, available for subsequent eg. pattern-matching.
+
+Recomputable : (A : Set a) → Set a
+Recomputable A = .A → A
+
+------------------------------------------------------------------------
+-- Fundamental properties:
+-- given `Recomputable A`, `recompute` is a constant function;
+-- moreover, the identity, if `A` is propositionally irrelevant.
+
+module _ (recompute : Recomputable A) where
+
+  recompute-constant : (p q : A) → recompute p ≡ recompute q
+  recompute-constant _ _ = refl
+
+  recompute-irrelevant-id : Irrelevant A → (a : A) → recompute a ≡ a
+  recompute-irrelevant-id irr a = irr (recompute a) a
+