<div><div dir="auto"><div dir="auto">Hi everyone,</div><div dir="auto"><br></div><div dir="auto">  Interesting discussion! I don’t think you need to be a brain surgeon to program in Coq (I wouldn’t trust an arbitrary Coq user with my brain in any case :), but it’s true it can easily be misused (the video-game effect of the tactic mode in particular can be pretty bad). In my opinion however what is true for Coq is also true for Agda, type theory cannot scale up to large verification problems without good abstractions: whether they are robust tactic languages avoiding the nitty-gritty of proof terms (maintaining an Agda development written without abstractions by someone else is not more fun or easy than a fragile Coq proof script), or using the highly-expressive type systems we have to express ideas concisely and efficiently. I think these two can work hand-in-hand actually: an example being the treatment of views and the reflect predicate of ssreflect in Coq for example, which leverages dependent elimination and computation and integrates it with a tactic language construct to seamlessly move between different specifications about a given function. Likewise, the rewrite construct of Agda, provides a higher-level ‘tactic’ during programming, inferring a rewriting predicate and applying it using the eliminator of equality, just like the rewrite tactic of Coq does.</div></div><div dir="auto"><br></div><div dir="auto">  Abstractions can be costly to compilers but I would guess the main differences in performance between Agda on one side and Coq and Lean on the other side would rather be in the conversion / reduction algorithms and in unification, where they are mostly incomparable right now, although getting closer in some respects (e.g. the use of abstract to block reductions).</div><div dir="auto"><br></div><div dir="auto"><div><div class="gmail_quote"></div></div></div></div><div><div><div><div dir="ltr" class="gmail_attr">Le lun. 5 août 2019 à 11:17, Jacques Carette <<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>> a écrit :<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I can't help but comment on a mis-perception in this particular message <br>
earlier in this thread:<br>
<br>
On 2019-08-03 4:47 p.m., Xuanrui Qi wrote:<br>
> Also, it's widely agreed that tactic-based proofs and backwards<br>
> reasoning are definitely more suited for large-scale proof efforts. As<br>
> a result, most if not all large mechanized computer system<br>
> verifications proof efforts use proof assistants with LCF-style tactic<br>
> language (CompCert and CertiKOS in Coq, seL4 in Isabelle, CakeML in<br>
> HOL4, etc.)<br>
<br>
It used to be "widely agreed" that dependent types were too hard for <br>
doing anything of any size - this has been thoroughly debunked. Same <br>
with the meta-theory of binders. Lots of hard work had to be done to <br>
figure out 'how to do it', but out of that hard work techniques were <br>
distilled so that it no longer is so hard.<br>
<br>
Tactics originate from the LCF view of proofs as abstract objects that <br>
you cannot reach in to; they are 'proof transformers'. And they are <br>
absolutely necessary if your proofs are in Prop. And having proofs in <br>
Prop itself originates from classical mathematical ideas that "proofs <br>
have no content" and the "widely agreed" (!) idea that carrying <br>
irrelevant proofs around will produce a system that is much too slow.</blockquote><div dir="auto"><br></div></div></div></div><div><div><div><div dir="auto">For what it’s worth, despite having proofs in Prop in Coq (or Lean), they are still around in memory (albeit blocked by Qeds usually, and sometimes lazily loaded from disk). So the view of Prop as a bracket of Type, reconciling with the Agda/HoTT-style view of proofs as by default relevant (and maybe just squashed/truncated explicitely when irrelevance/erasure matters or impredicativity is used) would not change much w.r.t. the space efficiency story — a definionally proof-irrelevant sort (OTT’s Prop, SProp) does change the time-efficiency story significantly however, as terms standing for proof terms (in SProp) must never be converted in this case. Also, Agda uses call-by-name or call-by-need reduction (Coq uses a variant of call-by-need in its default conversion algorithm), so unfolding of proofs usually happens only if necessary and they shouldn’t differ much (the devil’s in the details of course).</div></div></div></div><div dir="auto"><br></div><div><div><div><div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
But, well, Agda's notion of proof, as embedded as specific terms in Set, <br>
is not proof-irrelevant. And, lo and behold, dependent pattern-matching <br>
makes that extremely useful! All of a sudden, what used to be <br>
complicated tactics are now just normal programs. This is a major <br>
advance. (See <a href="http://r6.ca/blog/20171008T222703Z.html" rel="noreferrer" target="_blank">http://r6.ca/blog/20171008T222703Z.html</a> for reflections of <br>
a Coq expert 'discovering' this.)<br>
<br>
Having said that, there does remain issues worthy of further research IMHO:<br>
1. ssreflect-style reflection, or the "local approach" to reflection. <br>
There really are times when a domain has decision procedures based on <br>
the *syntax* of its terms based on some (usually quotiented) <br>
term-algebra; think polynomials over Nat and their normal form as a <br>
decision procedure for semirings [i.e. pure arithmetic induces proofs <br>
via an interpretation]. Calling these 'tactics' obscures much of the <br>
reason for the power of the method.<br>
2. global style reflection (see the work of William M. Farmer). For when <br>
you want to embed all of your language. This is what MetaCoq is trying too.<br>
3. "sufficient lazyness" -- i.e. figuring out when both values (which <br>
can be proofs) and control paths are no longer needed, and just erasing <br>
them. [See <a href="https://arxiv.org/abs/1907.13227" rel="noreferrer" target="_blank">https://arxiv.org/abs/1907.13227</a> but also <br>
<a href="http://sci-hub.tw/10.1145/115866.115890" rel="noreferrer" target="_blank">http://sci-hub.tw/10.1145/115866.115890</a> which links back to ideas of #2 <br>
for really interesting ideas from generic PL in that direction]<br>
4. more automation. Yes, it is painful to do a case-split into > 100 <br>
cases [yes, I have such code], where only 4 require a non-trivial <br>
sub-proof [and even then], and the rest of the ~100 cases are just <br>
'refl'. Or maybe the answer isn't automation, it's some eta-like rule <br>
for inductive types -- who knows.</blockquote><div dir="auto"><br></div></div></div></div></div></div></div><div><div><div><div><div><div class="gmail_quote"><div dir="auto">I think the view pattern can help here, using dependent elimination to let the typechecker know only a handful of cases are interesting and the rest are treated the same, e.g. using predicates of the form:</div><div dir="auto"><br></div><div dir="auto">data MyCases : MyType -> Set where</div><div dir="auto">  interesting a b : MyCases (foo a b)</div><div dir="auto">  interesting2 : MyCases bar</div><div dir="auto">  notsointeresting m : ~ (is_foo_or_bar m) -> MyCases m.</div><div dir="auto"><br></div><div dir="auto">Then:</div><div dir="auto"><br></div><div dir="auto">mycases m : MyCases m</div><div dir="auto">mycases (foo a b) = ...</div><div dir="auto">mycases bar = ...</div><div dir="auto">mycases other = notsointeresting m refl</div></div></div></div></div></div><div><div class="gmail_quote"><div dir="auto"><br></div><div dir="auto">You’ll do a full case split one time only this way.</div><div dir="auto">Again it’s a matter of using the right tool for the job, and type theory provides plenty of options!</div><div dir="auto">I guess Coq gives more options to brute force such proofs using the tactic language, but in the long term such methods don’t scale well.</div><div dir="auto"><br></div><div dir="auto">Best,</div><div dir="auto">— Matthieu</div></div></div></div>