[Agda] "with .. postulate"

[Andreas Abel]

It seems like the story is the following

The original goal of totalInv-sub is

   justYes? (invMb-sub a') ≡ true

which normalizes to

   justYes?
   (.Where._.invMb-sub upMon extSubDSet .Where._._.extSubsemig
    .Where._._.member-ε a'
    | Monoid.invMb Mon (repr a')) ≡ true

Since you with-abstract over

  invMb (repr a')

which normalizes to

   Monoid.invMb Mon (repr a')

this expression is replaced in your goal by the match

   just (yes (i , iProofs))

so the goal becomes

   justYes?
   (.Where._.invMb-sub upMon extSubDSet .Where._._.extSubsemig
    .Where._._.member-ε a'
    | just (yes (i , iProofs))) ≡ true

which further normalizes to

   justYes?
       (just
        (.Where._.decInv-sub upMon extSubDSet .Where._._.extSubsemig
         .Where._._.member-ε (repr a') (member-repr a') (i , iProofs)
         | (member? ⟨$⟩ i) Data.Bool.≟ true))
       ≡ true

You can see this if you replace the rejected attempt "afterInv" by a ?

But the type of postulate afterInv is

   justYes? (invMb-sub a') ≡ true

which normalizes to

   justYes?
       (.Where._.invMb-sub upMon extSubDSet .Where._._.extSubsemig
        .Where._._.member-ε a'
        | Monoid.invMb Mon (repr a'))
       ≡ true

and this is not convertible with the type of your goal.

How to get out of this?

1. Do not use with in this case, but define your own auxiliary function 
that lets you match on (invMb (repr a')).

Internally, Agda translates every 'with' into an auxiliary function, 
using a heuristic to abstract over the 'with'-expressions in the goal. 
Sometimes the heuristic does not do what you expect, e.g., in your case.

2. Use some tricks that prevent Agda from normalizing so far (which is 
further than you want it).  Ask the list for these tricks, or the people 
in the chat, I have not used them.

Hope this helps.

Cheers,
Andreas

On 05.03.2013 16:18, Serge D. Mechveliani wrote:
> On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:
>> Sorry, I cannot explain this, because I cannot run your example
>> (incomplete). --Andreas
>>
>
>
>      http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip
>
> contains the precise  Main.agda  and  readme.agda
> (please, read first  readme.agda).
> I am sorry: the proggram is large.
> I tried to present a small example, but have failed.
> Of course, it can be reduced, say, 10 times, but this would need a
> considerable effort.
> It looks like I am currently stuck in my attempt to write a library.
>
> Thank you in advance for help,
>
> -------
> Sergei
>
>
>
>> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:
>>> Dear all,
>>> the attachement  t.agda.zip
>>>
>>> contains a small code example where the same declaration of kind
>>>                                          postulate p : <signature>
>>> is taken in   Agda-2.3.2 MAlonzo
>>> as a correct type for  p  or not  -- depending on whether  p  is set
>>> directly after ` = ' or in the last branch for `with'.
>>>
>>> Can you, please, explain this?
>>>
>>>
>>>
>>> _______________________________________________
>>> 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/
>> 	
>


-- 
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/