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

[Jan Stolarek]

Thanks Sergei! This looks more verbose, but it makes it clear what derives from what. I like that. 
As a beginner I'm only a bit scared of all these imports - I didn't find any documentation or 
tutorial of the standard library and learning it from the source comments seems like a daunting 
task.

Janek

Dnia czwartek, 14 listopada 2013, napisałeś:
> open import Algebra  using (module CommutativeSemiring)
> open import Data.Nat using (ℕ; suc; _+_)
> open import Data.Nat.Properties as NatProp using ()
>                  renaming (commutativeSemiring to natCommSemiring)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> open CommutativeSemiring natCommSemiring using (+-comm)
> open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
>                                                 _∎ to _≡end)
>
> +suc : (a b : ℕ) → a + suc b ≡ b + suc a
> +suc a b =
>      ≡begin
>        a + (suc b)    ≡[ +-comm a _ ]
>        (suc b) + a    ≡[ PE.refl ]  -- can be skipped
>
>        suc (b + a)    ≡[ PE.cong suc (+-comm b a) ]
>        suc (a + b)    ≡[ PE.sym PE.refl ]
>        (suc a) + b    ≡[ +-comm _ b ]
>        b + (suc a)
>      ≡end
>
> On Thu, 2013-11-14 at 09:45 +0100, Jan Stolarek wrote:
> > 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
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda