<div dir="ltr"><div>Is there a way to inspect a term in the context of a function? To find its type and the type of the variables it depends on?</div><div>It seems that all you can do is be directed to the definition of a function and nothing more.</div><div><br></div><div>Holes are very useful when you write a proof. As soon as you have written the proof , you lose all information about it except from what you can see in the text.</div><div>So here is an oxymoron. It is easier to write proofs than to understand already written ones.</div><div>I too believe that the future is the use of interactive tools to inspect the code.</div><div><br></div><div>As far as replacing hand written proofs all together , I am not so sure it is possible. I hope that one day we get there , though.<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Sat, Nov 17, 2018 at 8:14 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Sat, 2018-11-17 at 16:54 +0000, Peter Hancock wrote:<br>
> On 17/11/2018 15:53, Martin Escardo wrote:<br>
> > If you want mathematicians to use proof assistants, you have to<br>
> > implement the notations they use, not the notations that computer<br>
> > scientists / engineers find convenient to write computer programs.<br>
> > Martin<br>
> <br>
> You might as well say that if you want mathematicians to use <br>
> type-setting software you have to implement the notations they use.<br>
> The mathematicians I know seem to find their way pretty well around LaTeX, etc,<br>
> for all its barbarity. <br>
> <br>
> Perhaps one can think of mathematical notation as a matter of DSLs.<br>
> LaTeX is full of DSL-like apparatus for things like category theory diagrams, etc.<br>
> I think the support in Agda for equational reasoning might be<br>
> a nice example of a DSL.<br>
> <br>
> Is there a general definition of coercion?  Is there a connection with identity types? <br>
> <br>
> [..]<br>
<br>
Coercion has not sense in general. <br>
But mathematicians (S.Lang and Van der Waerden, and many others) write<br>
that a group homomorphism is a map f that satisfies<br>
the equality                            <br>
                               f(xy) = f(x)f(y),<br>
<br>
that a ring homomorphism needs to satisfy<br>
<br>
                               f(x+y) = f(x) + f(y),<br>
and so on.<br>
These books write so, because this way it is easier to explain and to<br>
understand. This has been tested by thousands of professors and millions<br>
of students.<br>
<br>
Generally, compilers are forced to follow science (mathematics). <br>
<br>
* For example, in early days programs used numbers instead of names. <br>
Then they have improved.<br>
* They used different functions to add polynomials over integers, <br>
to add polynomials over rationals, over polynomial, and so on. <br>
Then, they have improved, and introduced generic programming -- this<br>
follows mathematics.<br>
* In mathematics, domains depend on a value, and this value can be<br>
computed dynamically, and a function can return a domain.<br>
Compilers could not handle this.<br>
But they have improved, and now they can.  <br>
<br>
* Similar it is (or will be) with implicit conversion.<br>
<br>
Science has more sense than programming, science is wiser than a<br>
technology, it is fundamental. And programming has to follow science.   <br>
<br>
Regards,<br>
<br>
------<br>
Sergei<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>