<div dir="ltr"><div>The improved reflection, which you can read about here:</div><div><br></div><a href="http://agda.readthedocs.org/en/latest/language/reflection.html">http://agda.readthedocs.org/en/latest/language/reflection.html</a><br><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 11, 2016 at 10:08 PM, Bradley Hardy <span dir="ltr">&lt;<a href="mailto:bch29@cam.ac.uk" target="_blank">bch29@cam.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">By the new tactic language, do you mean the improved reflection capabilities in 2.5, or has something more Coq-like recently been implemented?<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
&gt; On 11 Apr 2016, at 20:14, Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt; wrote:<br>
&gt;<br>
&gt; Since (f n) does not reduce to 0 (both equations are more specific), you have to split on n.<br>
&gt;<br>
&gt; You could implement a tactic using Agda&#39;s new tactic language that does such routine jobs for you.<br>
&gt;<br>
&gt; On 11.04.2016 18:28, Sergei Meshveliani wrote:<br>
&gt;&gt; Hello, All.<br>
&gt;&gt;<br>
&gt;&gt; I have the following question.<br>
&gt;&gt; The program<br>
&gt;&gt;<br>
&gt;&gt; -------------------------------------------------<br>
&gt;&gt; open import Relation.Binary.PropositionalEquality<br>
&gt;&gt; open import Data.Nat<br>
&gt;&gt;<br>
&gt;&gt; f : ℕ → ℕ<br>
&gt;&gt; f 0       = 0<br>
&gt;&gt; f (suc _) = 0<br>
&gt;&gt;<br>
&gt;&gt; theorem :  ∀ n → f n ≡ 0<br>
&gt;&gt; theorem _ =  refl<br>
&gt;&gt; --------------------------------------------------<br>
&gt;&gt;<br>
&gt;&gt; is not type-checked, because Agda expects the two proofs to be given.<br>
&gt;&gt; One for the case 0, another for the case (suc _).<br>
&gt;&gt; Both proofs can be set `refl&#39;, that is -- by normalization.<br>
&gt;&gt;<br>
&gt;&gt; Could the type checker check the proof by a single `refl&#39;, by<br>
&gt;&gt; normalizing each branch?<br>
&gt;&gt; (this will simplify many proofs).<br>
&gt;&gt;<br>
&gt;&gt; Thanks,<br>
&gt;&gt;<br>
&gt;&gt; ------<br>
&gt;&gt; Sergei<br>
&gt;&gt;<br>
&gt;&gt; _______________________________________________<br>
&gt;&gt; Agda mailing list<br>
&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
&gt; --<br>
&gt; Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
&gt;<br>
&gt; Department of Computer Science and Engineering<br>
&gt; Chalmers and Gothenburg University, Sweden<br>
&gt;<br>
&gt; <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
&gt; <a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
</div></div></blockquote></div><br></div>