[Agda] Boolean and Decidable comparison

[Philip Wadler]

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/

On 15 February 2018 at 18:35, Miëtek Bak <mietek at bak.io> wrote:

> 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.
>
>
>
> On 15 Feb 2018, at 20:26, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>
> 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/
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/d5e23d95/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/d5e23d95/attachment-0001.ksh>