Move T? to Relation.Nullary.Decidable.Core (#2189)

* Move `T?` to `Relation.Nullary.Decidable.Core`

* Var name fix

* Some refactoring

* Fix failing tests and address remaining comments

* Fix style-guide

Author: MatthewDaggitt

CHANGELOG.md

@@ -838,6 +838,9 @@ Non-backwards compatible changes
 
   4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated
          and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`.
+		 
+  5. The proof `T?` has been moved from `Data.Bool.Properties` to `Relation.Nullary.Decidable.Core`
+	 (but is still re-exported by the former).
 
   as well as the following breaking changes:
 
@@ -3563,6 +3566,12 @@ Additions to existing modules
   poset          : Set a → Poset _ _ _
   ```
 
+* Added new proof in `Relation.Nullary.Reflects`:
+  ```agda
+  T-reflects : Reflects (T b) b
+  T-reflects-elim : Reflects (T a) b → b ≡ a
+  ```
+
 * Added new operations in `System.Exit`:
   ```
   isSuccess : ExitCode → Bool

README/Design/Hierarchies.agda

@@ -265,7 +265,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 --       IsA                     A
 --    /  ||   \               /  ||  \
 -- IsB   IsC   IsD          B    C    D
- 
+
 -- The procedure for re-exports in the bundles is as follows:
 
 -- 1. `open IsA isA public using (IsC, M)` where `M` is everything
@@ -280,7 +280,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
 
 -- 5. `open B b public using (O)` where `O` is everything exported
 --    by `B` but not exported by `IsA`.
- 
+
 -- 6. Construct `d : D` via the `isC` obtained in step 1.
 
 -- 7. `open D d public using (P)` where `P` is everything exported

notes/style-guide.md

@@ -402,7 +402,7 @@ word within a compound word is capitalized except for the first word.
 
 * Rational variables are named `p`, `q`, `r`, ... (default `p`)
 
-* All other variables tend to be named `x`, `y`, `z`.
+* All other variables should be named `x`, `y`, `z`.
 
 * Collections of elements are usually indicated by appending an `s`
   (e.g. if you are naming your variables `x` and `y` then lists

src/Data/Bool.agda

@@ -8,9 +8,6 @@
 
 module Data.Bool where
 
-open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 

src/Data/Bool/Base.agda

@@ -57,17 +57,19 @@ true  xor b = not b
 false xor b = b
 
 ------------------------------------------------------------------------
--- Other operations
-
-infix  0 if_then_else_
-
-if_then_else_ : Bool → A → A → A
-if true  then t else f = t
-if false then t else f = f
+-- Conversion to Set
 
 -- A function mapping true to an inhabited type and false to an empty
 -- type.
-
 T : Bool → Set
 T true  = ⊤
 T false = ⊥
+
+------------------------------------------------------------------------
+-- Other operations
+
+infix 0 if_then_else_
+
+if_then_else_ : Bool → A → A → A
+if true  then t else f = t
+if false then t else f = f

src/Data/Bool/Properties.agda

@@ -28,8 +28,7 @@ open import Relation.Binary.Definitions
   using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
-open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
+open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -726,15 +725,17 @@ xor-∧-commutativeRing = ⊕-∧-commutativeRing
   open XorRing _xor_ xor-is-ok
 
 ------------------------------------------------------------------------
--- Miscellaneous other properties
+-- Properties of if_then_else_
 
-⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
-⇔→≡ {true } {true }         hyp = refl
-⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl)
-⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl
-⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl
-⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl)
-⇔→≡ {false} {false}         hyp = refl
+if-float : ∀ (f : A → B) b {x y} →
+           f (if b then x else y) ≡ (if b then f x else f y)
+if-float _ true  = refl
+if-float _ false = refl
+
+------------------------------------------------------------------------
+-- Properties of T
+
+open Relation.Nullary.Decidable.Core public using (T?)
 
 T-≡ : ∀ {x} → T x ⇔ x ≡ true
 T-≡ {false} = mk⇔ (λ ())       (λ ())
@@ -757,18 +758,20 @@ T-∨ {false} {false} = mk⇔ inj₁ [ id , id ]
 T-irrelevant : U.Irrelevant T
 T-irrelevant {true}  _  _  = refl
 
-T? : U.Decidable T
-does  (T? b) = b
-proof (T? true ) = ofʸ _
-proof (T? false) = ofⁿ λ()
-
 T?-diag : ∀ b → T b → True (T? b)
-T?-diag true  _ = _
+T?-diag b = fromWitness
+
+------------------------------------------------------------------------
+-- Miscellaneous other properties
+
+⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
+⇔→≡ {true } {true }         hyp = refl
+⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl)
+⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl
+⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl
+⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl)
+⇔→≡ {false} {false}         hyp = refl
 
-if-float : ∀ (f : A → B) b {x y} →
-           f (if b then x else y) ≡ (if b then f x else f y)
-if-float _ true  = refl
-if-float _ false = refl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Data/List/Relation/Binary/BagAndSetEquality.agda

@@ -44,7 +44,7 @@ import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; _≗_; refl)
 open import Relation.Binary.Reasoning.Syntax
-open import Relation.Nullary
+open import Relation.Nullary.Negation using (¬_)
 open import Data.List.Membership.Propositional.Properties
 
 private

src/Effect/Applicative.agda

@@ -56,7 +56,7 @@ record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where
   -- Haskell-style alternative name for pure
   return : A → F A
   return = pure
-  
+
   -- backwards compatibility: unicode variants
   _⊛_ : F (A → B) → F A → F B
   _⊛_ = _<*>_

src/Function/Bundles.agda

@@ -380,7 +380,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
   -- For further background on (split) surjections, one may consult any
   -- general mathematical references which work without the principle
   -- of choice. For example:
-  -- 
+  --
   --   https://ncatlab.org/nlab/show/split+epimorphism.
   --
   -- The connection to set-theoretic notions with the same names is

src/Relation/Nullary.agda

@@ -15,20 +15,9 @@ open import Agda.Builtin.Equality
 ------------------------------------------------------------------------
 -- Re-exports
 
-open import Relation.Nullary.Negation.Core public using
-  ( ¬_; _¬-⊎_
-  ; contradiction; contradiction₂; contraposition
-  )
-
-open import Relation.Nullary.Reflects public using
-  ( Reflects; ofʸ; ofⁿ
-  ; _×-reflects_; _⊎-reflects_; _→-reflects_
-  )
-
-open import Relation.Nullary.Decidable.Core public using
-  ( Dec; does; proof; yes; no; _because_; recompute
-  ; ¬?; _×-dec_; _⊎-dec_; _→-dec_
-  )
+open import Relation.Nullary.Negation.Core public
+open import Relation.Nullary.Reflects public
+open import Relation.Nullary.Decidable.Core public
 
 ------------------------------------------------------------------------
 -- Irrelevant types