[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
> 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.


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 ?



More information about the Agda mailing list