[Agda] Boolean and Decidable comparison

[Miëtek Bak]

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.



> On 15 Feb 2018, at 21: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/ <http://homepages.inf.ed.ac.uk/wadler/>
>> On 15 February 2018 at 18:35, Miëtek Bak <mietek at bak.io <mailto: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 <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 <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 <mailto: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/ <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 <mailto:Agda at lists.chalmers.se>
>>> 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
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/47e044ed/attachment-0001.html>