<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
my coin here is to point out that it is not necessary that Coq beats Agda by far in development speed. It turns out that Coq and Agda are good at problems in their specific domains.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
for example, due to dependent pattern matching, Agda does better job at proofs requiring large chunks of inversions; in those cases, there won't even be cases generated.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
another domain in which Agda beats Coq is when complex inductive scheme is necessary. termination checker in Agda is significantly more permissive than Coq's. Agda permits mutual simultaneous induction while in Coq, proving such kind of inductive schemes requires
significant effort.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Equations shows very good potential to fill up but at this moment, Equations is still too buggy to take the role. not to mention that its lack of Emacs interaction.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Xuanrui Qi <xqi01@cs.tufts.edu><br>
<b>Sent:</b> August 3, 2019 8:03 PM<br>
<b>To:</b> Roman <effectfully@gmail.com>; Nils Anders Danielsson <nad@cse.gu.se><br>
<b>Cc:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] Using Agda in proving computer system correct</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Metaprogramming is a powerful tool and Agda/Idris style metaprogramming<br>
is enough to implement a powerful tactic system like Coq's. For this<br>
matter, Idris has the library Pruviloj (<br>
<a href="https://github.com/idris-lang/Idris-dev/tree/master/libs/pruviloj">https://github.com/idris-lang/Idris-dev/tree/master/libs/pruviloj</a>) that<br>
works basically like Mtac, although Pruviloj is still pretty limited at<br>
the current point (mainly due to the lack of active development<br>
effort). <br>
<br>
Agda's reflection mechanism is certainly strong enough for one to do<br>
the same, but I agree that the main problem here is the lack of library<br>
support. For example, AFAIK there's no mechanism in Agda that works<br>
like like elaborator reflection in Idris. Sure we can do the same<br>
things using Agda's reflection mechanism, but with a lot of extra<br>
effort.<br>
<br>
Of course, we all hope that one day we would have a programming<br>
language/proof assistant that works equally well as a dependently-typed <br>
programming language and as a (tactic-based) interactive theorem<br>
prover. We already have a lot of work towards this (e.g. Program and<br>
Equations in Coq to improve DTP, elborator reflection in Idris &<br>
reflection in Agda to support tactics-style reasoning). But what we<br>
really need now, IMO, is better tool support for all of this.<br>
<br>
-Xuanrui<br>
<br>
On Sun, 2019-08-04 at 00:11 +0300, Roman wrote:<br>
> “Using Coq is like doing brain surgery over the telephone.” – Peter<br>
> Hancock<br>
> <br>
> That was my experience with Coq as well. I think Agda's reflection<br>
> machinery (and the Idris' one for that matter) is highly<br>
> underappreciated, one can do wonders with it as it gives you first<br>
> class access to internals of Agda, including the ability to declare<br>
> functions, quote data type definitions, infer/check types and deal<br>
> with metavariables. The `TC` monad and the `macro` gadget are some<br>
> really nice and intuitive things.<br>
> <br>
> However library support is almost non-existing. There are several<br>
> libraries that deal with reflection (most notably the Ulf's<br>
> `agda-prelude`), but most of them (if not all) are either dead (i.e.<br>
> do not even build) or undocumented.<br>
> <br>
> I learned how to use reflection through trial and error and was able<br>
> to implement the equivalent of Haskell's `deriving Eq`, only for<br>
> decidable equality and with full support of<br>
> dependent/higher-order/indexed data types with implicits, instance<br>
> arguments, irrelevance and universe polymorphism [1], which showcases<br>
> that Agda's reflection is quite powerful. Others have implemented<br>
> ring<br>
> solvers [2] [3] [4], rewrite as a tactic [5], another `deriving Eq`<br>
> [6] and various other stuff. Still, library support of general<br>
> metaprogramming tools is lacking. I also wasn't satisfied by naked<br>
> and<br>
> raw De Bruijn indices that Agda uses for its internal representation<br>
> (which is very error-prone and inefficient) and not having static<br>
> information on how many times a term was quoted was quite unpleasant,<br>
> but these are technical details that are pretty solvable. Additional<br>
> features like defining data types using reflection also can be added.<br>
> <br>
> What is harder to fix is that Agda since its creation hadn't been<br>
> scaling well (I stopped paying attention a couple of years ago, so I<br>
> don't know whether things have changed or not). It was the case that<br>
> you could type check things in almost no time, then open some module<br>
> (without using anything from it) and wait for two minutes for type<br>
> checking to finish. People have reported that their projects required<br>
> a dozen or two of GBs of RAM. Even something as simple as printing a<br>
> natural number had terrible performance (I think it even was<br>
> exponential?) for many years (which has been fixed rather recently).<br>
> I<br>
> can't count for how many times I was thinking "ok, I'll wait a bit<br>
> more and kill the process". It is quite discouraging to develop<br>
> something for months just to figure out that you can only test it on<br>
> completely trivial things, because otherwise type checking won't<br>
> finish. Again, I don't know whether the situation has been improved<br>
> in<br>
> recent years.<br>
> <br>
> So for me performance was a deal breaker, not theoretical<br>
> limitations.<br>
> <br>
> Does Agda still implement call-by-name reduction strategy (as opposed<br>
> to call-by-need)?<br>
> <br>
> [1] <a href="https://github.com/effectfully/Generic/">https://github.com/effectfully/Generic/</a><br>
> [2] <a href="https://oisdk.github.io/agda-ring-solver/README.html">https://oisdk.github.io/agda-ring-solver/README.html</a><br>
> [3] <br>
> <a href="https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Solver/Ring.agda">
https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Solver/Ring.agda</a><br>
> [4] <br>
> <a href="https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda">
https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda</a><br>
> [5] <br>
> <a href="https://github.com/UlfNorell/agda-prelude/blob/master/test/Reright.agda">
https://github.com/UlfNorell/agda-prelude/blob/master/test/Reright.agda</a><br>
> [6] <br>
> <a href="https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda">
https://github.com/UlfNorell/agda-prelude/blob/master/test/DeriveEqTest.agda</a><br>
> _______________________________________________<br>
> Agda mailing list<br>
> Agda@lists.chalmers.se<br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>