# [Agda] "with .. postulate"

Serge D. Mechveliani mechvel at botik.ru
Wed Mar 6 11:38:45 CET 2013

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