[Agda] "with .. postulate"

Serge D. Mechveliani mechvel at botik.ru
Thu Mar 7 18:53:20 CET 2013

On Wed, Mar 06, 2013 at 08:11:56PM +0100, Andreas Abel wrote:
> 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} e a))) ->
>          justYes? r \equiv true -> justYes? (invMb-sub a') \equiv true
>
>     go nothing                    ()
>     go (just (no _))              ()
>     go (just (yes (i , iProofs))) _ =  afterInv
>        where
>        postulate afterInv : justYes? (invMb-sub a') \equiv true
>

(I have changed a couple of math symbols)

> Hope this helps!

Indeed, it helps. Thank you.
I see now that my version of go' did not really present a proof.

And the subject is new for me.
Before yesterday I thought:
if I have a simple intuitive mathematical and constructive proof for a
statement, then it needs no real invention to convert it to a proof for
Agda.

And now I start to doubt in this. Because one also needs to find a
signature  sig  for helper functions like the above go'
(consider more complex examples). It needs to be found among many
possible ones, the argument expressions must belong to  sig,  and  sig
must be special enough to allow a proof.
1) I need to gain experience in this.
2) What people think of this:
provided that the implemnentation part is given, to what extent
finding a sufficient signature can be automated in general?

(for note that my go' and your go' have the same implementation code).

Thanks,

------
Sergei