Discussion:
Boolean and Decidable comparison
(too old to reply)
Philip Wadler
2018-02-15 20:26:55 UTC
Permalink
I presume there are operations in the standard prelude to compute whether
one natural is less than or equal to another with types

Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)

But I can't find them. Where are they and what are they called? Cheers, -- P

PS. Using ^C ^Z to search Everything.agda (see previous thread) for Nat
Bool or Nat Dec yields nothing. Indeed, using it to search for Nat gives:

Definitions about Nat

followed by nothing! I'm not sure why.




. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Miëtek Bak
2018-02-15 20:35:28 UTC
Permalink
The standard library defines synonyms that obscure the underlying types. I haven’t found C-c C-z to be of much use; I grep the source trees instead.

$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_

Here’s the second operation:
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179

We can obtain the first operation via projection:
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822
--
M.
I presume there are operations in the standard prelude to compute whether one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/ <http://homepages.inf.ed.ac.uk/wadler/>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-02-15 21:21:29 UTC
Permalink
Thanks to Amr and Miëtek for their responses. Here is a follow up question.

First, is there a name in the standard library for the operation called _≀ᵇ_
below?

Second, and less trivially, is there a way to fill in the holes in the
proof of _≀?′_ below, or to complete a proof along similar lines?

Many thanks, -- P


open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)

data Bool : Set where
true : Bool
false : Bool

T : Bool → Set
T true = ⊀
T false = ⊥

_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n

≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n

≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn = s≀s (≀ᵇ→≀ m n m≀ᵇn)

data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A

_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }

_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})


. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Miëtek Bak
The standard library defines synonyms that obscure the underlying types.
I haven’t found C-c C-z to be of much use; I grep the source trees instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822
--
M.
I presume there are operations in the standard prelude to compute whether
one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
PS. Using ^C ^Z to search Everything.agda (see previous thread) for Nat
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Miëtek Bak
2018-02-15 21:49:24 UTC
Permalink
First, is there a name in the standard library for the operation called _≀ᵇ_ below?
I don’t think the _≀ᵇ_ operation appears in the standard library. Instead, the library supplies a projection function that lets us define _≀ᵇ_ in one line.

open import Data.Bool using (Bool; T)
open import Data.Nat using (ℕ; _≀_; _≀?_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)

_≀ᵇ_ : ℕ → ℕ → Bool
m ≀ᵇ n = ⌊ m ≀? n ⌋

≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ p = fromWitness p

≀ᵇ→≀ : ∀ {m n : ℕ} → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ p = toWitness p

_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n = m ≀? n

Alternative type notation using synonyms supplied by the library:

≀→≀ᵇ′ : ∀ {m n : ℕ} → m ≀ n → True (m ≀? n)
≀→≀ᵇ′ p = fromWitness p

≀ᵇ→≀′ : ∀ {m n : ℕ} → True (m ≀? n) → m ≀ n
≀ᵇ→≀′ p = toWitness p

_≀?″_ : Decidable _≀_
m ≀?″ n = m ≀? n
--
M.
Second, and less trivially, is there a way to fill in the holes in the proof of _≀?′_ below, or to complete a proof along similar lines?
Many thanks, -- P
open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)
data Bool : Set where
true : Bool
false : Bool
T : Bool → Set
T true = ⊀
T false = ⊥
_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n
≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn = s≀s (≀ᵇ→≀ m n m≀ᵇn)
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/ <http://homepages.inf.ed.ac.uk/wadler/>
The standard library defines synonyms that obscure the underlying types. I haven’t found C-c C-z to be of much use; I grep the source trees instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179 <https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179>
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822 <https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822>
--
M.
I presume there are operations in the standard prelude to compute whether one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/ <http://homepages.inf.ed.ac.uk/wadler/>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Miëtek Bak
2018-02-15 21:55:10 UTC
Permalink
Ah, I forgot there is a similar _<_ operation supplied as part of Agda built-ins. Note that the Agda.Builtin.* modules are available even when the standard library is not installed.

