Adding ssreflect's `Reflects` idiom

[gallais]

Following Phil's question on the Agda ML, I realised we could maybe benefit
from having Reflects in the standard library:

data Reflects (P : Set) : Bool → Set where
  yes : (p : P)    → Reflects P true
  no  : (¬p : ¬ P) → Reflects P false

Sample properties:

map : ∀ {P Q} → (P → Q) → (Q → P) → ∀ {b} → Reflects P b → Reflects Q b
map p⇒q q⇒p (yes p) = yes (p⇒q p)
map p⇒q q⇒p (no ¬p) = no (λ q → ¬p (q⇒p q))

dec-Reflects : ∀ {b P} → Reflects P b → Dec P
dec-Reflects (yes p) = yes p
dec-Reflects (no ¬p) = no ¬p

Typical use-case:

_≤ᵇ_ : ℕ → ℕ → Bool
zero ≤ᵇ n = true
suc m ≤ᵇ zero = false
suc m ≤ᵇ suc n = m ≤ᵇ n

s≤s-inj : ∀ {m n} → suc m ≤ suc n → m ≤ n
s≤s-inj (s≤s p) = p

≤?⇔≤ᵇ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)
≤?⇔≤ᵇ zero    n       = yes z≤n
≤?⇔≤ᵇ (suc m) zero    = no (λ ())
≤?⇔≤ᵇ (suc m) (suc n) = map s≤s s≤s-inj (≤?⇔≤ᵇ m n)

[MatthewDaggitt]

Do we want to encourage further programming with Bool? I feel like we've been making progress against that programming style in the library recently.

In my opinion your use case isn't really a use case as _≤ᵇ_ should never be defined!

[gallais]

In this blog post @laMudri makes the case that it can sometimes be interesting
computationally to use the Bool-variant of a decidability proof.

In which case, being able to easily relate it to its proof-carrying counterpart
cannot hurt.

[MatthewDaggitt]

Fair enough! I've definitely feel less strongly about the point than I did last year. (As I remember I was in the middle of trying to prove properties about the horrendous boolean-based filter functions)

[laMudri]

What cases are there where stdlib's Dec is preferable to what I called EDec (Σ-2-large elim)? I didn't really put much thought into it other than that it works in my situation, and probably generally for equality tests on inductive types. Given pattern synonyms, the two should look pretty similar, too – though always using the patterns would remove the computational benefits.

pattern yes p = true , p
pattern no ¬p = false , ¬p

And what's the motivation for Reflects over EDec?

[laMudri]

Having talked with @gallais and tried it out a bit, I'm keen on definitions like these:

data Reflects (P : Set p) : Bool → Set p where
  true : (p : P) → Reflects P true
  false : (¬p : ¬ P) → Reflects P false

Dec : Set p → Set p
Dec P = ∃ (Reflects P)

pattern yes p = true , true p
pattern no ¬p = false , false ¬p

Reflects is useful to have. It is the graph of if b then P else ¬ P, so quite likely preferable to it. And having it separate from Dec lets us deal with the cases where we have an existing boolean-valued function and we're wanting to explain what it says (extrinsically).

On the other hand, intrinsic Dec programming is often quite nice, so it'd be good to have library support for it (to the extent we already have for the other definition of Dec). Here, for example, is the proof of decidable equality on ℕ:

_≟_ : (m n : ℕ) → Dec (m ≡ n)
zero ≟ zero = yes refl
zero ≟ suc n = no λ ()
suc m ≟ zero = no λ ()
suc m ≟ suc n = map′ (cong suc) suc-injective (m ≟ n)

Crucially, we have that proj₁ (map′ (b , r)) = b, letting the boolean portion compute just as a plain boolean function would.

[laMudri]

I did a quick test, and when I replace Dec by the definitions I gave above, index.agda checks nearly as-is. There is one weird case where using _$_ with the yes and no patterns causes some metavariables to not get solved. Replacing _$_ by _$′_ fixes these cases, listed below.

diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index d49f50a..89c9e1b 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -214,9 +214,9 @@ zero  ∣? zero                     = yes (0 ∣0)
 zero  ∣? suc n                    = no ((λ()) ∘′ 0∣⇒≡0)
 suc m ∣? n                        with n divMod suc m
 suc m ∣? .(q * suc m)             | result q zero    refl =
-  yes $ divides q refl
+  yes $′ divides q refl
 suc m ∣? .(1 + toℕ r + q * suc m) | result q (suc r) refl =
-  no $ nonZeroDivisor-lemma m q (suc r) (λ())
+  no $′ nonZeroDivisor-lemma m q (suc r) (λ())

There are also a couple of warnings, which would be fixed by deleting hiding (module Dec) in two places.

/home/ywb17173/repos/agda-stdlib-dev/src/Reflection.agda:24,30-49
The module Relation.Nullary doesn't export the following:
module Dec
when scope checking the declaration
  open import Relation.Nullary hiding (module Dec)

/home/ywb17173/repos/agda-stdlib-dev/src/Function/Related/TypeIsomorphisms.agda:31,30-49
The module Relation.Nullary doesn't export the following:
module Dec
when scope checking the declaration
  open import Relation.Nullary hiding (module Dec)

Now I'm wondering whether we really should replace Dec in the library.

---

The full diff from Relation.Nullary:

diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 8713416..39c660b 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -8,6 +8,8 @@
 
 module Relation.Nullary where
 
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Sigma
 open import Data.Empty hiding (⊥-elim)
 open import Data.Empty.Irrelevant
 open import Level
@@ -21,9 +23,25 @@ infix 3 ¬_
 
 -- Decidable relations.
 
-data Dec {p} (P : Set p) : Set p where
-  yes : ( p :   P) → Dec P
-  no  : (¬p : ¬ P) → Dec P
+-- data Dec {p} (P : Set p) : Set p where
+--   yes : ( p :   P) → Dec P
+--   no  : (¬p : ¬ P) → Dec P
+
+-- `Reflects` idiom: the truth value of P is reflected by a
+-- boolean value.
+
+data Reflects {p} (P : Set p) : Bool → Set p where
+  true  : ( p :   P) → Reflects P true
+  false : (¬p : ¬ P) → Reflects P false
+
+-- A version of `Dec` based on `Reflects`. Can compute
+-- conveniently when we only care about the boolean value.
+
+Dec : ∀ {p} → Set p → Set p
+Dec P = Σ Bool (Reflects P)
+
+pattern yes p = true , true p
+pattern no ¬p = false , false ¬p
 
 -- Given an irrelevant proof of a decidable type, a proof can
 -- be recomputed and subsequently used in relevant contexts.