[Agda] "with .. postulate"

[Andreas Abel]

Your definition of 'go' almost works, you only have to abstract over 
(invMb a).  Calling this abstraction 'r', I get the following code which 
type-checks.

     go : (r : Maybe (Dec (Inverse {M = Mg} ε a))) ->
          justYes? r ≡ true -> justYes? (invMb-sub a') ≡ true

     go nothing                    ()
     go (just (no _))              ()
     go (just (yes (i , iProofs))) _ =  afterInv
        where
        postulate afterInv : justYes? (invMb-sub a') ≡ true

Hope this helps!

Cheers,
Andreas

On 06.03.13 11:38 AM, Serge D. Mechveliani wrote:
> On Tue, Mar 05, 2013 at 06:05:21PM +0100, Andreas Abel wrote:
>> It seems like the story is the following
>>
>> The original goal of totalInv-sub is
>>
>>    justYes? (invMb-sub a') \equiv true
>>
>> which normalizes to
>>
>> [..]
>
>> [..]
>>    justYes?
>>        (.Where._.invMb-sub upMon extSubDSet .Where._._.extSubsemig
>>         .Where._._.member-?? a'
>>         | Monoid.invMb Mon (repr a'))
>>        \equiv 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.
>>
>
>
> Of course, I tried earlier various approaches.
>
>     http://botik.ru/pub/local/Mechveliani/agdaNotes/rep2.zip
>
> presents the variant with the helper function `go' that matches on
> (invMb (repr a')).
>
> The report is different:
> --------------------------
> Failed to solve the following constraints:
>    [0] Is empty: justYes? (Monoid.invMb Mon (repr a')) \equiv true
>    [0] Is empty: justYes? (Monoid.invMb Mon (repr a')) \equiv true
> --------------------------
>
> (the line No is not reported).
> This looks like a different problem: the checker does not solve
> non-emptyness of the above type.
>
> But the second argument in `go' is exactly a value of this needed type.
>
> The idea of the code is that the value of  (totalInv a _)
> rejects the first two clauses in the definition of `go'.
>
> And I do not see how to explain this to the checker in any more detail.
>
> Can you, please, look into this  rep2.zip ?
>
> Thanks,
>
> ------
> Sergei
>

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