https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#651
--
M.
Post by Miëtek Bak
First, is there a name in the standard library for the operation called _≀ᵇ_ below?
I don’t think the _≀ᵇ_ operation appears in the standard library. Instead, the library supplies a projection function that lets us define _≀ᵇ_ in one line.
open import Data.Bool using (Bool; T)
open import Data.Nat using (ℕ; _≀_; _≀?_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)
_≀ᵇ_ : ℕ → ℕ → Bool
m ≀ᵇ n = ⌊ m ≀? n ⌋
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ p = fromWitness p
≀ᵇ→≀ : ∀ {m n : ℕ} → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ p = toWitness p
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n = m ≀? n
≀→≀ᵇ′ : ∀ {m n : ℕ} → m ≀ n → True (m ≀? n)
≀→≀ᵇ′ p = fromWitness p
≀ᵇ→≀′ : ∀ {m n : ℕ} → True (m ≀? n) → m ≀ n
≀ᵇ→≀′ p = toWitness p
_≀?″_ : Decidable _≀_
m ≀?″ n = m ≀? n
--
M.
Second, and less trivially, is there a way to fill in the holes in the proof of _≀?′_ below, or to complete a proof along similar lines?
Many thanks, -- P
open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)
data Bool : Set where
true : Bool
false : Bool
T : Bool → Set
T true = ⊀
T false = ⊥
_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n
≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn = s≀s (≀ᵇ→≀ m n m≀ᵇn)
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/ <http://homepages.inf.ed.ac.uk/wadler/>
The standard library defines synonyms that obscure the underlying types. I haven’t found C-c C-z to be of much use; I grep the source trees instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179 <https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179>
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822 <https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822>
--
M.
I presume there are operations in the standard prelude to compute whether one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/ <http://homepages.inf.ed.ac.uk/wadler/>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
Philip Wadler
2018-02-16 13:15:24 UTC
Permalink
Thanks, Miëtek. That's clearly the cleanest way to define those functions.
But, I was starting with _≀ᵇ_ as in my notes for pedagogical purposes, not
because I need those particular functions. I'm still curious as to
whether _≀?′_
can be defined along the lines I sketch. Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Philip Wadler
First, is there a name in the standard library for the operation called _≀ᵇ_
below?
I don’t think the _≀ᵇ_ operation appears in the standard library.
Instead, the library supplies a projection function that lets us define _≀ᵇ_
in one line.
open import Data.Bool using (Bool; T)
open import Data.Nat using (ℕ; _≀_; _≀?_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)
_≀ᵇ_ : ℕ → ℕ → Bool
m ≀ᵇ n = ⌊ m ≀? n ⌋
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ p = fromWitness p
≀ᵇ→≀ : ∀ {m n : ℕ} → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ p = toWitness p
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n = m ≀? n
≀→≀ᵇ′ : ∀ {m n : ℕ} → m ≀ n → True (m ≀? n)
≀→≀ᵇ′ p = fromWitness p
≀ᵇ→≀′ : ∀ {m n : ℕ} → True (m ≀? n) → m ≀ n
≀ᵇ→≀′ p = toWitness p
_≀?″_ : Decidable _≀_
m ≀?″ n = m ≀? n
--
M.
Second, and less trivially, is there a way to fill in the holes in the
proof of _≀?′_ below, or to complete a proof along similar lines?
Many thanks, -- P
open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)
data Bool : Set where
true : Bool
false : Bool
T : Bool → Set
T true = ⊀
T false = ⊥
_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n
≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn = s≀s (≀ᵇ→≀ m n m≀ᵇn)
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Miëtek Bak
The standard library defines synonyms that obscure the underlying types.
I haven’t found C-c C-z to be of much use; I grep the source trees instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822
--
M.
I presume there are operations in the standard prelude to compute whether
one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
PS. Using ^C ^Z to search Everything.agda (see previous thread) for Nat
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Guillaume Allais
2018-02-16 13:41:33 UTC
Permalink
Hi Phil,

