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

[Jan Stolarek]

Thank you all for responses. I came up with this proof:

+x : (a b : Nat) → a + suc b ≡ b + suc a
+x a b = trans (sym (+suc a b)) (trans (cong suc (+comm a b)) (+suc b a))

which indeed looks a bit ugly. I'll take a look at ≡-Reasoning some time in the future. For the 
moment I'm learning basics of Agda, so I'm reinventing the wheel wherever I can :-)

Janek

Dnia środa, 13 listopada 2013, Andrea Vezzosi napisał:
> 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