[Agda] Boolean and Decidable comparison
Guillaume Allais
guillaume.allais at ens-lyon.org
Fri Feb 16 14:41:33 CET 2018
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
> <mailto: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.
>
>
>
>
> 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/20180216/83b677c0/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/83b677c0/attachment-0001.sig>
More information about the Agda
mailing list