[Agda] Agda standard library tutorial?

[Andreas Abel]

Hi all,

is there a tutorial on how to use the standard library?  I am having 
(again) problems with the complexity of its organization.  My problem is 
rather simple.  I want to use commutativity and associativity of the 
boolean connectives.  Looking at Data.Bool.Properties, I have them there 
dangling right before my eyes:

------------------------------------------------------------------------
-- (Bool, ∨, ∧, false, true) forms a commutative semiring

private

   ∨-assoc : Associative _∨_
   ∨-assoc true  y z = refl
   ∨-assoc false y z = refl

   ...

But, sigh, they are private.  Ok, not too bad, there is a structure 
embedding them:

isCommutativeSemiring-∨-∧
   : IsCommutativeSemiring _≡_ _∨_ _∧_ false true
isCommutativeSemiring-∨-∧ = record
   { +-isCommutativeMonoid = record
     { isSemigroup = record
       { isEquivalence = isEquivalence
       ; assoc         = ∨-assoc
       ; ∙-cong        = cong₂ _∨_
       }
     ; identityˡ = λ _ → refl
     ; comm      = ∨-comm
     }
   ; *-isCommutativeMonoid = record
     ...

Somehow the simple names ∨-assoc,... are gone and replaced by some 
hierarchical structure of names.  Ok, how do I get to them?  I cannot 
project out of a record directly because the projections are tied in 
with the module associated to the record type, so let's find it in 
Algebra.Structures.

record IsCommutativeSemiring
          {a ℓ} {A : Set a} (≈ : Rel A ℓ)
          (_+_ _*_ : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   open FunctionProperties ≈
   field
     +-isCommutativeMonoid : IsCommutativeMonoid ≈ _+_ 0#
     *-isCommutativeMonoid : IsCommutativeMonoid ≈ _*_ 1#
     distribʳ              : _*_ DistributesOverʳ _+_
     zeroˡ                 : LeftZero 0# _*_

   private
     module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
     open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
            using () renaming (comm to *-comm)
   open EqR (record { isEquivalence = +-CM.isEquivalence })

   distrib : _*_ DistributesOver _+_
   distrib = (distribˡ , distribʳ)
     where
     distribˡ : _*_ DistributesOverˡ _+_
     distribˡ x y z = begin
       (x * (y + z))        ≈⟨ *-comm x (y + z) ⟩
       ((y + z) * x)        ≈⟨ distribʳ x y z ⟩
       ((y * x) + (z * x))  ≈⟨ *-comm y x ⟨ +-CM.∙-cong ⟩ *-comm z x ⟩
       ((x * y) + (x * z))  ∎

   zero : Zero 0# _*_
   zero = (zeroˡ , zeroʳ)
     where
     zeroʳ : RightZero 0# _*_
     zeroʳ x = begin
       (x * 0#)  ≈⟨ *-comm x 0# ⟩
       (0# * x)  ≈⟨ zeroˡ x ⟩
       0#        ∎

   isSemiring : IsSemiring ≈ _+_ _*_ 0# 1#
   isSemiring = record
     { isSemiringWithoutAnnihilatingZero = record
       { +-isCommutativeMonoid = +-isCommutativeMonoid
       ; *-isMonoid            = *-CM.isMonoid
       ; distrib               = distrib
       }
     ; zero                              = zero
     }

   open IsSemiring isSemiring public
          hiding (distrib; zero; +-isCommutativeMonoid)

   isCommutativeSemiringWithoutOne :
     IsCommutativeSemiringWithoutOne ≈ _+_ _*_ 0#
   isCommutativeSemiringWithoutOne = record
     { isSemiringWithoutOne = isSemiringWithoutOne
     ; *-comm               = *-CM.comm
     }

I must confess at this point I am lost.  What the h... are all these 
local modules and record and how on earth shall I quickly extract from 
this heap what the names of the innocent lemmata are I want to use??  My 
brain does not implement the Agda module system!  My clumsy attempt to 
open this structure fails:

open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Bool.Properties using (isCommutativeSemiring-∨-∧)
import Algebra.Structures
open Algebra.Structures.IsCommutativeSemiring isCommutativeSemiring-∨-∧ 
hiding (zero)
open import Relation.Binary.PropositionalEquality

Because now "refl" is ambiguous!

Forgive me, but at this point my patience is spent.  Before investing 
more hours fighting with a complex structure that I do not understand 
and which is documented by nothing than the source code, I give in to 
the temptation and cut-and-paste, or reimplement myself.

I think I am not the only one having this problem with the standard 
library.  Others might have more patients wrestling with the correct 
list of imports, module definitions, and opens.

What can be done about this?  I have some ideas, but cannot implement 
them myself (otherwise I would not have this problem...)

1. Write a tutorial for the standard library that shows how its 
definitions can be used.  I know that there are README files, but imho 
they only show how definitions can be used in principle, but not concretely.

2. Supply (documented) example programs for each of the library modules 
that explain how to use the stuff there.  Would that not also have the 
benefit to have some initial users and test cases?

3. Provide "preludes" that extract the most important definitions from a 
package into a single file, such that definitions are available directly 
without sophisticated module- or open-statements.  For instance, one 
could have a Data.Bool.Prelude, Data.Nat.Prelude, Data.List.Prelude etc.

Frustrated,
Andreas