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

[roconnor at theorem.ca]

The non-uniform inductive types I use make it more difficult to define 
recursion schemes.  I seem to recall a paper on how to define recursion 
schemes for theses sorts of types (probably written by Bird) in some 
cases.  I haven't reacquanted myself with that paper yet mostly because I 
don't define that many recursive functions.  Most of the work is spent 
doing inductive proofs proving equality of compositions of those few 
recursive functions, and I'm not sure I know any information on to do that 
generically for these sorts of non-uniform inductive types.

On Mon, 10 Aug 2015, Andrea Vezzosi wrote:

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

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