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

[Jan Stolarek]

Thanks. I think I'll take a look at least at some modules of the standard library. I just did a 
proof that (a + suc b) + c ≡ b + suc (c + a) and the result looks like LISP:

+case4 : (a b c : Nat) → (a + suc b) + c ≡ b + suc (c + a)
+case4 a b c = trans (sym ((cong (λ n → n + c) (+suc a b))))
              (trans (cong suc
              (trans (cong (λ n → n + c) (+comm a b))
              (trans (+assoc b a c) (cong (λ n → b + n) (+comm a c))))) (+suc b (c + a)))

Janek

Dnia czwartek, 14 listopada 2013, Serge D. Mechveliani napisał:
> On Thu, Nov 14, 2013 at 10:21:47AM +0100, Jan Stolarek wrote:
> > 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
>
> Most of  `using ...'  parts can be omitted here, and  emacs  can show
> the place in the corresponding module for each item clicked at in the
> current source.
>
> But I import items explicitly, because this makes a program more clear.
> For example,  `setoid' and _+_  occur in many diferent library modules,
> and have many different meanings.
>
> > - I didn't find any documentation or tutorial of the standard library
> > and learning it from the source comments seems like a daunting task.
>
> Yes. After 17 months with Agda, I still ask sometimes
> "has Standard library such and such thing?".
>
> 1) I thank Agda people for answering to such.
>
> 2) For a beginner, it has sense to inspect (after, say, 2 months
>    experience) _all_ the Agda code of Standard library, paying attention
>    to signatures and skipping (for the first studying) most of
>    implementation.
>
> 3) A regular documentation on the library is desirable, of a similar
>    kind as on the language
>    (a messy and boring work -- I agree).
>    For example, look at the on-line doc on the Haskall-2010 Standard
>    library.
>
> Regards,
>
> ------
> Sergei
>
> > Dnia czwartek, 14 listopada 2013, napisa??e??:
> > > open import Algebra  using (module CommutativeSemiring)
> > > open import Data.Nat using (???; suc; _+_)
> > > [..]