<div dir="ltr"><div dir="ltr">Hi Philip,</div><div> I think the key point is that irrelevant arguments still have to be valid members of the type. It's not that Agda doesn't require a valid value for an irrelevant argument, it's that Agda doesn't care which particular valid value you provide. So in your example "proof", you would not be able to divide by "a - b" as you would not have a proof that it is non-zero. However if in different circumstances you had <i>two</i> proofs that "a - b" is non-zero then the irrelevancy would ensure that Agda wouldn't care which one you used. In summary, using irrelevant arguments does not allow us to prove 1 == 2.</div><div><br></div><div>There's also been some discussion on the type of irrelevance we should be aiming for on this pull request that you might find interesting: <a href="https://github.com/agda/agda-stdlib/pull/1538">https://github.com/agda/agda-stdlib/pull/1538</a></div><div>Cheers,</div><div>Matthew</div><div><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jul 7, 2021 at 2:22 AM Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">There is a standard proof that 1 = 2. You are probably familiar with it; if not, see below. You write:<div><br><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Agda doesn't consider irrelevant arguments when proving propositional equality. Therefore to prove </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m / n </code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">and </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x / y</code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> are propositionally equal will only require that we prove </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m</code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> equals </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x</code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> and </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">n</code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> equals </span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">y</code><span style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> and will not require us to explicitly prove that the result doesn't depend on the proofs of non-zeroness.</span></blockquote><div style="color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"> </div><div>Does making the proof of nonzero divisor an irrelevant argument open up the possibility to prove 1 = 2? Go well, -- P</div><div><br></div><div><a href="https://www.quickanddirtytips.com/education/math/how-to-prove-that-1-2" target="_blank">https://www.quickanddirtytips.com/education/math/how-to-prove-that-1-2</a><br></div><div><br></div><div><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-family:Lato,sans-serif;font-size:16px;color:rgb(102,117,135)">Here's how it works:</p><ul style="box-sizing:border-box;list-style-position:outside;margin:0px 0px 1.25rem 1.1rem;padding:0px;font-size:16px;line-height:1.6;font-family:Lato,sans-serif;color:rgb(102,117,135)"><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Assume that we have two variables <em style="box-sizing:border-box;line-height:inherit">a</em> and <em style="box-sizing:border-box;line-height:inherit">b</em>, and that: <strong style="box-sizing:border-box;line-height:inherit"><em style="box-sizing:border-box;line-height:inherit">a</em> = <em style="box-sizing:border-box;line-height:inherit">b</em></strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Multiply both sides by <em style="box-sizing:border-box;line-height:inherit">a</em> to get: <strong style="box-sizing:border-box;line-height:inherit"><em style="box-sizing:border-box;line-height:inherit">a</em><span style="box-sizing:border-box;font-size:12px;line-height:0;vertical-align:baseline">2</span> = </strong><em style="box-sizing:border-box;line-height:inherit"><strong style="box-sizing:border-box;line-height:inherit">ab</strong></em></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Subtract <em style="box-sizing:border-box;line-height:inherit">b</em><span style="box-sizing:border-box;font-size:12px;line-height:0;vertical-align:baseline">2</span> from both sides to get: <strong style="box-sizing:border-box;line-height:inherit"><em style="box-sizing:border-box;line-height:inherit">a</em><span style="box-sizing:border-box;font-size:12px;line-height:0;vertical-align:baseline">2</span> - <em style="box-sizing:border-box;line-height:inherit">b</em><span style="box-sizing:border-box;font-size:12px;line-height:0;vertical-align:baseline">2</span> = <em style="box-sizing:border-box;line-height:inherit">ab</em> - <em style="box-sizing:border-box;line-height:inherit">b</em><span style="box-sizing:border-box;font-size:12px;line-height:0;vertical-align:baseline">2</span></strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">This is the tricky part: Factor the left side (using FOIL from algebra) to get (<em style="box-sizing:border-box;line-height:inherit">a</em> + <em style="box-sizing:border-box;line-height:inherit">b</em>)(<em style="box-sizing:border-box;line-height:inherit">a</em> - <em style="box-sizing:border-box;line-height:inherit">b</em>) and factor out <em style="box-sizing:border-box;line-height:inherit">b</em> from the right side to get <em style="box-sizing:border-box;line-height:inherit">b</em>(<em style="box-sizing:border-box;line-height:inherit">a</em> - <em style="box-sizing:border-box;line-height:inherit">b</em>). If you're not sure how FOIL or factoring works, don't worry—you can check that this all works by multiplying everything out to see that it matches. The end result is that our equation has become: <strong style="box-sizing:border-box;line-height:inherit">(<em style="box-sizing:border-box;line-height:inherit">a</em> + <em style="box-sizing:border-box;line-height:inherit">b</em>)(<em style="box-sizing:border-box;line-height:inherit">a</em> - <em style="box-sizing:border-box;line-height:inherit">b</em>) = <em style="box-sizing:border-box;line-height:inherit">b</em>(<em style="box-sizing:border-box;line-height:inherit">a</em> - <em style="box-sizing:border-box;line-height:inherit">b</em>)</strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Since (<em style="box-sizing:border-box;line-height:inherit">a</em> - <em style="box-sizing:border-box;line-height:inherit">b</em>) appears on both sides, we can cancel it to get: <strong style="box-sizing:border-box;line-height:inherit"><em style="box-sizing:border-box;line-height:inherit">a</em> + <em style="box-sizing:border-box;line-height:inherit">b</em> = <em style="box-sizing:border-box;line-height:inherit">b</em></strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Since <em style="box-sizing:border-box;line-height:inherit">a</em> = <em style="box-sizing:border-box;line-height:inherit">b</em> (that's the assumption we started with), we can substitute <em style="box-sizing:border-box;line-height:inherit">b</em> in for <em style="box-sizing:border-box;line-height:inherit">a</em> to get: <strong style="box-sizing:border-box;line-height:inherit"><em style="box-sizing:border-box;line-height:inherit">b</em> + <em style="box-sizing:border-box;line-height:inherit">b</em> = <em style="box-sizing:border-box;line-height:inherit">b</em></strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Combining the two terms on the left gives us: <strong style="box-sizing:border-box;line-height:inherit">2<em style="box-sizing:border-box;line-height:inherit">b</em> = <em style="box-sizing:border-box;line-height:inherit">b</em></strong></p></li><li style="box-sizing:border-box;margin:0px;padding:0px;font-size:1rem;line-height:1.6"><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-size:1rem">Since <em style="box-sizing:border-box;line-height:inherit">b</em> appears on both sides, we can divide through by <em style="box-sizing:border-box;line-height:inherit">b</em> to get: <strong style="box-sizing:border-box;line-height:inherit">2 = 1</strong></p></li></ul><p style="box-sizing:border-box;margin:0px 0px 1.25rem;padding:0px;line-height:1.6;font-family:Lato,sans-serif;font-size:16px;color:rgb(102,117,135)">Wait, what?! Everything we did there looked totally reasonable. How in the world did we end up proving that 2 = 1?</p><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr"><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 dir="ltr"><br></div></div></div></div></div></div></div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 6 Jul 2021 at 05:43, Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" target="_blank">matthewdaggitt@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">


