I think it would be very useful (especially for beginners) to present a simple interface to the basic properties of Data.Nat.

Rather than writing difficult to remember/understand code like:

open import Data.Nat
open import Algebra
import Data.Nat.Properties as Nat
private
module CS = CommutativeSemiring Nat.commutativeSemiring

ex₃ : ∀ m n → m * n ≡ n * m
ex₃ m n = CS.*-comm m n

I would like to be able to write:

open import Data.Nat
open import Data.Nat.Properties

ex₃ : ∀ m n → m * n ≡ n * m
ex₃ m n = *-comm m n

Perhaps the current contents of Data.Nat.Properties could be moved to another file and its functionality surfaced in a new simpler to use Data.Nat.Properties.

I get the following error:

/usr/share/agda-stdlib/src/Data/Colist.agda:387,23-29
from (Prod.proj₂ .x) (Prod.proj₂ (Prod.proj₂ (to (here p)))) !=
here p of type Any P (.x ∷ .xs)
when checking that the expression P.refl has type
from (Prod.proj₂ (Prod.proj₁ (to (here p))))
(Prod.proj₂ (Prod.proj₂ (to (here p))))
≡ here p

Commenting out Any-∈ (lines 360-388) permits type checking the entire file.

System:
Ubuntu 14.04 Server
The Glorious Glasgow Haskell Compilation System, version 7.6.3
Intel(R) Xeon(R) CPU E5-2650 0 @ 2.00GHz

Reproduced on the following commit:
bd6b7c0 (master)
e271944 (gh-pages)

Standard library has several statements for Data.List.++ (in Data.List.Properties).
But what about these two?

++[] : ∀ {α} {A : Set α} → (xs : List A) → xs ++ [] ≡ xs

++assoc : ∀ {α} {A : Set α} → (xs ys zs : List A) →
(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)

The commit d2b764f should be cherry-picked in the 2.4.2.1 branch.

+-mono is declared as infix in Dat.Nat.Properties -- unlike ∸-mono.

But they probably need to have the same format.

Agda 2.4.2.4 has been released. We haven't a released version of the library that type-checks with this version of Agda.

I think it's desirable back-port some commits from the master branch into the 2.4.2.4 branch before the release.

DecTotalOrder exports reflexive and trans. And these names are also exported by IsEquivalence for _≈_. Besides IsEquivalence and _≈_ are inside DecTotalOrder. This leads to a confusion.

It not this better to have ≤refl and ≤trans instead?

If the fixity of set intersection ∩ in Relation.Unary was changed to match the tuple type in Data.Product × and , the resulting pattern matches and constructions would be cleaner.

• infixl 7 ∩
• infixr 7 ∩

This would allow:

f : {A : Set} {P Q R : A → Set} → Σ A (P ∩ Q ∩ R) → ⊤
f (x , p , q , r) = _

The 2.4.2.1 branch has 21 commits which haven't been merged in the master branch. The list of the commits is https://github.com/agda/agda-stdlib/compare/2.4.2.1.

Please @andreasabel, @gallais and @np merge your commits into the master branch.

May be it has sense to add this to Standard library:

foldl++homo : ∀ {α β} {A : Set α} {B : Set β} → 
                           (f : A → B → A) → (x : A) → (ys zs : List B) →
                       foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs

I have a question about Relation.Binary.Core._Respects₂_

It is defined so that it is difficult to use. Normally, the programmer needs to write

 ~resps≈  x≈x'  y≈y'  x~y        -- (1)

for deriving x' ~ y' from x ≈ x', y ≈ y' and x ~ y where ~resps≈ : _~_ Respects₂' _≈_