There are a few different possibilities here:

* Using a multi-with `with x | y` so that the result of evaluating
`x` gets abstracted in the `y` expression like so:

===========================================================
module convo where

 _≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
 m ≀?′ n with m ≀ᵇ n | ≀ᵇ→≀ m n | ≀→≀ᵇ {m} {n}
 ... | true  | p | _   = yes (p tt)
 ... | false | _ | ¬p  = no ¬p
===========================================================

* Using the `inspect` idiom defined in PropositionalEquality to
remember that the boolean you get was created by calling `m ≀ᵇ n`

===========================================================
module inspect where

 open import Relation.Binary.PropositionalEquality

 _≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
 m ≀?′ n with m ≀ᵇ n | inspect (m ≀ᵇ_) n
 ... | true  | [ eq ] = yes (≀ᵇ→≀ m n (subst T (sym eq) tt))
 ... | false | [ eq ] = no  (contraposition ≀→≀ᵇ (subst (λ b → ¬ T b)
(sym eq) (λ x → x)))
===========================================================

* Finally doing away with your proofs that `≀→≀ᵇ` and `≀ᵇ→≀`
and instead using a ssreflect-style `Reflects` idiom and proving
directly that ≀?⇔≀ᵇ:

===========================================================
module reflects where

  data Reflects (P : Set) : Bool → Set where
    yes : (p : P)    → Reflects P true
    no  : (¬p : ¬ P) → Reflects P false

  map : ∀ {P Q} → (P → Q) → (Q → P) → ∀ {b} → Reflects P b → Reflects Q b
  map p⇒q q⇒p (yes p) = yes (p⇒q p)
  map p⇒q q⇒p (no ¬p) = no (λ q → ¬p (q⇒p q))

  s≀s-inj : ∀ {m n} → suc m ≀ suc n → m ≀ n
  s≀s-inj (s≀s p) = p

  ≀?⇔≀ᵇ : ∀ m n → Reflects (m ≀ n) (m ≀ᵇ n)
  ≀?⇔≀ᵇ zero    n       = yes z≀n
  ≀?⇔≀ᵇ (suc m) zero    = no (λ ())
  ≀?⇔≀ᵇ (suc m) (suc n) = map s≀s s≀s-inj (≀?⇔≀ᵇ m n)

  dec-Reflects : ∀ {b P} → Reflects P b → Dec P
  dec-Reflects (yes p) = yes p
  dec-Reflects (no ¬p) = no ¬p
===========================================================

Cheers,
--
gallais
Post by Philip Wadler
Thanks, Miëtek. That's clearly the cleanest way to define those
functions. But, I was starting with _≀ᵇ_ as in my notes for
pedagogical purposes, not because I need those particular functions.
I'm still curious as to whether _≀?′_ can be defined along the lines I
sketch. Cheers, -- P
.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Philip Wadler
First, is there a name in the standard library for the operation
called _≀ᵇ_ below?
I don’t think the _≀ᵇ_ operation appears in the standard library. 
Instead, the library supplies a projection function that lets us
define _≀ᵇ_ in one line.
open import Data.Bool using (Bool; T)
open import Data.Nat using (ℕ; _≀_; _≀?_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (⌊_⌋; True;
toWitness; fromWitness)
_≀ᵇ_ : ℕ → ℕ → Bool
m ≀ᵇ n = ⌊ m ≀? n ⌋
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ p = fromWitness p
≀ᵇ→≀ : ∀ {m n : ℕ} → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ p = toWitness p
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n = m ≀? n
≀→≀ᵇ′ : ∀ {m n : ℕ} → m ≀ n → True (m ≀? n)
≀→≀ᵇ′ p = fromWitness p
≀ᵇ→≀′ : ∀ {m n : ℕ} → True (m ≀? n) → m ≀ n
≀ᵇ→≀′ p = toWitness p
_≀?″_ : Decidable _≀_
m ≀?″ n = m ≀? n
-- 
M.
Post by Philip Wadler
Second, and less trivially, is there a way to fill in the holes
in the proof of _≀?′_ below, or to complete a proof along similar
lines?
Many thanks, -- P
open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)
data Bool : Set where
  true : Bool
  false : Bool