<div>
<div style="background-color:rgb(255,242,230);border:2px dotted rgb(255,136,77)"><span style="font-size:12pt;font-family:sans-serif;color:black;font-weight:bold;padding:0.2em">This email was sent to you by someone outside the University.</span>
<div style="font-size:10pt;font-family:sans-serif;font-style:normal;padding:0.2em">
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.</div>
</div>
<div>
<div dir="ltr">
<p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
Dear all, <br>
To kick things off, the first RFC (request for comment) for v2.0 of the Agda standard library is about proposed changes to how numeric operations that require non-zero proofs (e.g. division) work.</p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<span style="font-weight:600">The current situation</span></p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
Currently operations such as division are defined as <a href="https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43" style="color:rgb(0,136,204);text-decoration-line:none" target="_blank">follows</a>:</p>
<div style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none">
<pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span style="color:rgb(120,93,161)">_/_</span> <span style="color:rgb(165,30,255);font-weight:700">:</span> <span style="color:rgb(164,29,92)">(</span>dividend divisor <span style="color:rgb(165,30,255);font-weight:700">:</span> ℕ<span style="color:rgb(164,29,92)">)</span> <span style="color:rgb(164,29,92)">{</span>≢0 <span style="color:rgb(165,30,255);font-weight:700">:</span> False <span style="color:rgb(164,29,92)">(</span>divisor ≟ <span style="color:rgb(0,133,178)">0</span><span style="color:rgb(164,29,92)">)}</span> <span style="color:rgb(165,30,255);font-weight:700">→</span> ℕ
</code></pre>
</div>
<p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
taking an implicit proof that the result of the decision procedure of testing whether it is zero reduces to <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">false</code>.
 This is preferable to passing a direct proof of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor
 ≢ 0</code> as it means that when <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor</code> normalises
 to something of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc n</code> then the
 type of the proof reduces to unit <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">⊤</code> which
 Agda automatically fills in. Consequently you can write <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">7
 / 3</code> or <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m /
