Sergei Meshveliani | 7 Oct 16:30 2013
Picon

using Induction.Nat

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
(Continue reading)

Daniel Peebles | 8 Oct 03:13 2013
Picon

Re: using Induction.Nat

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.


On Mon, Oct 7, 2013 at 10:30 AM, Sergei Meshveliani <mechvel-p4AAo9Fem04@public.gmane.org> 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-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andreas Abel | 8 Oct 05:10 2013
Picon

Re: using Induction.Nat

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@...> 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@...
>> 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@...
> 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/
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...
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani | 9 Oct 16:17 2013
Picon

Re: using Induction.Nat

On Tue, 2013-10-08 at 12:10 +0900, Andreas Abel wrote:
> Using Data.Bin was also my hunch.  Here is a partial solution to your 
> problem:
> 
> [..]

> 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

Indeed, using the Bin⁺ argument simplifies the proofs greatly.
Because  (2 *)  converts to  (bit ::),  and termination becomes given
for free.  
So, my introduction to inductive types is delayed to the first future
unlucky case.

Thanks to people!

------
Sergei
Andreas Abel | 10 Oct 09:30 2013
Picon

Re: using Induction.Nat

The hard work to show termination is done in Data.Digit, in showing 
that the function that converts a unary into a binary number is 
terminating.  But it seems more principled to do the work there instead 
of the binary exponentiation function, which is best understood as 
structural recursion over binary numbers.

Cheers,
Andreas

On 2013-10-09 23:17, Sergei Meshveliani wrote:
> On Tue, 2013-10-08 at 12:10 +0900, Andreas Abel wrote:
>> Using Data.Bin was also my hunch.  Here is a partial solution to 
>> your
>> problem:
>>
>> [..]
>
>> 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
>
>
> Indeed, using the Bin⁺ argument simplifies the proofs greatly.
> Because  (2 *)  converts to  (bit ::),  and termination becomes given
> for free.
> So, my introduction to inductive types is delayed to the first future
> unlucky case.
>
> Thanks to people!
>
> ------
> Sergei

--

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

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

Gmane