[Agda] Q: Equational Reasoning

[Christoph Herrmann]

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
and comm* is a  theorem I defined myself  (since I do not know how to 
use the library yet).
Basically the body of the lambda abstraction reflects the expression on 
which the theorem
is applied and the abstracted variable the subterm to be rewritten.

> 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.
>
> 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?
>
> Andrej
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>   
Cheers

-- 
  Dr. Christoph Herrmann
  University of St Andrews, Scotland/UK
  phone: office: +44 1334 461629, home: +44 1334 478648
  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
  URL:   http://www.cs.st-andrews.ac.uk/~ch
 
  The University of St Andrews is a charity registered in Scotland: No SC013532