[Agda] difficulties with patterns

[Andreas Abel]

On 28.11.2013 18:05, Sergei Meshveliani wrote:
> Andreas responded recently:
>> Mmh, I would guess this is because Agda creates a local function for
>> the
>> \ { ... } (which is called "extended-lambda" in Agda-speak).
>>
>> What you can try instead is to write
>>
>>    case toBDigits n of \ pr ->
>>      let (bs , (_ , hasLast1-if-bs)) = pr
>>          ... more let bindings ...
>>
>>      in cong-...

Ah, I screwed this one up.  The case loses the connection between 
"toBDigits n" and "pr".  You should do without the case.

   hasLast1-toBDigs-suc : (n : ℕ) → HasLast1 $ toBDigs $ suc n
   hasLast1-toBDigs-suc n =
           let (bs , (_ , hasLast1-if-bs)) = toBDigits n
               digs-n'          = toBDigs $ suc n
               digs-n'=addC1-bs = toBDigs-suc-eq {n}

               hasLast1-addC1-bs : HasLast1 $ addC1 bs
               hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
           in
           cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs

Can you try again?

Cheers,
Andreas

> This is not type-checked:
>
>   hasLast1-toBDigs-suc : (n : ℕ) → HasLast1 $ toBDigs $ suc n
>   hasLast1-toBDigs-suc n =
>
>     case  toBDigits n
>     of \ pr →
>           let (bs , (_ , hasLast1-if-bs)) = pr
>               digs-n'          = toBDigs $ suc n
>               digs-n'=addC1-bs = toBDigs-suc-eq {n}
>
>               hasLast1-addC1-bs : HasLast1 $ addC1 bs
>               hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>           in
>           cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>
> The report
>
> --------------------
> (proj₁ pr) != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl))) of
> type (List Bit)
> when checking that the expression hasLast1-addC1-bs has type
> HasLast1 (addC1 (toBDigs n))
> -------------------
>
> looks similar as the previous one (see the citation below).
>
> I tried to compose a stand-alone example of 5 - 15 lines, but my first
> simple attempt has failed.
>
> If you do not see such an example, I could consider reducing the
> existing one.
>
> Regards,
>
> ------
> Sergei
>
>
>
> On Wed, 2013-11-27 at 18:27 +0400, Sergei Meshveliani wrote:
>> Please,
>> how can one avoid difficulties in using patterns?
>> (what is a common way out?).
>>
>> For example, this program works:
>>
>>   hasLast1-toBDigs-suc-n : (n : ℕ) → HasLast1 $ toBDigs $ suc n
>>   hasLast1-toBDigs-suc-n n =
>>               cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>>      where
>>      pr             = toBDigits n
>>      bs             = proj₁ pr
>>      hasLast1-if-bs = proj₂ $ proj₂ pr
>>
>>      digs-n'          = toBDigs $ suc n
>>      digs-n'=addC1-bs = toBDigs-suc-eq {n}
>>
>>      hasLast1-addC1-bs : HasLast1 $ addC1 bs
>>      hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>>
>>
>> Then I try to improve the style and replace the three assignments and
>> projections with pattern matching:
>>
>>      case toBDigits n
>>      of \
>>      { (bs , (_ ,  hasLast1-if-bs)) →
>>              let
>>                 digs-n'          = toBDigs $ suc n
>>                 digs-n'=addC1-bs = toBDigs-suc-eq {n}
>>
>>                 hasLast1-addC1-bs : HasLast1 $ addC1 bs
>>                 hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>>              in
>>             cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>>      }
>>
>> And obtain the report
>>
>>    bs != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl)))
>>    of type  (List Bit)
>>    when checking that the expression  hasLast1-addC1-bs  has type
>>    HasLast1 (addC1 (toBDigs n)).
>>
>> The checker somehow does not allow to improve style.
>>
>> Thanks,
>>
>> ------
>> Sergei
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> 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
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/