Add proofs on truth value

Adds a handful of properties that prove the truth
value of a decidable:

- `Relation.Nullary.Decidable`:
  - `does-≡`: decidables over the same type have the same truth value
  - `does-⇔`: generalization of `does-≡` to mutually implied types

- `Relation.Unary.Properties`:
  - `≐?`: generalization of `Decidable.map` to predicates
    (if two predicates are equivalent, one is decidable if the other is)
  - `does-≡`: generalization of `does-≡` to predicates
  - `does-≐`: generalization of `does-⇔` to predicates

Author: mildsunrise

CHANGELOG.md

@@ -800,9 +800,11 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
-* Added new proof in `Relation.Nullary.Decidable`:
+* Added new proofs in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+  does-≡  : (a? b? : Dec A) → does a? ≡ does b?
   ```
 
 * Added new definitions and proofs in `Relation.Nullary.Decidable.Core`:
@@ -822,14 +824,21 @@ Additions to existing modules
   ```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`
+* Added new definitions in `Relation.Unary`:
   ```agda
   Stable          : Pred A ℓ → Set _
   WeaklyDecidable : Pred A ℓ → Set _
   ```
 
+* Added new proofs in `Relation.Nullary.Properties`:
+  ```agda
+  ≐?     : P ≐ Q → Decidable P → Decidable Q
+  does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
+  does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
+  ```
+
 * Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details.
   - Provide a marker function, `⌞_⌟`, for user-guided anti-unification.
   - Improved support for equalities between terms with instance arguments,

src/Relation/Nullary/Decidable.agda

@@ -10,9 +10,10 @@ module Relation.Nullary.Decidable where
 
 open import Level using (Level)
 open import Data.Bool.Base using (true; false)
-open import Data.Product.Base using (∃; _,_)
+open import Data.Product.Base using (∃; _×_; _,_)
+open import Function.Base using (id; _∘_)
 open import Function.Bundles using
-  (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
+  (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Irrelevant)
@@ -80,3 +81,10 @@ 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?))
+
+does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+does-⇔ A⇔B a? (yes b) = dec-true a? (Equivalence.from A⇔B b)
+does-⇔ A⇔B a? (no ¬b) = dec-false a? (¬b ∘ Equivalence.to A⇔B)
+
+does-≡ : (a? b? : Dec A) → does a? ≡ does b?
+does-≡ = does-⇔ (mk⇔ id id)

src/Relation/Unary/Properties.agda

@@ -8,17 +8,19 @@
 
 module Relation.Unary.Properties where
 
+open import Data.Bool.Base using (not)
 open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Level using (Level)
 open import Relation.Binary.Core as Binary
 open import Relation.Binary.Definitions
   hiding (Decidable; Universal; Irrelevant; Empty)
-open import Relation.Binary.PropositionalEquality.Core using (refl)
+open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does; does-⇔)
 open import Function.Base using (id; _$_; _∘_)
+open import Function.Bundles using (mk⇔)
 
 private
   variable
@@ -200,6 +202,10 @@ U-Universal = λ _ → _
 ------------------------------------------------------------------------
 -- Decidability properties
 
+≐? : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+     P ≐ Q → Decidable P → Decidable Q
+≐? (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
+
 ∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
 ∁? P? x = ¬? (P? x)
 
@@ -233,6 +239,15 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
 
+does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
+         (P? : Decidable P) → (Q? : Decidable Q) →
+         does ∘ P? ≗ does ∘ Q?
+does-≐ (P⊆Q , Q⊆P) P? Q? x = does-⇔ (mk⇔ P⊆Q Q⊆P) (P? x) (Q? x)
+
+does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
+         does ∘ P? ≗ does ∘ P?′
+does-≡ {P} P? P?′ = does-≐ ≐-refl P? P?′
+
 ------------------------------------------------------------------------
 -- Irrelevant properties