<div dir="ltr"><div>I wonder what is more confusing : Using "+" and "*_i" to denote addition for Nat and addition for Integers <br></div><div>or "+" and "+" to denote addition for both Nat and Integers.</div><div><br></div><div>Using correct symbols that do not confuse is a responsibility that cannot be avoided even without coercions.</div><div><br></div><div>If we are able to inspect terms of a proof , any confusion is removed entirely, while at the same time simplifying our proof.</div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Nov 19, 2018 at 6:45 AM Peter Hancock <<a href="mailto:hancock@fastmail.fm">hancock@fastmail.fm</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 18/11/2018 21:32, Jason -Zhong Sheng- Hu wrote:<br>
> If we can have a hierarchy of views, which allows us to zoom in and<br>
> out of mathematics/proofs/programs, I think coersion can have way<br>
> more value.<br>
<br>
Someone who's opinion is worth having about the presentation of<br>
mathematical material is Lamport.  I am thinking about his<br>
specification language TLA+, and  its proof system TLP (I think).<br>
<br>
These formalisms were designed to be used by engineers, who I suppose<br>
are mathematicians of some kind. Stylistically, they resemble COBOL,<br>
with lots of upper-case keywords, etc.  IMHO, they are readable, largely<br>
because notational fuss is kept to a minimum.  Things are designed to be<br>
emailable in ASCII. <br>
<br>
Most interesting is that TLP is designed for writing informal proofs.<br>
At any point, you can put in an informal "handwave" (a bit like a hole). <br>
A "folding" metaphor is used to browse TLP proofs. You can choose to<br>
hide uninteresting portions of a proof, and drill down to <br>
particular steps in full gory detail.  Lamport says one should<br>
write a proof in small enough steps that everything is completely obvious,<br>
then provide one more level of formal proof.<br>
<br>
I presume coercions are injective functions that resolve type-clashes between <br>
things like natural numbers and signed integers, or fractions, etc.<br>
There are times when we want to see these things, and there are times<br>
when we would like them to be hidden. <br>
Could one have a "pedantry" knob when editing or browsing agda? <br>
At pedantry level 11 absolutely nothing would be hidden....<br>
<br>
Sergie's gave some examples of using "+", "*" etc to mean different<br>
operations in different rings.  Is this an example of coercion?<br>
I'm inclined to call it overloading.  (Which also helps to dispense with <br>
pedantic crap.) <br>
<br>
<br>
<br>
_______________________________________________<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>