[Agda] Proving a + suc b == b + suc a
Martin Escardo
m.escardo at cs.bham.ac.uk
Wed Nov 13 12:48:49 CET 2013
On 13/11/13 11:27, Jan Stolarek wrote:
> Hi *,
>
> I'm trying to prove that: a + suc b == b + suc a. I see the solution on paper, but I don't know
> how to express it in Agda:
>
> 1. From the commutativity of addition (+comm a b) I know that:
> a + b == b + a
> 2. Using congruence I know that
> suc (a + b) == suc (b + a)
> 3. I also know +suc, which proves that:
> suc (a + b) = a + suc b
>
> Now if I could apply +suc to both sides of (cong suc (+comm a b)) I would turn:
> suc (a + b) == suc (b + a)
> into:
> a + suc b == b + suc a
> which would end my proof. How can I do that?
You don't need to do anything in the last step, because both equations
are definitionally the same. You are done.
M.
More information about the Agda
mailing list