[Agda] "with .. postulate"

[Serge D. Mechveliani]

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