<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">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">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">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">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">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">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">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">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">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">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>