<div dir="ltr">My first inclination for your repeated halving is to switch to a representation where your work is structural Data.Bin comes to mind, and you could write your exponentiation algorithm on Bin values, then convert back and forth on the way in and out as a wrapper. It'd probably be a lot more efficient, too.<div>
<br></div><div>Alternately, since the conversion to Data.Bin is doing well-founded recursion of the sort you need, you could use it as an example. The real work is done in Data.Digits, and you can find more at <a href="http://www.cse.chalmers.se/~nad/listings/lib/Data.Digit.html#2612">http://www.cse.chalmers.se/~nad/listings/lib/Data.Digit.html#2612</a>.</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Oct 7, 2013 at 10:30 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I have this program for powering x^(n+1)<br>
for x : Carrier of a Semigroup:<br>
<br>
half : ℕ → ℕ<br>
half = ⌊_/2⌋<br>
<br>
powerTo-suc : C → (e : ℕ) → C -- x^(e+1)<br>
powerTo-suc x 0 = x<br>
powerTo-suc x (suc e) = case even? e of \<br>
{ (yes _) → p ∙ p<br>
; _ → x ∙ (p ∙ p) }<br>
where<br>
h = half e<br>
p = powerTo-suc x h<br>
<br>
The checker cannot prove its termination.<br>
I can help this proof by adding the counter argument cnt for the<br>
number of the `half' calls.<br>
But this complicates various further proofs for powerTo-suc.<br>
<br>
So, I think of trying _inductive families_ for ℕ provided by<br>
Induction, Induction.Nat ... in the standard library<br>
(the question of whether this will make further proofs easier is open<br>
for me).<br>
<br>
But it is difficult to understand the idea, some introductory text is<br>
needed, with a couple of simple examples.<br>
<br>
Induction.Nat gives an example for `half'. It is too simple, because<br>
it is for the step from n to suc n.<br>
And in my example, it is the step from half (suc e) to suc e,<br>
assuming that we have a proof for<br>
half (suc e) < suc e.<br>
<br>
Probably cRec needs here to be given something additional, maybe some<br>
builder needs to be defined.<br>
<br>
May be you can demonstrate this Agda induction right on this example of<br>
powerTo-suc ?<br>
<br>
Thank you in advance for explanation.<br>
<br>
------<br>
Sergei<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>