[Agda] Q: Equational Reasoning

[Conor McBride]

Hi folks

On 27 May 2009, at 11:21, Christoph Herrmann wrote:

> Hi Andrej
>
> Andrej Bauer wrote:
>> Hi,
>>
>> this might be a good opportunity to ask.  How does Agda deal with
>> equational reasoning in subterms? It's one thing to say "use
>> commutativity to prove that a * b equals b * a", but it's a different
>> game when we say "use commutativity to prove that f(x, g(a * b)) =
>> f(x, g(b* a))"?
>>
>
> I use (cong (\lambda p -> f (x,  g (  p ) )) (comm* {a} {b}) )   
> where cong stands for congruence

That's traditional: it's the term synthesized by
rewriting tactics in systems like Coq.

The annoying thing is writing down the blasted
rewriting context. It's particularly annoying as
the implementation of "with" must surely contain the
components required to synthesize such abstractions.

>> I am asking because I think Agda is very c00l, but I do not see (yet)
>> whether it's suitable for developing large swaths of mathematics. Any
>> opinions about that? What would it take to prove the fundamental
>> theorem of calculus, for example?

I'll make my usual remarks here. As a document format,
Agda files are good at presenting inhabitants of Sets:
often we care which inhabitant we get, and we want to
state what the actual Set is at most when the
construction is indirected via definition. By the same
token, Agda files are bad at explaining the
inhabitation of Props, because they expose unimportant
choices of particular proof terms and conceal meaningful
statements of subgoals. For my money, the declarative
Mizar-style has the edge in this territory.

I'd like to see a clearer Set/Prop distinction, with
support for the appropriate style in each. (Of course,
you need proof irrelevance to get away with it...)

We could also do with a clearer idea about how to
support the reflection method: it has that annoying
character of deliberate accident at the moment, and
is correspondingly too much like hard work. We
have some algebra we'd like to reflect. It so happens
that we can define the initial algebra on its
signature and then write an interpretation function:
who would have thought it? I don't know how to do
much better just now, but it's certainly worth
thinking about.

I guess I'd also make some vague sort of plea for the
McKinna philosophy of proof/programming as stepwise
problem decomposition, where possible decompositions
are specified by types. Agda only has this for
*expressions*, but Epigram has it for *programs*.
Agda hardwires the specific instance of constructor
case analysis (which is certainly worthy of more
sugary treatment than it got in Epigram 1), but it
throws away the general notion. I speculate that as
problems become more varied and interesting, a richer
language of problem solving will be needed.

I don't think I posted my experimental implementation
of a decision procedure for intuitionistic implicational
logic, with a flavour of Dyckhoff, There was a rather
enigmatic blogpost

   http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=187

which got curtailed by an emergency. I haven't cleaned
the file up at all, but I attach it for the intrepid.
The point is that it uses a recursive problem-solving
strategy which is beyond the power of Agda's termination
checker to recognize, but not beyond the power of type
theory to explain. I ended up writing a hand-elaborated
Epigram program in Agda's expression language. Granted,
that's currently the best sort of Epigram program you
can get, but still...

Have fun

Conor



-------------- next part --------------
A non-text attachment was scrubbed...
Name: Memo.agda
Type: application/octet-stream
Size: 8609 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20090527/ab4efc16/Memo.obj
-------------- next part --------------