[Agda] Boolean and Decidable comparison

[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

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/5e5a2116/attachment.html>