[Agda] small oddity of DistributesOver in the standard library 0.7

[Kenichi Asai]

I report on a small oddity I encountered with the standard library 0.7.

Attached is a proof for: 2 * (1 + 2 + ... + n) = n * (1 + n).
During the proof, I used both of the following laws:

(A) (y + z) * x = y * x + z * x
(B) x * (y + z) = x * y + x * z

These laws are proved in isCommutativeSemiring in Data.Nat.Properties.
After declaring:

  open import Algebra.Structures  -- for IsCommutativeSemiring
  private module M = IsCommutativeSemiring

I can use for (A) either of the following two:

  M.distrib^r isCommutativeSemiring x y z
  proj_2 (M.distrib isCommutativeSemiring) x y z

But for (B), I can use only:

  proj_1 (M.distrib isCommutativeSemiring) x y z

Why is M.distrib^l not provided for (B)?  If it happens to be so
without reasons, I would like it to be defined, too.  (Or, to attain
symmetry, one could remove M.distrib^r, but I rather prefer having
M.distrib^l defined.)

I don't have enough skill to change the standard library, but I hope
somebody can fix it in the future (but without any pressure).

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module Sum where

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.??Reasoning

open import Data.Nat.Properties -- for isCommutativeSemiring
open import Algebra.Structures  -- for IsCommutativeSemiring
private module M = IsCommutativeSemiring

sum : ??????sum zero = zero
sum (suc n) = suc n + sum n

lemma1 : (n : ?? ??2 * (sum n) ??n * suc n
lemma1 zero = refl
lemma1 (suc n) = begin
   2 * sum (suc n)
  ??? proj??(M.distrib isCommutativeSemiring) 2 (suc n) (sum n) ??   2 * suc n + 2 * sum n
  ??? cong (_+_ (2 * suc n)) (lemma1 n) ??   2 * suc n + n * suc n
  ??? sym (M.distrib? isCommutativeSemiring (suc n) 2 n) ??   (2 + n) * suc n
  ??? M.*-comm isCommutativeSemiring (2 + n) (suc n) ??   suc n * suc (suc n)
  ??