<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<tt>Hi Phil,<br>
<br>
There are a few different possibilities here:<br>
<br>
* Using a multi-with `with x | y` so that the result of evaluating<br>
`x` gets abstracted in the `y` expression like so:<br>
<br>
===========================================================</tt><tt><tt><br>
module convo where<br>
<br>
_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)<br>
m ≤?′ n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}<br>
... | true | p | _ = yes (p tt)<br>
... | false | _ | ¬p = no ¬p<br>
===========================================================<br>
<br>
* Using the `inspect` idiom defined in PropositionalEquality to<br>
remember that the boolean you get was created by calling `</tt></tt><tt><tt><tt><tt><tt>m
≤ᵇ n`</tt></tt></tt><br>
<br>
</tt></tt><tt><tt><tt>===========================================================<br>
module inspect where<br>
<br>
open import Relation.Binary.PropositionalEquality<br>
<br>
_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)<br>
m ≤?′ n with m ≤ᵇ n | inspect (m ≤ᵇ_) n<br>
... | true | [ eq ] = yes (≤ᵇ→≤ m n (subst T (sym eq) tt))<br>
... | false | [ eq ] = no (contraposition ≤→≤ᵇ (subst (λ b →
¬ T b) (sym eq) (λ x → x)))<br>
</tt></tt></tt><tt><tt><tt><tt>===========================================================<br>
<br>
* Finally doing away with your proofs that `≤→≤ᵇ` and `≤ᵇ→≤`<br>
and instead using a ssreflect-style `Reflects` idiom and
proving<br>
directly that </tt></tt></tt></tt><tt><tt><tt><tt><tt><tt><tt><tt>≤?⇔≤ᵇ</tt></tt></tt></tt>:<br>
</tt></tt></tt></tt><br>
<tt><tt><tt><tt><tt><tt><tt><tt>===========================================================<br>
</tt></tt></tt></tt>module reflects where<br>
<br>
data Reflects (P : Set) : Bool → Set where<br>
yes : (p : P) → Reflects P true<br>
no : (¬p : ¬ P) → Reflects P false<br>
<br>
map : ∀ {P Q} → (P → Q) → (Q → P) → ∀ {b} → Reflects P b →
Reflects Q b<br>
map p⇒q q⇒p (yes p) = yes (p⇒q p)<br>
map p⇒q q⇒p (no ¬p) = no (λ q → ¬p (q⇒p q))<br>
<br>
s≤s-inj : ∀ {m n} → suc m ≤ suc n → m ≤ n<br>
s≤s-inj (s≤s p) = p<br>
<br>
≤?⇔≤ᵇ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)<br>
≤?⇔≤ᵇ zero n = yes z≤n<br>
≤?⇔≤ᵇ (suc m) zero = no (λ ())<br>
≤?⇔≤ᵇ (suc m) (suc n) = map s≤s s≤s-inj (≤?⇔≤ᵇ m n)<br>
<br>
dec-Reflects : ∀ {b P} → Reflects P b → Dec P<br>
dec-Reflects (yes p) = yes p<br>
dec-Reflects (no ¬p) = no ¬p</tt></tt></tt></tt><br>
<tt><tt><tt><tt><tt><tt><tt><tt>===========================================================<br>
<br>
Cheers,<br>
--<br>
gallais<br>
<br>
</tt></tt></tt></tt></tt></tt></tt></tt>
<div class="moz-cite-prefix">On 16/02/18 14:15, Philip Wadler wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAESRbco2ECzogoqQKewxMyS0JP+=4MO=aoFBx0nuiZZ4UzBK8A@mail.gmail.com">
<div dir="ltr">Thanks, Miëtek. That's clearly the cleanest way to
define those functions. But, I was starting with _<span
style="color:rgb(80,0,80);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">≤ᵇ_
as in my notes for pedagogical purposes, not because I need
those particular functions. I'm still curious as to whether <span
style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">_≤?′_
can be defined along the lines I sketch. Cheers, -- P</span></span><br>
<div class="gmail_extra"><br clear="all">
<div>
<div class="gmail_signature"
data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of
Theoretical Computer Science,<br>
. /\ School of Informatics, University of
Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a
href="http://homepages.inf.ed.ac.uk/wadler/"
target="_blank" moz-do-not-send="true">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 15 February 2018 at 19:49, Miëtek
Bak <span dir="ltr"><<a href="mailto:mietek@bak.io"
target="_blank" moz-do-not-send="true">mietek@bak.io</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word">
<div><span class="">
<blockquote type="cite">
<div dir="ltr">
<div>First, is there a name in the standard
library for the operation called <span
style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-variant-ligatures:normal;background-color:rgb(255,255,255);float:none;display:inline">_≤ᵇ_
below?</span></div>
</div>
</blockquote>
<div><br>
</div>
</span>
<div>I don’t think the <span
style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;background-color:rgb(255,255,255)">_≤ᵇ_</span> operation
appears in the standard library. Instead, the
library supplies a projection function that lets us
define <span
style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;background-color:rgb(255,255,255)">_≤ᵇ_
in one line.</span></div>
<div><br>
</div>
<div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>open
import Data.Bool using (Bool; T)</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>open
import Data.Nat using (ℕ; _≤_; _≤?_)</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>open
import Relation.Nullary using (Dec)</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>open
import Relation.Nullary.Decidable using (⌊_⌋;
True; toWitness; fromWitness)</div>
<span class="">
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>_≤ᵇ_
: ℕ → ℕ → Bool</div>
</span>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>m
≤ᵇ n = ⌊ m ≤? n ⌋</div>
<span class="">
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤→≤ᵇ
: ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)</div>
</span>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤→≤ᵇ
p = fromWitness p</div>
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤ᵇ→≤
: ∀ {m n : ℕ} → T (m ≤ᵇ n) → m ≤ n</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤ᵇ→≤
p = toWitness p</div>
<span class="">
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>_≤?′_
: ∀ (m n : ℕ) → Dec (m ≤ n)</div>
</span>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>m
≤?′ n = m ≤? n</div>
<div><br>
</div>
<div>Alternative type notation using synonyms
supplied by the library:</div>
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤→≤ᵇ′
: ∀ {m n : ℕ} → m ≤ n → True (m ≤? n)</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤→≤ᵇ′
p = fromWitness p</div>
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤ᵇ→≤′
: ∀ {m n : ℕ} → True (m ≤? n) → m ≤ n</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>≤ᵇ→≤′
p = toWitness p</div>
<div><br>
</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>_≤?″_
: Decidable _≤_</div>
<div><span class="m_-944103099344809019Apple-tab-span" style="white-space:pre-wrap"> </span>m
≤?″ n = m ≤? n</div>
<span class="HOEnZb"><font color="#888888">
<div><br>
</div>
<div><br>
</div>
<div>-- </div>
<div>M.</div>
<div><br>
</div>
</font></span></div>
<div>
<div class="h5"><br>
<blockquote type="cite">
<div dir="ltr">
<div><br>
</div>
<div>Second, and less trivially, is there a
way to fill in the holes in the proof of <span
style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">_≤?′_
below, or to complete a proof along
similar lines?</span></div>
<div><br>
</div>
<div>Many thanks, -- P<br>
<div><br>
</div>
</div>
<div><br>
</div>
<div>
<div>open import Data.Nat using (ℕ; zero;
suc; _≤_; z≤n; s≤s)</div>
<div>open import Relation.Nullary using (¬_)</div>
<div>open import Relation.Nullary.Negation
using (contraposition)</div>
<div>open import Data.Unit using (⊤; tt)</div>
<div>open import Data.Empty using (⊥)</div>
<div><br>
</div>
<div>data Bool : Set where</div>
<div> true : Bool</div>
<div> false : Bool</div>
<div><br>
</div>
<div>T : Bool → Set</div>
<div>T true = ⊤</div>
<div>T false = ⊥</div>
<div><br>
</div>
<div>_≤ᵇ_ : ℕ → ℕ → Bool</div>
<div>zero ≤ᵇ n = true</div>
<div>suc m ≤ᵇ zero = false</div>
<div>suc m ≤ᵇ suc n = m ≤ᵇ n</div>
<div><br>
</div>
<div>≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)</div>
<div>≤→≤ᵇ z≤n = tt</div>
<div>≤→≤ᵇ (s≤s m≤n) = ≤→≤ᵇ m≤n</div>
<div><br>
</div>
<div>≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n</div>
<div>≤ᵇ→≤ zero n tt = z≤n</div>
<div>≤ᵇ→≤ (suc m) zero ()</div>
<div>≤ᵇ→≤ (suc m) (suc n) m≤ᵇn = s≤s (≤ᵇ→≤
m n m≤ᵇn)</div>
<div><br>
</div>
<div>data Dec (A : Set) : Set where</div>
<div> yes : A → Dec A</div>
<div> no : ¬ A → Dec A</div>
<div><br>
</div>
<div>_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div>
<div>zero ≤? n = yes z≤n</div>
<div>suc m ≤? zero = no λ()</div>
<div>suc m ≤? suc n with m ≤? n</div>
<div>... | yes m≤n = yes (s≤s m≤n)</div>
<div>... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n
m≤n }</div>
<div><br>
</div>
<div>_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div>
<div>m ≤?′ n with m ≤ᵇ n</div>
<div>... | true = yes (≤ᵇ→≤ m n {!!})</div>
<div>... | false = no (contraposition ≤→≤ᵇ
{!!})</div>
</div>
<div><br>
</div>
</div>
<div class="gmail_extra"><br clear="all">
<div>
<div
class="m_-944103099344809019gmail_signature"
data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler,
Professor of Theoretical Computer
Science,<br>
. /\ School of Informatics,
University of Edinburgh<br>
</div>
<div>. / \ and Senior Research
Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a
href="http://homepages.inf.ed.ac.uk/wadler/"
target="_blank"
moz-do-not-send="true">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
<br>
<div class="gmail_quote">On 15 February 2018
at 18:35, Miëtek Bak <span dir="ltr"><<a
href="mailto:mietek@bak.io"
target="_blank" moz-do-not-send="true">mietek@bak.io</a>></span>
wrote:<br>
<blockquote class="gmail_quote"
style="margin:0 0 0 .8ex;border-left:1px
#ccc solid;padding-left:1ex">
<div style="word-wrap:break-word">
<div>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.</div>
<div><br>
</div>
<div>$ git grep Dec | grep Nat</div>
<div>src/Data/Nat/Base.agda:156:_≤?<wbr>_
: Decidable _≤_</div>
<div><br>
</div>
<div>Here’s the second operation:</div>
<div><a
href="https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179"
target="_blank"
moz-do-not-send="true">https://agda.github.io/agda-st<wbr>dlib/Data.Nat.Base.html#3179</a></div>
<div><br>
</div>
<div>We can obtain the first operation
via projection:</div>
<div><a
href="https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822"
target="_blank"
moz-do-not-send="true">https://agda.github.io/agda-st<wbr>dlib/Relation.Nullary.Decidabl<wbr>e.html#822</a></div>
<span
class="m_-944103099344809019HOEnZb"><font
color="#888888">
<div><br>
</div>
<div><br>
</div>
<div>-- </div>
<div>M.</div>
<div><br>
</div>
<div><br>
</div>
</font></span>
<div><br>
<div>
<blockquote type="cite">
<div>
<div
class="m_-944103099344809019h5">
<div>On 15 Feb 2018, at 20:26,
Philip Wadler <<a
href="mailto:wadler@inf.ed.ac.uk"
target="_blank"
moz-do-not-send="true">wadler@inf.ed.ac.uk</a>>
wrote:</div>
<br
class="m_-944103099344809019m_2941185566432368495Apple-interchange-newline">
</div>
</div>
<div>
<div>
<div
class="m_-944103099344809019h5">
<div dir="ltr">
<div>I presume there are
operations in the
standard prelude to
compute whether one
natural is less than or
equal to another with
types</div>
<div><br>
</div>
<div> Nat -> Nat ->
Bool</div>
<div> (n : Nat) -> (m
: Nat) -> Dec (m \leq
n)</div>
<div><br>
</div>
<div>But I can't find
them. Where are they and
what are they called?
Cheers, -- P</div>
<div><br>
</div>
<div>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:</div>
<div><br>
</div>
<div> Definitions about
Nat</div>
<div><br>
</div>
<div>followed by nothing!
I'm not sure why.</div>
<div><br>
</div>
<div> </div>
<div><br>
</div>
<br clear="all">
<div>
<div
class="m_-944103099344809019m_2941185566432368495gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">.
\ Philip Wadler,
Professor of
Theoretical
Computer
Science,<br>
. /\ School of
Informatics,
University of
Edinburgh<br>
</div>
<div>. / \ and
Senior Research
Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a
href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank"
moz-do-not-send="true">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<span>
The University of Edinburgh is
a charitable body, registered
in<br>
Scotland, with registration
number SC005336.<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a
href="mailto:Agda@lists.chalmers.se"
target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
target="_blank"
moz-do-not-send="true">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</span></div>
</blockquote>
</div>
<br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
The University of Edinburgh is a charitable
body, registered in<br>
Scotland, with registration number SC005336.<br>
</blockquote>
</div>
</div>
</div>
<br>
</div>
</blockquote>
</div>
<br>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>