[Agda] using Induction.Nat
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Oct 10 09:30:57 CEST 2013
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/
More information about the Agda
mailing list