[Agda] Boolean and Decidable comparison

Fri Feb 16 18:53:48 CET 2018

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 <
guillaume.allais at ens-lyon.org> wrote:

> 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
>
> On 16/02/18 14:15, Philip Wadler wrote:
>
> 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.
>>
>>
>>
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> 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/20180216/a67efe2f/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/a67efe2f/attachment-0001.ksh>