</code><span style="color:rgb(0,0,0);font-family:"Source Code Pro",monospace;font-size:11.55px;white-space:pre-wrap">suc</span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">n</code> without
 having to explicitly construct the proof.</p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<span style="font-weight:600">The current problems</span></p>
<ol style="padding:0px;margin:0px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<li style="line-height:inherit">When the denominator is not in the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc
 _</code>, Agda can't infer the proof and therefore it must always be passed explicitly even when the proof is in scope. This leads to having to write the ugly code like the following:</li></ol>
<div style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none">
<pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span style="color:rgb(165,30,255);font-weight:700">∀</span> m n <span style="color:rgb(164,29,92)">{</span>gcd≢0 <span style="color:rgb(165,30,255);font-weight:700">:</span> NonZero <span style="color:rgb(164,29,92)">(</span>gcd m n<span style="color:rgb(164,29,92)">)}</span> <span style="color:rgb(165,30,255);font-weight:700">→</span> Coprime <span style="color:rgb(164,29,92)">((</span>m / gcd m n<span style="color:rgb(164,29,92)">)</span> <span style="color:rgb(164,29,92)">{</span>gcd≢0<span style="color:rgb(164,29,92)">})</span> <span style="color:rgb(164,29,92)">((</span>n / gcd m n<span style="color:rgb(164,29,92)">)</span> <span style="color:rgb(164,29,92)">{</span>gcd≢0<span style="color:rgb(164,29,92)">})</span>
</code></pre>
</div>
<ol start="2" style="padding:0px;margin:2px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<li style="line-height:inherit">
<p style="margin:3px 0px">When proving equalities over <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> you
 can't use <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">cong₂</code> from <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Relation.Binary.PropositionalEquality</code> directly
 as Agda requires that you explicitly prove the proofs of non-zeroness do not affect the result. This makes it very finicky to use equational reasoning.</p>
</li><li style="line-height:inherit">
<p style="margin:3px 0px">The use of the decision procedure <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_≟_</code> means
 that the definition must depend on <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Properties</code> where <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_≟_</code> lives.
 This means that a) type-checking anything involving <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> requires
 type-checking a much larger proportion of the library that one would expect and b) <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> can't
 live in <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Base</code>.</p>
</li><li style="line-height:inherit">
<p style="margin:3px 0px">Constructing a proof of the type <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">False
 (divisor ≟ 0)</code> is much trickier than a proof of <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor
 ≢ 0</code>and requires extra imports from <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Relation.Nullary</code>.</p>
</li></ol>
<p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<span style="font-weight:600">Proposed solution</span></p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
We propose to take a leaf out of Ulf Norell's Prelude library and instead pass the proofs as <em>irrelevant</em>, <em>instance</em> arguments that use the new <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicates
 introduced in v1.5:</p>
