[Agda] Agda standard library tutorial?

[gallais at EnsL.org]

Hi andreas,

I was also quite lost when I first looked at this and I ended up
mimicking what Nils does in the ring solver files. This is (I guess)
the pattern that you are looking for:

=======
import Data.Bool.Properties as BoolProp
import Algebra.Structures as Struct
private module BSR = Struct.IsAStructure
BoolProp.istheproofassociatedtothisstructure
=======

You can now use BSR.F to access the field F.

Cheers,

--
guillaume


On 13 January 2011 15:03, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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
>
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>