Move T? to Relation.Nullary.Decidable.Core (agda#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:
 
@@ -3574,6 +3577,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

src/Relation/Nullary/Decidable/Core.agda

@@ -12,7 +12,7 @@
 module Relation.Nullary.Decidable.Core where
 
 open import Level using (Level; Lift)
-open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
+open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
 open import Data.Empty using (⊥)
 open import Data.Empty.Irrelevant using (⊥-elim)
@@ -79,6 +79,9 @@ recompute (no ¬a) a = ⊥-elim (¬a a)
 infixr 1 _⊎-dec_
 infixr 2 _×-dec_ _→-dec_
 
+T? : ∀ x → Dec (T x)
+T? x = x because T-reflects x
+
 ¬? : Dec A → Dec (¬ A)
 does  (¬? a?) = not (does a?)
 proof (¬? a?) = ¬-reflects (proof a?)

src/Relation/Nullary/Reflects.agda

@@ -11,11 +11,12 @@ module Relation.Nullary.Reflects where
 open import Agda.Builtin.Equality
 
 open import Data.Bool.Base
+open import Data.Unit.Base using (⊤)
 open import Data.Empty
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Level using (Level)
-open import Function.Base using (_$_; _∘_; const)
+open import Function.Base using (_$_; _∘_; const; id)
 
 open import Relation.Nullary.Negation.Core
 
@@ -54,28 +55,31 @@ invert (ofⁿ ¬a) = ¬a
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 
+infixr 1 _⊎-reflects_
+infixr 2 _×-reflects_ _→-reflects_
+
+T-reflects : ∀ b → Reflects (T b) b
+T-reflects true  = of _
+T-reflects false = of id
+
 -- If we can decide A, then we can decide its negation.
 ¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
 ¬-reflects (ofʸ  a) = ofⁿ (_$ a)
 ¬-reflects (ofⁿ ¬a) = ofʸ ¬a
 
 -- If we can decide A and Q then we can decide their product
-infixr 2 _×-reflects_
 _×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A × B) (a ∧ b)
 ofʸ  a ×-reflects ofʸ  b = ofʸ (a , b)
 ofʸ  a ×-reflects ofⁿ ¬b = ofⁿ (¬b ∘ proj₂)
 ofⁿ ¬a ×-reflects _      = ofⁿ (¬a ∘ proj₁)
 
-
-infixr 1 _⊎-reflects_
 _⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                Reflects (A ⊎ B) (a ∨ b)
 ofʸ  a ⊎-reflects      _ = ofʸ (inj₁ a)
 ofⁿ ¬a ⊎-reflects ofʸ  b = ofʸ (inj₂ b)
 ofⁿ ¬a ⊎-reflects ofⁿ ¬b = ofⁿ (¬a ¬-⊎ ¬b)
 
-infixr 2 _→-reflects_
 _→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
                 Reflects (A → B) (not a ∨ b)
 ofʸ  a →-reflects ofʸ  b = ofʸ (const b)
@@ -95,3 +99,6 @@ det (ofʸ  a) (ofʸ  _) = refl
 det (ofʸ  a) (ofⁿ ¬a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofʸ  a) = contradiction a ¬a
 det (ofⁿ ¬a) (ofⁿ  _) = refl
+
+T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
+T-reflects-elim {a} r = det r (T-reflects a)