<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><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><br class=""></div><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);" class="">_≤ᵇ_</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);" class="">_≤ᵇ_ in one line.</span></div><div><br class=""></div><div><div><span class="Apple-tab-span" style="white-space:pre"> </span>open import Data.Bool using (Bool; T)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>open import Data.Nat using (ℕ; _≤_; _≤?_)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>open import Relation.Nullary using (Dec)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>_≤ᵇ_ : ℕ → ℕ → Bool</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>m ≤ᵇ n = ⌊ m ≤? n ⌋</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤→≤ᵇ p = fromWitness p</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤ᵇ→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ n) → m ≤ n</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤ᵇ→≤ p = toWitness p</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>m ≤?′ n = m ≤? n</div><div><br class=""></div><div>Alternative type notation using synonyms supplied by the library:</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤→≤ᵇ′ : ∀ {m n : ℕ} → m ≤ n → True (m ≤? n)</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤→≤ᵇ′ p = fromWitness p</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤ᵇ→≤′ : ∀ {m n : ℕ} → True (m ≤? n) → m ≤ n</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>≤ᵇ→≤′ p = toWitness p</div><div><br class=""></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>_≤?″_ : Decidable _≤_</div><div><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 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" class="">_≤?′_ 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=""><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 dir="ltr" class=""><<a href="mailto:mietek@bak.io" target="_blank" class="">mietek@bak.io</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word" class=""><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=""><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=""></body></html>