[Agda] An Agda proof of the Church-Rosser theorem

[Andrea Vezzosi]

Hi Russel,

I have not read the code fully, but I can see that you also got
trapped into writing loads of boilerplate code to do proofs that are
mostly induction + congruence.

I'd be really interested in figuring out how to avoid these parts.

If we are trying to be very structured there would be something like
generic traversals from "scrap your boilerplate" haskell libraries,
with provided reasoning principles that allow proofs to only speak
about the interesting cases.

However it might be more realistic to define a tactic that just tries
to use congruence and otherwise fails, but still I don't know what the
interface would be for handling cases where that does not work without
having to write out the whole proof instead.

Cheers,
Andrea

On Tue, Aug 4, 2015 at 10:38 PM,  <roconnor at theorem.ca> wrote:
> URL: http://hub.darcs.net/roconnor/STLC/browse
>
> This is my first development in Agda. I'm interested in getting some
> feedback on this work of any sort, including but not limited to
>
>  * Abstractions in the standard library that I could take advantage of.
>  * Standard naming conventions I should be using.
>  * Where I should or shouldn't be using implicit arguments.
>  * Better use of unicode operators.
>  * Better argument orders.
>  * Should I be using equational reasoning?
>  * Ideas on how to use recursion schemes to simplify functions taking Terms.
> Recursions schemes for dependent families are kinda tricky.
>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda