[Agda] Boolean and Decidable comparison

[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/

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

> 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/
>
> 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
>>
>>
>>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/2d3c3774/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/2d3c3774/attachment.ksh>