[Agda] Holes 0.1.0

[Bradley Hardy]

Hi Victor,

I’ve seen your library before — it is indeed unfortunate that the new reflection API broke it so thoroughly!

First, I’ll mention that explicitly marking where we want to rewrite was a design choice for this library. The idea is that it potentially makes things clearer to the reader while not actually being much of a burden to the writer (at least compared to writing out `cong (\h -> …)` everywhere…). And it saves having to do any kind of proof search, so type-checking is quick!

But you’re right, it would be nice to be able to do things more automatically, too, and it should definitely be doable. I could imagine building a list of ‘possible holes’ in the LHS. Then I would try to apply my macro as it stands to each of those until one type checks.

Inferring the parameters passed to the lemma for rewriting could be done as well, but might be more difficult in the general case. I think that, since the lemma might use its parameters to generate the proof in an arbitrary way, this might not even always be possible. I’m sure the general strategy that you used in `agda-rw` would still work though!

Bradley

> On 27 Jan 2017, at 13:42, Victor Miraldo <v.cacciarimiraldo at gmail.com> wrote:
> 
> Hello Bradley,
> 
> Interesting library, thanks! It is nice to see people are still working
> on better equational reasoning! :)
> 
> I did some related work in the past
> (https://github.com/VictorCMiraldo/agda-rw) but
> soon after that Agda changed its reflection API. This rendered our
> library unusable for
> newer versions of Agda.
> 
> Since we had to do our unification from scratch, we could get away
> without having to explicitly
> mark where we wanted the rewrite or even the parameters to be passed
> to the lemma used
> to rewrite. How hard would it be to extend your approach for one or
> both of these features?
> 
> Cheers,
> Victor