<div style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none">
<pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span style="color:rgb(120,93,161)">_/_</span> <span style="color:rgb(165,30,255);font-weight:700">:</span> <span style="color:rgb(164,29,92)">(</span>dividend divisor <span style="color:rgb(165,30,255);font-weight:700">:</span> ℕ<span style="color:rgb(164,29,92)">)</span> <span style="color:rgb(164,29,92)">{{</span><span style="color:rgb(165,30,255);font-weight:700">.</span><span style="color:rgb(164,29,92)">(</span>NonZero divisor<span style="color:rgb(164,29,92)">)}}</span> <span style="color:rgb(165,30,255);font-weight:700">→</span> ℕ
</code></pre>
</div>
<p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
which preserves the ability to not provide the proofs for divisors of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc
 _</code> and fixes the problems listed above as follows:</p>
<ol style="padding:0px;margin:0px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<li style="line-height:inherit">Agda automatically fills in instance arguments if they are in scope, therefore removing the need to supply them to every place in the expression where they can't be inferred. For example we would then be able to write the much
 nicer:</li></ol>
<div style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none">
<pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span style="color:rgb(165,30,255);font-weight:700">∀</span> m n <span style="color:rgb(164,29,92)">{{</span>NonZero <span style="color:rgb(164,29,92)">(</span>gcd m n<span style="color:rgb(164,29,92)">)}}</span> <span style="color:rgb(165,30,255);font-weight:700">→</span> Coprime <span style="color:rgb(164,29,92)">(</span>m / gcd m n<span style="color:rgb(164,29,92)">)</span> <span style="color:rgb(164,29,92)">(</span>n / gcd m n<span style="color:rgb(164,29,92)">)</span>
</code></pre>
</div>
<ol start="2" style="padding:0px;margin:2px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<li style="line-height:inherit">
<p style="margin:3px 0px">Agda doesn't consider irrelevant arguments when proving propositional equality. Therefore to prove <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m
 / n</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x / y</code> are propositionally
 equal will only require that we prove <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m</code> equals <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">n</code> equals <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">y</code> and
 will not require us to explicitly prove that the result doesn't depend on the proofs of non-zeroness.</p>
</li><li style="line-height:inherit">
<p style="margin:3px 0px">The <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicate
 is much more lightweight than the decidability proof and lives in <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Base</code> rather
 than <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Properties</code>.</p>
</li><li style="line-height:inherit">
<p style="margin:3px 0px">The <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicate
 comes with nice constructors <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">nonZero-<</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">nonZero-≢</code> that
 makes constructing such proofs much easier.</p>
</li></ol>
<p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
This has an additional advantage in that for certain operations that always result in a non-zero result, e.g. factorial, it will be possible to declare a proof of the non-zeroness as an instance and you will never have to explicitly pass a proof.</p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<span style="font-weight:600">Backwards incompatibilities</span></p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
In cases where the proof is already automatically inferred nothing will need to change. In places where the proof has to be passed explicitly, then the type of the proof will need to change and will need to be passed using instance brackets <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">{{_}}</code> rather
 than implict brackets <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">{_}</code>. As mentioned
 above, <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> comes with constructors
 so constructing the new proofs should be much easier.</p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
<span style="font-weight:600">Feedback</span></p>
<p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">
Any feedback would be greatly appreciated! Please feel free to reply in one of the following issues:<br>
<a href="https://github.com/agda/agda-stdlib/issues/921" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/921" style="color:rgb(0,136,204);text-decoration-line:none" target="_blank">https://github.com/agda/agda-stdlib/issues/921</a><br>
<a href="https://github.com/agda/agda-stdlib/issues/1170" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/1170" style="color:rgb(0,136,204);text-decoration-line:none" target="_blank">https://github.com/agda/agda-stdlib/issues/1170</a><br>
<a href="https://github.com/agda/agda-stdlib/issues/1408" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/1408" style="color:rgb(0,136,204);text-decoration-line:none" target="_blank">https://github.com/agda/agda-stdlib/issues/1408<br>
</a></p>
</div>
</div>
</div>

_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
</blockquote></div></div>