T : Bool → Set
T true = ⊀
T false = ⊥
_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n
≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn =  s≀s (≀ᵇ→≀ m n m≀ᵇn)
data Dec (A : Set) : Set where
  yes : A → Dec A
  no : ¬ A → Dec A
_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})
.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
<http://homepages.inf.ed.ac.uk/wadler/>
The standard library defines synonyms that obscure the
underlying types.  I haven’t found C-c C-z to be of much use;
I grep the source trees instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179
<https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179>
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822
<https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822>
-- 
M.
Post by Philip Wadler
I presume there are operations in the standard prelude to
compute whether one natural is less than or equal to another
with types
  Nat -> Nat -> Bool
  (n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they
called? Cheers, -- P
PS. Using ^C ^Z to search Everything.agda (see previous
thread) for Nat Bool or Nat Dec yields nothing. Indeed,
  Definitions about Nat
followed by nothing! I'm not sure why.
 
.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
<http://homepages.inf.ed.ac.uk/wadler/>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-02-16 17:53:48 UTC
Permalink
Thank you very much, Guillaume. Exactly what I needed to learn! Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 16 February 2018 at 11:41, Guillaume Allais <
Post by Guillaume Allais
Hi Phil,
* Using a multi-with `with x | y` so that the result of evaluating
===========================================================
module convo where
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n | ≀ᵇ→≀ m n | ≀→≀ᵇ {m} {n}
... | true | p | _ = yes (p tt)
... | false | _ | ¬p = no ¬p
===========================================================
* Using the `inspect` idiom defined in PropositionalEquality to
remember that the boolean you get was created by calling `m ≀ᵇ n`
===========================================================
module inspect where
open import Relation.Binary.PropositionalEquality
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n | inspect (m ≀ᵇ_) n
... | true | [ eq ] = yes (≀ᵇ→≀ m n (subst T (sym eq) tt))
... | false | [ eq ] = no (contraposition ≀→≀ᵇ (subst (λ b → ¬ T b) (sym
eq) (λ x → x)))
===========================================================
* Finally doing away with your proofs that `≀→≀ᵇ` and `≀ᵇ→≀`
and instead using a ssreflect-style `Reflects` idiom and proving
===========================================================
module reflects where
data Reflects (P : Set) : Bool → Set where
yes : (p : P) → Reflects P true
no : (¬p : ¬ P) → Reflects P false
map : ∀ {P Q} → (P → Q) → (Q → P) → ∀ {b} → Reflects P b → Reflects Q b
map p⇒q q⇒p (yes p) = yes (p⇒q p)
map p⇒q q⇒p (no ¬p) = no (λ q → ¬p (q⇒p q))
s≀s-inj : ∀ {m n} → suc m ≀ suc n → m ≀ n
s≀s-inj (s≀s p) = p
≀?⇔≀ᵇ : ∀ m n → Reflects (m ≀ n) (m ≀ᵇ n)
≀?⇔≀ᵇ zero n = yes z≀n
≀?⇔≀ᵇ (suc m) zero = no (λ ())
≀?⇔≀ᵇ (suc m) (suc n) = map s≀s s≀s-inj (≀?⇔≀ᵇ m n)
dec-Reflects : ∀ {b P} → Reflects P b → Dec P
dec-Reflects (yes p) = yes p
dec-Reflects (no ¬p) = no ¬p
===========================================================
Cheers,
--
gallais
Thanks, Miëtek. That's clearly the cleanest way to define those functions.
But, I was starting with _≀ᵇ_ as in my notes for pedagogical purposes,
not because I need those particular functions. I'm still curious as to
whether _≀?′_ can be defined along the lines I sketch. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Philip Wadler
First, is there a name in the standard library for the operation called _≀ᵇ_
below?
I don’t think the _≀ᵇ_ operation appears in the standard library.
Instead, the library supplies a projection function that lets us define _≀ᵇ_
in one line.
open import Data.Bool using (Bool; T)
open import Data.Nat using (ℕ; _≀_; _≀?_)
open import Relation.Nullary using (Dec)
open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness;
fromWitness)
_≀ᵇ_ : ℕ → ℕ → Bool
m ≀ᵇ n = ⌊ m ≀? n ⌋
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ p = fromWitness p
≀ᵇ→≀ : ∀ {m n : ℕ} → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ p = toWitness p
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n = m ≀? n
≀→≀ᵇ′ : ∀ {m n : ℕ} → m ≀ n → True (m ≀? n)
≀→≀ᵇ′ p = fromWitness p
≀ᵇ→≀′ : ∀ {m n : ℕ} → True (m ≀? n) → m ≀ n
≀ᵇ→≀′ p = toWitness p
_≀?″_ : Decidable _≀_
m ≀?″ n = m ≀? n
--
M.
Second, and less trivially, is there a way to fill in the holes in the
proof of _≀?′_ below, or to complete a proof along similar lines?
Many thanks, -- P
open import Data.Nat using (ℕ; zero; suc; _≀_; z≀n; s≀s)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Data.Unit using (⊀; tt)
open import Data.Empty using (⊥)
data Bool : Set where
true : Bool
false : Bool
T : Bool → Set
T true = ⊀
T false = ⊥
_≀ᵇ_ : ℕ → ℕ → Bool
zero ≀ᵇ n = true
suc m ≀ᵇ zero = false
suc m ≀ᵇ suc n = m ≀ᵇ n
≀→≀ᵇ : ∀ {m n : ℕ} → m ≀ n → T (m ≀ᵇ n)
≀→≀ᵇ z≀n = tt
≀→≀ᵇ (s≀s m≀n) = ≀→≀ᵇ m≀n
≀ᵇ→≀ : ∀ (m n : ℕ) → T (m ≀ᵇ n) → m ≀ n
≀ᵇ→≀ zero n tt = z≀n
≀ᵇ→≀ (suc m) zero ()
≀ᵇ→≀ (suc m) (suc n) m≀ᵇn = s≀s (≀ᵇ→≀ m n m≀ᵇn)
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
_≀?_ : ∀ (m n : ℕ) → Dec (m ≀ n)
zero ≀? n = yes z≀n
suc m ≀? zero = no λ()
suc m ≀? suc n with m ≀? n
... | yes m≀n = yes (s≀s m≀n)
... | no ¬m≀n = no λ{ (s≀s m≀n) → ¬m≀n m≀n }
_≀?′_ : ∀ (m n : ℕ) → Dec (m ≀ n)
m ≀?′ n with m ≀ᵇ n
... | true = yes (≀ᵇ→≀ m n {!!})
... | false = no (contraposition ≀→≀ᵇ {!!})
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
Post by Miëtek Bak
The standard library defines synonyms that obscure the underlying
types. I haven’t found C-c C-z to be of much use; I grep the source trees
instead.
$ git grep Dec | grep Nat
src/Data/Nat/Base.agda:156:_≀?_ : Decidable _≀_
https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179
https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822
--
M.
I presume there are operations in the standard prelude to compute
whether one natural is less than or equal to another with types
Nat -> Nat -> Bool
(n : Nat) -> (m : Nat) -> Dec (m \leq n)
But I can't find them. Where are they and what are they called? Cheers, -- P
PS. Using ^C ^Z to search Everything.agda (see previous thread) for Nat
Definitions about Nat
followed by nothing! I'm not sure why.
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Loading...