[Agda] "with .. postulate"

[Andreas Abel]

I see that Dominic has already answered your problem.

On 05.03.2013 18:05, Andreas Abel wrote:
> 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/