<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Ah, I forgot there is a similar _<_ operation supplied as part of Agda built-ins. Note that the Agda.Builtin.* modules are available even when the standard library is not installed.</div><div class=""><br class=""></div><div class=""><a href="https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#651" class="">https://agda.github.io/agda-stdlib/Agda.Builtin.Nat.html#651</a></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">-- </div><div class="">M.</div><div class=""><br class=""></div><div class=""><br class=""></div><br class=""><div><blockquote type="cite" class=""><div class="">On 15 Feb 2018, at 21:49, Miëtek Bak <<a href="mailto:mietek@bak.io" class="">mietek@bak.io</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class="">First, is there a name in the standard library for the operation called <span class="" 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 class=""><br class=""></div><div class="">I don’t think the <span class="" 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 class="" 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 class=""><br class=""></div><div class=""><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>open import Data.Bool using (Bool; T)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>open import Data.Nat using (ℕ; _≤_; _≤?_)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>open import Relation.Nullary using (Dec)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>_≤ᵇ_ : ℕ → ℕ → Bool</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>m ≤ᵇ n = ⌊ m ≤? n ⌋</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤→≤ᵇ p = fromWitness p</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤ᵇ→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ n) → m ≤ n</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤ᵇ→≤ p = toWitness p</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>m ≤?′ n = m ≤? n</div><div class=""><br class=""></div><div class="">Alternative type notation using synonyms supplied by the library:</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤→≤ᵇ′ : ∀ {m n : ℕ} → m ≤ n → True (m ≤? n)</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤→≤ᵇ′ p = fromWitness p</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤ᵇ→≤′ : ∀ {m n : ℕ} → True (m ≤? n) → m ≤ n</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>≤ᵇ→≤′ p = toWitness p</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>_≤?″_ : Decidable _≤_</div><div class=""><span class="Apple-tab-span" style="white-space: pre;"> </span>m ≤?″ n = m ≤? n</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">-- </div><div class="">M.</div><div class=""><br class=""></div></div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Second, and less trivially, is there a way to fill in the holes in the proof of <span class="" 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); float: none; display: inline;">_≤?′_ below, or to complete a proof along similar lines?</span></div><div class=""><br class=""></div><div class="">Many thanks, -- P<br class=""><div class=""><br class=""></div></div><div class=""><br class=""></div><div class=""><div class="">open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)</div><div class="">open import Relation.Nullary using (¬_)</div><div class="">open import Relation.Nullary.Negation using (contraposition)</div><div class="">open import Data.Unit using (⊤; tt)</div><div class="">open import Data.Empty using (⊥)</div><div class=""><br class=""></div><div class="">data Bool : Set where</div><div class=""> true : Bool</div><div class=""> false : Bool</div><div class=""><br class=""></div><div class="">T : Bool → Set</div><div class="">T true = ⊤</div><div class="">T false = ⊥</div><div class=""><br class=""></div><div class="">_≤ᵇ_ : ℕ → ℕ → Bool</div><div class="">zero ≤ᵇ n = true</div><div class="">suc m ≤ᵇ zero = false</div><div class="">suc m ≤ᵇ suc n = m ≤ᵇ n</div><div class=""><br class=""></div><div class="">≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)</div><div class="">≤→≤ᵇ z≤n = tt</div><div class="">≤→≤ᵇ (s≤s m≤n) = ≤→≤ᵇ m≤n</div><div class=""><br class=""></div><div class="">≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n</div><div class="">≤ᵇ→≤ zero n tt = z≤n</div><div class="">≤ᵇ→≤ (suc m) zero ()</div><div class="">≤ᵇ→≤ (suc m) (suc n) m≤ᵇn = s≤s (≤ᵇ→≤ m n m≤ᵇn)</div><div class=""><br class=""></div><div class="">data Dec (A : Set) : Set where</div><div class=""> yes : A → Dec A</div><div class=""> no : ¬ A → Dec A</div><div class=""><br class=""></div><div class="">_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div><div class="">zero ≤? n = yes z≤n</div><div class="">suc m ≤? zero = no λ()</div><div class="">suc m ≤? suc n with m ≤? n</div><div class="">... | yes m≤n = yes (s≤s m≤n)</div><div class="">... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n m≤n }</div><div class=""><br class=""></div><div class="">_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div><div class="">m ≤?′ n with m ≤ᵇ n</div><div class="">... | true = yes (≤ᵇ→≤ m n {!!})</div><div class="">... | false = no (contraposition ≤→≤ᵇ {!!})</div></div><div class=""><br class=""></div></div><div class="gmail_extra"><br clear="all" class=""><div class=""><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class="">. \ Philip Wadler, Professor of Theoretical Computer Science,<br class="">. /\ School of Informatics, University of Edinburgh<br class=""></div><div class="">. / \ and Senior Research Fellow, IOHK<br class=""></div><div dir="ltr" class="">.<span class="Apple-converted-space"> </span><span class=""><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank" class="">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div><br class=""><div class="gmail_quote">On 15 February 2018 at 18:35, Miëtek Bak<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:mietek@bak.io" target="_blank" class="">mietek@bak.io</a>></span><span class="Apple-converted-space"> </span>wrote:<br class=""><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;"><div class="" style="word-wrap: break-word;"><div class="">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 class=""><br class=""></div><div class="">$ git grep Dec | grep Nat</div><div class="">src/Data/Nat/Base.agda:156:_≤?<wbr class="">_ : Decidable _≤_</div><div class=""><br class=""></div><div class="">Here’s the second operation:</div><div class=""><a href="https://agda.github.io/agda-stdlib/Data.Nat.Base.html#3179" target="_blank" class="">https://agda.github.io/agda-<wbr class="">stdlib/Data.Nat.Base.html#3179</a></div><div class=""><br class=""></div><div class="">We can obtain the first operation via projection:</div><div class=""><a href="https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822" target="_blank" class="">https://agda.github.io/agda-<wbr class="">stdlib/Relation.Nullary.<wbr class="">Decidable.html#822</a></div><span class="HOEnZb"><font color="#888888" class=""><div class=""><br class=""></div><div class=""><br class=""></div><div class="">-- </div><div class="">M.</div><div class=""><br class=""></div><div class=""><br class=""></div></font></span><div class=""><br class=""><div class=""><blockquote type="cite" class=""><div class=""><div class="h5"><div class="">On 15 Feb 2018, at 20:26, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk" target="_blank" class="">wadler@inf.ed.ac.uk</a>> wrote:</div><br class="m_2941185566432368495Apple-interchange-newline"></div></div><div class=""><div class=""><div class="h5"><div dir="ltr" class=""><div class="">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 class=""><br class=""></div><div class=""> Nat -> Nat -> Bool</div><div class=""> (n : Nat) -> (m : Nat) -> Dec (m \leq n)</div><div class=""><br class=""></div><div class="">But I can't find them. Where are they and what are they called? Cheers, -- P</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class=""> Definitions about Nat</div><div class=""><br class=""></div><div class="">followed by nothing! I'm not sure why.</div><div class=""><br class=""></div><div class=""> </div><div class=""><br class=""></div><br clear="all" class=""><div class=""><div class="m_2941185566432368495gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class="">. \ Philip Wadler, Professor of Theoretical Computer Science,<br class="">. /\ School of Informatics, University of Edinburgh<br class=""></div><div class="">. / \ and Senior Research Fellow, IOHK<br class=""></div><div dir="ltr" class="">.<span class="Apple-converted-space"> </span><span class=""><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank" class="">http://homepages.inf.ed.ac.uk/<wbr class="">wadler/</a></span></div></div></div></div></div></div></div></div><span class="">The University of Edinburgh is a charitable body, registered in<br class="">Scotland, with registration number SC005336.<br class="">______________________________<wbr class="">_________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" class="">https://lists.chalmers.se/<wbr class="">mailman/listinfo/agda</a><br class=""></span></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></div>The University of Edinburgh is a charitable body, registered in<br class="">Scotland, with registration number SC005336.<br class=""></blockquote></div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">_______________________________________________</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">Agda mailing list</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="mailto:Agda@lists.chalmers.se" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">Agda@lists.chalmers.se</a><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">https://lists.chalmers.se/mailman/listinfo/agda</a></div></blockquote></div><br class=""></body></html>