Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jamesmckinna merged 5 commits into from
Nov 1, 2023
Merged

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

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e3a3ad0
Move `T?` to `Relation.Nullary.Decidable.Core`
MatthewDaggitt Oct 31, 2023
ea53921
Var name fix
MatthewDaggitt Oct 31, 2023
bfb7959
Some refactoring
MatthewDaggitt Nov 1, 2023
e42161a
Fix failing tests and address remaining comments
MatthewDaggitt Nov 1, 2023
a173664
Fix style-guide
MatthewDaggitt Nov 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down Expand Up @@ -3563,6 +3566,11 @@ Additions to existing modules
poset : Set a → Poset _ _ _
```

* Added new proof in `Relation.Nullary.Reflects`:
```agda
T-reflects : Reflects (T b) b
```
Copy link
Collaborator

@jamesmckinna jamesmckinna Oct 31, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, I chose the name T⁺ in #2055 on the model of the style-guide for "pre- and post-conditions". I don't disagree with the new name per se, but then what would you call T⁻ defined below? In any case, I don't think these names should ever be exported outside Relation.Nullary.Decidable.Core...?

Copy link
Collaborator Author

@MatthewDaggitt MatthewDaggitt Nov 1, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I chose this name because it was consistent with the other properties immediately below. I don't think this falls into pre- and post- conditions convention in the style guide.:

When defining a new relation P over a datatype X in a Data.X.Relation module, it is often common to define how to introduce and eliminate that relation with respect to various functions.

Firstly, we're not in a Data.X.Relation module. Secondly, I guess you could argue that P is Reflects but then what is the datatype X and what is the function that eliminates or introduces it?

I'll have a think about a suitable name.

Copy link
Collaborator

@jamesmckinna jamesmckinna Nov 1, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that's a fair response (modulo my regarding Reflects as the datatype, or else as a Set-valued view of Bool, but in any case, as an inductive family; and then the 'function' is... T itself; but I admit those are the possibly-unconventional spectacles through which I look at the world), and given the rest of Reflects, the choice of name here seems fine... up to what its dual/inverse should be called. But I do think the principle that, just as with introduction/elimination, these things 'come in pairs', should be adhered to wherever possible. The T⁺/T⁻ scheme is then a convenient, and minimum-ink, reification of that principle. But this probably belongs in a separate style-guide collection of issues... ;-)


* Added new operations in `System.Exit`:
```
isSuccess : ExitCode → Bool
Expand Down
2 changes: 1 addition & 1 deletion notes/style-guide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, including `Bool`, 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
Expand Down
3 changes: 0 additions & 3 deletions src/Data/Bool.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
18 changes: 10 additions & 8 deletions src/Data/Bool/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
43 changes: 23 additions & 20 deletions src/Data/Bool/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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} _≡_
Expand Down Expand Up @@ -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⇔ (λ ()) (λ ())
Expand All @@ -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
Expand Down
17 changes: 3 additions & 14 deletions src/Relation/Nullary.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 4 additions & 1 deletion src/Relation/Nullary/Decidable/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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?)
Expand Down
42 changes: 22 additions & 20 deletions src/Relation/Nullary/Reflects.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,18 +11,20 @@ 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

private
variable
a : Level
A B : Set a
x y : Bool

------------------------------------------------------------------------
-- `Reflects` idiom.
Expand All @@ -43,54 +45,54 @@ data Reflects (A : Set a) : Bool → Set a where
-- `ofʸ`), and `invert` strips off the constructor to just give either
-- the proof of `A` or the proof of `¬ A`.

of : ∀ {b} → if b then A else ¬ A → Reflects A b
of {b = false} ¬a = ofⁿ ¬a
of {b = true } a = ofʸ a
of : if x then A else ¬ A → Reflects A x
of {x = false} ¬a = ofⁿ ¬a
of {x = true } a = ofʸ a

invert : ∀ {b} → Reflects A b → if b then A else ¬ A
invert : Reflects A x → if x then A else ¬ A
invert (ofʸ a) = a
invert (ofⁿ ¬a) = ¬a

------------------------------------------------------------------------
-- Interaction with negation, product, sums etc.

infixr 1 _⊎-reflects_
infixr 2 _×-reflects_ _→-reflects_

T-reflects : ∀ x → Reflects (T x) x
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 : Reflects A x → Reflects (¬ A) (not x)
¬-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)
_×-reflects_ : Reflects A x → Reflects B y → Reflects (A × B) (x ∧ y)
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)
_⊎-reflects_ : Reflects A x → Reflects B y → Reflects (A ⊎ B) (x ∨ y)
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)
_→-reflects_ : Reflects A x → Reflects B y → Reflects (A → B) (not x ∨ y)
ofʸ a →-reflects ofʸ b = ofʸ (const b)
ofʸ a →-reflects ofⁿ ¬b = ofⁿ (¬b ∘ (_$ a))
ofⁿ ¬a →-reflects _ = ofʸ (⊥-elim ∘ ¬a)

------------------------------------------------------------------------
-- Other lemmas

fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Reflects A b
fromEquivalence {b = true} sound complete = ofʸ (sound _)
fromEquivalence {b = false} sound complete = ofⁿ complete
fromEquivalence : (T x → A) → (A → T x) → Reflects A x
fromEquivalence {x = true} sound complete = ofʸ (sound _)
fromEquivalence {x = false} sound complete = ofⁿ complete

-- `Reflects` is deterministic.
det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
det : Reflects A x → Reflects A y → x ≡ y
det (ofʸ a) (ofʸ _) = refl
det (ofʸ a) (ofⁿ ¬a) = contradiction a ¬a
det (ofⁿ ¬a) (ofʸ a) = contradiction a ¬a
Expand Down