Without using `Respects₂' (defined in an evident way), what may be a simple expression for (1)?
Am I missing something?

Would it make sense to add another variant of PreorderReasoning that simplifies reasoning on views (i.e. successive application of dependently-typed functions)?

Please see https://stackoverflow.com/q/22676703/3168666 for an example application and two example implementations.

Is there scope for further generalization?

The abbreviation 'mono' in the function names

                      '+-mono', 'pred-mono',  and such

looks a bit ambiguous. And 'monot'

will point more definitely to the monotonicity property with respect to <=.

After fixing issue #52, please add the changelog entry to https://github.com/agda/agda-stdlib/blob/2.4.2.1/CHANGELOG.

Reported by [email protected], Jan 10, 2014

The following is suggested for Data.Sign.Properties and
Data.Integer, Data.Integer.Properties.

1. For Data.Sign :

   _s-assoc : Associative _s
   _s-comm : Commutative _s
   *s-invol : (s : Sign) → s *s s ≡ Sign.+

This is for *s = Sign.*.
I use these lemmata, and they are evidently of a general use.

1. For Data.Integer, Data.Integer.Properties :

divMod is desirable for division with remainder, with proofs.

It can be lifted from Nat.DivMod.divMod.
But this lift still needs implementation.

For example, I need

decDivide : (x y : ℤ) → Dec $ RightQuotient intSetoid * x y

-- which also returns proof/disprove for \exist \q -> y * q == y.
It can be either by calling Integer.divMod
or by lifting to ℤ from a similar decDivide-Nat for Nat.
My implementation for this lifting takes about 200 lines
(despite that the subject looks trivial).

I think, Integer.divMod will help in this and in many other cases,
and I suspect that its lifting to ℤ will take not less than 100 lines.

1. The following are useful :

   negneg : (x : ℤ) → - (- x) ≡ + x

   x+◃ : (m : ℕ) → (Sign.+ ◃ m) ≡ + m
   -◃ : (m : ℕ) → (Sign.- ◃ m) ≡ - (+ m)

   +m*+n= : (m n : ℕ) → (+ m) * (+ n) ≡ + (m *n n)

   -*- : (x y : ℤ) → (- x) * (- y) ≡ x * y

   s◃m*s'◃n : (s s' : Sign) → (m n : ℕ) →
   (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n)

(for the last one I have a proof of about 30 lines).

Please cherry-pick the commits 656c248 and b2ef507 in the 2.4.2.1 branch.

TODO:

• Prepare the repo
• Update wiki
• Announce on mailing list

Shouldn't all values, such as Data.List.monad now be declared as instances?

instance
    monad : ∀ {ℓ} → RawMonad (List {ℓ})
    monad = record
      { return = λ x → x ∷ []
      ; _>>=_  = λ xs f → concat (map f xs)
      }

Or am I supposed to declare these values as instances locally?

import Data.List as List
private
    instance
        ListMonad = List.monad

The Makefile installs the "lib" package system-wide when it's run. I was wondering if this isn't perhaps a bit too much for what basically amounts to a utility script. Would it maybe be better just to call

cabal install --dependencies-only
runhaskell GenerateEverything.hs

instead of

cabal install
GenerateEverything

?

It is probably natural to add to Standard library the following two lemmas.

  foldr-ys++y-eq : ∀ {α β} {A : Set α} {B : Set β} →
                            (f : A → B → B) → (x : B) → (y : A) → (ys : List A) →
                           foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys

  foldl-≗foldr∘reverse : ∀ {α β} {A : Set α} {B : Set β} →
                                     (f : A → B → B) → (x : B) → (ys : List A) →
                                    foldl (flip f) x ys ≡ foldr f x (reverse ys)

Need them to be added?

Probably, it worths to add this to Data.Nat.Divisibilty :

∤ : Rel ℕ 0ℓ
∤ x = ¬_ ∘ ∣ x

What the summary says. These properties were added in 131e69d. Please add the missing entry in https://github.com/agda/agda-stdlib/blob/2.4.2.1/CHANGELOG.

I've spent the last few days playing with travis to build various projects of mine and applied the newly acquired knowledge to Agda's standard library.

Here is the result
Here are the builds
Here is my repo with the appropriate scripts, travis file and cleaned up gh-pages branch.

Now, travis needs a token from a user allowed to push to the repository in order to deploy the pages so I can't really prepare a pull request that would work. I can either explain to someone how to replicate the work based on the state my repo is in or do it myself if you give me push rights.

Happy holidays,

May be it has sense to add this to Standard library:

length∘reverse-eq : ∀ {α} {A : Set α} → length ∘ reverse {A = A} ≗ length

Consider proofs for things like

  P Respects _≈_ → (¬_ ∘ P) Respects _≈_,

  x ≈ x' -> y ≈ y' -> x ∤ y -> x' ∤ y'   (for a generic "not divides").

I write for this:

  ¬respects : ∀ {α α= β} →  {A : Set α} → (_≈_ : Rel A α=) → Symmetric _≈_ →
                                           (P : A → Set β) → 
                                           P Respects _≈_ → (¬_ ∘ P) Respects _≈_
  ...
  ¬respects = ...

But has Standard library something for this?
If not, then needs it to have?

After fixing issue #46, please add a changelog entry for the commit d2b764f in the file https://github.com/agda/agda-stdlib/blob/2.4.2.1/CHANGELOG.

.../std-lib/README/Container/FreeMonad.agda:58,8-34
Could not parse the application runState prog 0 ≡ true , 1
Operators used in the grammar:
  , (prefix operator, level 4) [,_ (.../std-lib/src/Data/Product.agda:68,1-3)]           
  , (infixr operator, level 4) [_,_ (.../std-lib/src/Data/Product.agda:21,15-18)]        
  ≡ (infix operator, level 4)  [_≡_ (.../std-lib/src/Relation/Binary/Core.agda:147,8-11)]
(the treatment of operators has changed, so code that used to parse
may have to be changed)
when scope checking runState prog 0 ≡ true , 1

What the title says. I guess there needs to be a branch for maint-2.4.2 compatibility.

to-≡ from Data.Vec.Equality converts from vector equality to homogeneous equality, but only once you've done the work of casting the arguments so that they have the same length. That seems enough work that it'd be worth it having it in the stdlib, together with to-≡.
I certainly want to-≅. Part of the problem shows up also for ≅-to-≡ — see ≅-to-subst-≡ for an alternative.

Here's an example of the functions I'd like to have and some example:

-- Let's try to use the result of xs++[]=xs as an equality.
-- This problem was posted by Fuuzetsu on the #agda IRC channel.

module VectorEqualityExtras (A : Set) where

open import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; ≡-to-≅)

open import Function

open import Data.Vec
open import Data.Vec.Properties
open import Data.Vec.Equality
open UsingVectorEquality (setoid A)
open PropositionalEquality

{-
-- Does not work. The problem is that vector equality is semi-heterogeneous, in
-- that the two compared vectors do not need to have, a priori, the same length.
-- So you can't convert it to a homogeneous equality.
xs++[]=xs-propEq : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≡ xs
xs++[]=xs-propEq xs = to-≡ (xs++[]=xs xs)
-}

to-≅ : ∀ {a} {A : Set a} {m n} {xs : Vec A m} {ys : Vec A n} → xs ≈ ys → xs ≅ ys
to-≅ p with length-equal p
to-≅ p | P.refl = ≡-to-≅ (to-≡ p)

≅-to-t-≡ : ∀ {a} {A B : Set a} {xs : A} {ys : B} → (p : xs ≅ ys) → A ≡ B
≅-to-t-≡ H.refl = P.refl

-- If you need a propositional equality, you'll have to use subst on one side.
-- However, we can do that for you, in different ways.

-- A generic way to convert heterogeneous to homogeneous equality.
≅-to-subst-≡ : ∀ {a} {A B : Set a} {xs : A} {ys : B} → (p : xs ≅ ys) → subst (λ x → x) (≅-to-t-≡ p) xs ≡ ys
≅-to-subst-≡ H.refl = P.refl

-- We can use it to build the following:
to-subst-≡′ : ∀ {a} {A : Set a} {m n} {xs : Vec A m} {ys : Vec A n} → (p : xs ≈ ys) → subst (λ x → x) (≅-to-t-≡ (to-≅ p)) xs ≡ ys
to-subst-≡′ = ≅-to-subst-≡ ∘ to-≅

-- A more specific one, with a more precise type for you.
to-subst-≡ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} → (p : xs ≈ ys) → subst (Vec A) (length-equal p) xs ≡ ys
to-subst-≡ {xs = xs} p = H.≅-to-≡
  (H.trans
    (H.≡-subst-removable (Vec A) (length-equal p) xs)
    (to-≅ p))

-- Working variants of xs++[]=xs-propEq:
xs++[]=xs-hEq : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≅ xs
xs++[]=xs-hEq xs = to-≅ (xs++[]=xs xs)

xs++[]=xs-subst-propEq : ∀ {n} → (xs : Vec A n) → subst (Vec A) (length-equal (xs++[]=xs xs)) (xs ++ []) ≡ xs

-- Without to-subst-≡, we need an inlined version of it:
{-
xs++[]=xs-subst-propEq xs = H.≅-to-≡
  (H.trans
    (H.≡-subst-removable (Vec A) (length-equal (xs++[]=xs xs)) (xs ++ []))
    (xs++[]=xs-hEq xs))
-}

xs++[]=xs-subst-propEq xs = to-subst-≡ (xs++[]=xs xs)

This code also lives at
https://gist.github.com/Blaisorblade/87d7d50167704603e682

The current Algebra hierarchy is parametrized by levels and not Carrier, thus making it hard if not impossible to use with instance arguments (like type classes). However, the equivalence relation complicates fixing this.

The Standard library lib-0.7 has module Data.Fin.Props
and several module names of the kind .Properties

For unification, I suggest to set ".Props" in all these names.

Is there StrictTotalOrder for Integer ?

People, I need help with installing agda-stdlib-2.4.0.tar.gz.
I have installed Agda-2.4.0.tar.gz,
then untarred agda-stdlib-2.4.0, did
cd ffi
cabal install

It reports

cabal: Could not resolve dependencies:
trying: agda-lib-ffi-0.0.2 (user goal)
next goal: base (dependency of agda-lib-ffi-0.0.2)
rejecting: base-4.7.0.0/installed-018... (conflict: agda-lib-ffi =>
base>=3.0.3.1 && <4.7)
rejecting: base-4.7.0.0, 4.6.0.1, 4.6.0.0, 4.5.1.0, 4.5.0.0, 4.4.1.0, 4.4.0.0,
4.3.1.0, 4.3.0.0, 4.2.0.2, 4.2.0.1, 4.2.0.0, 4.1.0.0, 4.0.0.0, 3.0.3.2,
3.0.3.1 (global constraint requires installed instance)

Dependency tree exhaustively searched.

I am in Debian Linux.
ghc-pkg list shows only base-4.7.0.0 for base'. Probably, base-4.7.0.0 is needed for ghc-7.8.2, which I am using independently from Agda. Probably, agda-stdlib-2.4.0 needs a lower version ofbase'.
What may be a way out?
How to satisfy both ghc-7.8.2 and agda-stdlib-2.4.0 ?

Thanks,

Sergei

We'll release Agda 2.4.2.3 (see https://code.google.com/p/agda/issues/detail?id=1482). It's necessary to release a version of the library compatible with this version of Agda.

I think it's desirable back-port some commits from the master branch into the 2.4.2.3 branch before the release.

I have a code for StrictTotalOrder for Integer and some others items
-- to propose as an addition to Standard library. (the modules Nat1 and Integer1).
But how to attach here the .zip file?

Relation.Binary.Core has _Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _

And I introduce

  Respects₂gen : ∀ {α α= β β= ℓ} {A : Set α} {B : Set β} →
                               (A → B → Set ℓ) → Rel A α= → Rel B β= → Set _  
  Respects₂gen _~_ _~₁_ _~₂_ = ∀ {x x' y y'} → x ~₁ x' → y ~₂ y' → x ~ y → x' ~ y'

Example:

Respects₂gen _∈_ _≈_ _=set_ =    x ≈ x' → ys =set ys' → x ∈ xs → x' ∈ ys'`

