[Agda] using Induction.Nat

[Andreas Abel]

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
> at http://www.cse.chalmers.se/~nad/listings/lib/Data.Digit.html#2612
> [2].
>
> 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 [1]
>
>
>
> Links:
> ------
> [1] https://lists.chalmers.se/mailman/listinfo/agda
> [2] http://www.cse.chalmers.se/~nad/listings/lib/Data.Digit.html#2612
>
> _______________________________________________
> 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...