Add proofs on truth value (#2418)

* 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

* fixup! use ⇔-id

* simplify

* fixup! use qualified import instead of renaming

* Update src/Relation/Unary/Properties.agda

Co-authored-by: jamesmckinna <[email protected]>

* Update src/Relation/Unary/Properties.agda

Co-authored-by: jamesmckinna <[email protected]>

* rename ≐? to map

---------

Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: MatthewDaggitt <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -71,3 +71,16 @@ Additions to existing modules
   ```agda
   _≡?_ : DecidableEquality (Vec A n)
   ```
+
+* In `Relation.Nullary.Decidable`:
+  ```agda
+  does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+  does-≡  : (a? b? : Dec A) → does a? ≡ does b?
+  ```
+
+* In `Relation.Nullary.Properties`:
+  ```agda
+  map    : 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?′
+  ```

src/Relation/Nullary/Decidable.agda

@@ -80,3 +80,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? : Dec A) → does a? ≡ does b?
+does-≡ a? (yes a) = dec-true a? a
+does-≡ a? (no ¬a) = dec-false a? ¬a
+
+does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+does-⇔ A⇔B a? = does-≡ (map A⇔B a?)

src/Relation/Unary/Properties.agda

@@ -15,9 +15,9 @@ 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 as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
 open import Function.Base using (id; _$_; _∘_)
 
 private
@@ -200,6 +200,10 @@ U-Universal = λ _ → _
 ------------------------------------------------------------------------
 -- Decidability properties
 
+map : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+      P ≐ Q → Decidable P → Decidable Q
+map (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 +237,15 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
 
+does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
+         does ∘ P? ≗ does ∘ P?′
+does-≡ P? P?′ x = Dec.does-≡ (P? x) (P?′ x)
+
+does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
+         (P? : Decidable P) → (Q? : Decidable Q) →
+         does ∘ P? ≗ does ∘ Q?
+does-≐ P≐Q P? = does-≡ (map P≐Q P?)
+
 ------------------------------------------------------------------------
 -- Irrelevant properties