<div dir="ltr">Simplified, you have the following situation:<div><br></div><div>thm : ∀ n → T n<br></div><div>thm = induction -- works</div><div><br></div><div>thm' : ∀ n → T n</div><div>thm' n = induction n -- fails</div><div><br></div><div>The induction tactic looks at the current goal type, so to understand why</div><div>the first case works but the second one fails we have to figure out what</div><div>the goal types are for the two induction calls. In the first case the goal is</div><div>clearly ∀ n → T n, which induction can handle no problem. In the other</div><div>case however the goal is not so obvious. At the very least it needs to be a</div><div>function type, so</div><div><br></div><div> induction : ∀ x → _1 n x</div><div><br></div><div>for a fresh meta _1. Note that the meta has access to both the fresh x and</div><div>the n. Now we need</div><div><br></div><div> induction n : T n</div><div><br></div><div>for the right-hand side to type correct, so</div><div><br></div><div> _1 n n == T n</div><div><br></div><div>Here we can see the problem. There are two solutions to this equation:</div><div><br></div><div> _1 := λ x y → T x</div><div> _1 := λ x y → T y</div><div class="gmail_extra"><br></div><div class="gmail_extra">so the meta will not be solved.</div><div class="gmail_extra"><br></div><div class="gmail_extra">So, why is this not a problem in the by-hand case? Because in the by-hand case</div><div class="gmail_extra">you provide the solution to the meta explicitly. If you instead try</div><div class="gmail_extra"><br></div><div class="gmail_extra"> by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)</div> by-hand n = nat-induction _ auto (λ n eq → by eq) n<div><br></div><div>you'll get the same unsolved metas.</div><div><br></div><div>/ Ulf<br><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Jan 22, 2016 at 9:57 PM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div><div>I'm a newbie to reflection in Agda and am excited to learn the new-reflection machinery. I'm starting by working through the example of induction in Tactic.Nat.<br><br> induction-example : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br> induction-example = induction<br><br></div>I tried to figure out what the induction macro is doing and came up with this:<br><br></div><div> by-hand : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br> by-hand = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto (λ n eq → by eq)<br><br></div><div>So far, great. I also tried:<br><br> unsolved-metas : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br> unsolved-metas n = induction n<br><br></div><div>but that produces 3 yellow-highlighted errors. However, there are no such problems in the "by-hand" version:<br></div><div><br> by-hand-2 : ∀ n → sum (downFrom n) * 2 ≡ n * (n + 1)<br> by-hand-2 n = nat-induction (λ n → sum (downFrom n) * 2 ≡ n * (n + 1)) auto (λ n eq → by eq) n<br></div><div><br></div><div>I'm confused. TIA for help in understanding this.<br clear="all"></div><div><div><div><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div></div></div>
<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>
<br></blockquote></div><br></div></div></div>