expresses that the equality =set on lists (\xs ys -> xs ⊆ ys × ys ⊆ xs) agrees with
the equality _≈_ on elements and with the relation _∈_ betwen elements and lists.

Has Standard library a replacement for Respects₂gen ?
Has it a denotation for (A → B → Set ℓ) ?
(somewhat "Rel-heterogeneous A B" ? ...)

Blocked on #72.

The constructor name 'instance' of Visibility in Reflection.agda can no longer be used because it is now a keyword. It should be renamed.

I need the following analogue for Data.Nat.Properties.*-mono :

suc<-monot : (n : ℕ ) → (__ (suc n)) Preserves < ⟶ <

Its proof has 18 nonempty lines and uses the representation m' + d ≡ k for m' ≤ k
(and d = k ∸ m').

Need Standard library to have something additional related to * and (Preserves < ⟶ <) ?
I am missing some nice way to implement *suc<-monot ?

Lib 0.8.1 has (in Data.List.All)

tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → (∀ {x} → x ∈ xs → P x) → All P xs

And I need its `reverse' -- for (A : Setoid), C = Carrier, '≈'.
I implement
All-P→∀x∈xs-P : ∀ {p} {P : C → Set p} {xs} → P Respects ≈ → All P xs →
(∀ {x} → x ∈ xs → P x)
Has Standard library something of this sort?

The commits a85ed0e and 58ce766 broke the invariant.

The definition @asajeffrey proposes is the following:

  POSTULATE[_↦_] : ∀ {ℓ m} {A : Set ℓ} {B : A → Set m} → ∀ a → B a → (∀ a → B a)
  POSTULATE[ a ↦ b ] a′ with trustMe {x = a} {a′}
  POSTULATE[ a ↦ b ] .a | refl = b

I propose to name it postulate[_↦_] because:

• it is a valid name as well
• will trigger if one "grep postulate"
• looks less loud

Does Standard library need to implement

        all∘ :  ... →  All P (map f xs)  ←→ All (P ∘ f) xs

?
(is it somehow by All.map ?)

maint$ agda-stdlib src/Data/AVL.agda
...
Ambiguous name compare. It could refer to any one of
  Data.Nat.Base.compare
  bound at
  /home/asr/src/agda-stdlib/agda-stdlib-2.4.2.4/src/Data/Nat/Base.agda:180,1-8
  .Data.AVL._.compare
  bound at
  /home/asr/src/agda-stdlib/agda-stdlib-2.4.2.4/src/Relation/Binary.agda:360,5-12

This issue was introduced by 86676d7.

has it (DecTotalOrder Bin) ?

As Standard library has map-with-∈, probably, it also needs analogues of cong-map
(, map-compose, map-id, ... ?) for map-with-∈ for the pointwise equlaity on lists.
Say,

module _ {α α= β β=} {A : Setoid α α=} {A' : Setoid β β=} where
  ...
  map-with-∈-cong : ∀ xs → (f g : ∀ {x} → x ∈ xs → C') →
                                 (∀ {x} → (x∈xs : x ∈ xs) → f x∈xs ≈' g x∈xs) →
                                 map-with-∈ xs f  =p  map-with-∈ xs g,

  map-with-∈≗map : ∀ xs → (f : C → C') → map-with-∈ xs (\ {x} x∈xs → f x)  =p  map f xs

-- ?

analogues and such for `map-with-∈

Has Standard library something for this?

  counterimageInList : 
      (f : A → B) → {xs : List A} → {y : B}  →  y ∈' (map f xs) → ∃ \x → (x ∈ xs) × (f x ≈' y)

(≈, ∈ are on A; ≈', ∈' are on B).

This recursive universe-polymorphic definition of vectors fails to compile with the ⊤ defined in Data.Unit:

Vec : ∀ {α} -> Set α -> ℕ -> Set α
Vec A zero = ⊤
Vec A (suc n) = A × Vec A n

Set != Set .α
when checking that the expression ⊤ has type Set .α

I had to make my own universe-polymorphic copy of ⊤.

record ⊤ {α} : Set α where
  constructor ⟨⟩

Why doesn't the version in the library look like this? Would you be open to a pull request to change it?

I wonder of wherher the library needs some generalized zipWith-n functions.
For example, the below function is actually zipWith3,
but one list is by List and others are by List.All:

   zip3with? : (triples : List (C × ℕ × C))  →  All.All ^eq triples  →
                    All.All (\e → e > 0) $ map tuple32 triples  →  List Item 
    zip3with? [] _ _  =  []
    zip3with? ((p , e , d) ∷ triples) (d=p^e ∷a eqs) (e>0 ∷a restExps>0) =
                                                      item ∷ (zip3with? triples eqs restExps>0)
                                                     where
                                                     item = record{ ... }