Issue 777 [Re: [Agda] Semigroup.Carrier in 2.3.2]

[Dominique Devriese]

For those who are interested, I have posted a detailed analysis of
Serge's examples in issue 777. I am working on a patch that provides a
partial solution.

Dominique

2012/12/31 Andreas Abel <andreas.abel at ifi.lmu.de>:
> Your example below works under Agda 2.3.2 if we bring H into scope with {H =
> H}:
>
>   powerToPositive {H = H} x e e>0 =  pow e e e>0
>        where
>        open Semigroup {{...}}
>        pow : Nat -> (e : Nat) -> e > 0 -> Carrier
>
> However, this should not be necessary, I filed this as bug 777.
>
> Cheers,
> Andreas
>
> On 30.12.12 5:14 PM, Serge D. Mechveliani wrote:
>>
>> On Tue, Dec 25, 2012 at 09:26:00AM +0100, Andreas Abel wrote:
>>>
>>> Instance search is experimental, so it is likely not all things work
>>> the same.
>>>
>>> Could you please attach a test case I can try directly without have
>>> to do imports, renaming etc.?
>>
>>
>>
>> See the attachment to this letter:   Main.agda.zip.
>>
>> The first variant there works under  Agda-2.3.0.1
>> but not under                        Agda-2.3.2.
>>
>> The second variant is commented out,
>> it "fixes" the code for 2.3.2 by making the argument explicit.
>>
>> Which Agda version is more correct at this point?
>>
>> Regards,
>>
>> ------
>> Sergei
>>
>>
>>> On 23.12.12 12:09 PM, Serge D. Mechveliani wrote:
>>>>
>>>> People,
>>>> this program is accepted in by Agda-2.3.0.1
>>>> and rejected by                Agda-2.3.2 :
>>>>
>>>> ---------------------------------------------------------------
>>>> powerToPositive : {c l : Level} -> {H : Semigroup c l} ->
>>>>              let C = Semigroup.Carrier H in  C -> (e : Nat) -> e > 0 ->
>>>> C
>>>> --
>>>> -- Power  x  to a positive degree  e.  The binary method.
>>>>
>>>> powerToPositive x e e>0 =  pow e e e>0
>>>>       where
>>>>       open Semigroup {{...}}
>>>>       pow : Nat -> (e : Nat) -> e > 0 -> Carrier
>>>>          -- cnt  is the counter used in termination proof
>>>>
>>>>       pow 0         _             _  = x
>>>>       pow _         0             ()
>>>>       pow _         (suc 0)       _  = x
>>>>       pow (suc cnt) (suc (suc e)) _  =
>>>>                                (if even? e then  p * p  else (p * p) *
>>>> x)
>>>>                                where
>>>>                                half = suc $ quot2 e
>>>>                                p    = pow cnt half $ positiveHalf? e
>>>> ---------------------------------------------------------------
>>>>
>> [..]
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda