[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
More information about the Agda
mailing list