[Agda] Proving a + suc b == b + suc a

[Andrea Vezzosi]

On Wed, Nov 13, 2013 at 12:27 PM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:

> [...]
> 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?
>
>
To chain proofs like that you can use transitivity:

  trans : forall {A}{x y z : A} -> x == y -> y == z -> x == z
  trans refl eq = eq

in fact you'll need to nest them to apply something on both sides:

  trans (....) (trans (cong suc (+comm a b)) (....))

(Usually at this point the thing gets less than readable and we use the
prettier syntax provided by ≡-Reasoning in
Relation.Binary.PropositionalEquality from the stdlib.)

-- Andrea


> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131113/7ae76819/attachment.html