# [Agda] using Induction.Nat

Andreas Abel andreas.abel at ifi.lmu.de
Tue Oct 8 05:10:58 CEST 2013

```Using Data.Bin was also my hunch.  Here is a partial solution to your
problem:

open import Function
open import Data.Bool
open import Data.List
open import Data.Nat
open import Data.Fin using (zero; suc)
open import Data.Bin using (Bin⁺; 0#; _1#; fromℕ)

open import Relation.Binary.PropositionalEquality

-- Binary exponentiation

module Power {A : Set} (_•_ : A → A → A) (x : A) where

binPower : Bin⁺ → A
binPower []       = x
binPower (b ∷ bs) = case b of
λ { zero           → r²
; (suc zero)     → x • r²
; (suc (suc ()))
}
where
r  = binPower bs
r² = r • r

posPower : (n : ℕ) → n > 0 → A
posPower 0 ()
posPower (suc n) _ with fromℕ (1 + n)
... | bs 1# = binPower bs
... | 0#    = x  -- this case is impossible; showing this is extra
work...

On 2013-10-08 10:13, Daniel Peebles wrote:
> 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.
>
> 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
> .
>
> On Mon, Oct 7, 2013 at 10:30 AM, Sergei Meshveliani
> <mechvel at botik.ru> wrote:
>
>> People,
>> I have this program for powering  x^(n+1)
>> for  x : Carrier of a Semigroup:
>>
>>  half : ℕ → ℕ
>>  half = ⌊_/2⌋
>>
>>  powerTo-suc : C → (e : ℕ) → C     -- x^(e+1)
>>  powerTo-suc x 0       = x
>>  powerTo-suc x (suc e) = case  even? e  of
>>                                         { (yes _) → p ∙ p
>>                                         ; _       → x ∙ (p ∙ p) }
>>                                         where
>>                                         h = half e
>>                                         p = powerTo-suc x h
>>
>> The checker cannot prove its termination.
>> I can help this proof by adding the counter argument  cnt  for the
>> number of the  `half'  calls.
>> But this complicates various further proofs for  powerTo-suc.
>>
>> So, I think of trying _inductive families_ for  ℕ  provided by
>> Induction, Induction.Nat ... in the standard library
>> (the question of whether this will make further proofs easier is
>> open
>> for me).
>>
>> But it is difficult to understand the idea, some introductory text
>> is
>> needed, with a couple of simple examples.
>>
>> Induction.Nat  gives an example for  `half'. It is too simple,
>> because
>> it is for the step from  n  to  suc n.
>> And in my example, it is the step from  half (suc e)  to  suc e,
>> assuming that we have a proof for
>>                                   half (suc e) < suc e.
>>
>> Probably  cRec  needs here to be given something additional, maybe
>> some
>> builder needs to be defined.
>>
>> May be you can demonstrate this Agda induction right on this example
>> of
>> powerTo-suc ?
>>
>> Thank you in advance for explanation.
>>
>> ------
>> Sergei
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda 
>
>
>
> ------
>  https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

--
Andreas Abel  <><     Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-------------- next part --------------
module BinPowerStdLib where

open import Function
open import Data.Bool
open import Data.List
open import Data.Nat
open import Data.Fin using (zero; suc)
open import Data.Bin using (Bin⁺; 0#; _1#; fromℕ)

open import Relation.Binary.PropositionalEquality

-- Binary exponentiation

module Power {A : Set} (_•_ : A → A → A) (x : A) where

binPower : Bin⁺ → A
binPower []       = x
binPower (b ∷ bs) = case b of
λ { zero           → r²
; (suc zero)     → x • r²
; (suc (suc ()))
}
where
r  = binPower bs
r² = r • r

posPower : (n : ℕ) → n > 0 → A
posPower 0 ()
posPower (suc n) _ with fromℕ (1 + n)
... | bs 1# = binPower bs
... | 0#    = x  -- this case is impossible; showing this is extra work...
```