[Agda] Q: Equational Reasoning

[Liang-Ting Chen]

On Wed, May 27, 2009 at 1:33 PM, Andrej Bauer <andrej.bauer at andrej.com>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))"?


>
> A more basic question is how to explain to agda that the fact a=b can
> be used to replace a by b in an expression.

Hi,

Relation.Binary.PropositionalEquality.cong works for most case.


>
> 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?
>
hum it is possible, but personally, I think agda currently lacks the
facility like
Coq's tactics that could prove some trivial equations and properties.

I have constructed a proof of Grothendieck group with 300+ lines, but most
of
codes deal with trivial identities by commutativity and associativity.
Using the technique of reflection might solve this problem, but I'm not
familiar with this.

Proving the fundamental theorem of calculus is done with Coq few years ago.
You could find some information in the paper "Formalizing Real Calculus in
Coq" by Lus Cruz-Filipe.

>  Andrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090527/8ca255e7/attachment.html