[Changed the definition of _*_.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080407184806
 + The new definition matches the one used by the Coq standard
   libraries, and Ulf's simple-lib.
 + Some things became more complicated, but overall the new definition
   seems to be a win. For instance, concat and group in Data.Vec are
   now defined without any auxiliary lemmas. Furthermore 2*_ can be
   defined in terms of _*_.
] hunk ./Data/Digit.agda 17
-open import Algebra.Structures
hunk ./Data/Digit.agda 20
-open import Data.Product
hunk ./Data/Digit.agda 24
--- Some boring lemmas
+-- A boring lemma
hunk ./Data/Digit.agda 28
-  lem₀ : forall r k -> r + (k * 0 + 0 + 0) ≡ r
-  lem₀ r k = prove (Vec.fromList (r ∷ k ∷ []))
-                   (R :+ (K :* con 0 :+ con 0 :+ con 0)) R
-                   ≡-refl
-    where R = var fz; K = var (fs fz)
-
-  lem₁ : forall x k r -> 1 ≤ x -> 1 + x ≤′ x * (2 + k) + r
-  lem₁ x k r 1≤x = ≤⇒≤′ $ begin
-    1 + x
-      ≤⟨ 1≤x +-mono byDef ⟩
-    x + x
-      ≡⟨ *-comm 2 x ⟩
-    x * 2
-      ≤⟨ m≤m+n _ _ ⟩
-    x * 2 + x * k
-      ≡⟨ ≡-sym (proj₁ distrib x 2 k) ⟩
-    x * (2 + k)
+  lem : forall x k r -> 2 + x ≤′ r + (1 + x) * (2 + k)
+  lem x k r = ≤⇒≤′ $ begin
+    2 + x
hunk ./Data/Digit.agda 32
-    x * (2 + k) + r
+    2 + x + (x + (1 + x) * k + r)
+      ≡⟨ (let X = var fz; R = var (fs fz); K = var (fs (fs fz)) in
+         prove (Vec.fromList (x ∷ r ∷ k ∷ []))
+               (con 2 :+ X :+ (X :+ (con 1 :+ X) :* K :+ R))
+               (R :+ (con 1 :+ X) :* (con 2 :+ K))
+               ≡-refl) ⟩
+    r + (1 + x) * (2 + k)
hunk ./Data/Digit.agda 40
-    where open IsCommutativeSemiring _ ℕ-isCommutativeSemiring
-
-  lem₂ : forall {s} x r k -> s ≡ x -> r + k * s ≡ x * k + r
-  lem₂ x r k ≡-refl =
-    prove (Vec.fromList (x ∷ r ∷ k ∷ []))
-          (R :+ K :* X) (X :* K :+ R)
-          ≡-refl
-    where X = var fz; R = var (fs fz); K = var (fs (fs fz))
hunk ./Data/Digit.agda 104
-fromDigits {base} (d ∷ ds) = toℕ d + base * fromDigits ds
+fromDigits {base} (d ∷ ds) = toℕ d + fromDigits ds * base
hunk ./Data/Digit.agda 122
-  helper .(toℕ r) rec | result zero r ≡-refl =
-    exists (r ∷ []) (lem₀ (toℕ r) k)
+  helper .(toℕ r + 0 * base) rec | result zero r ≡-refl =
+    exists (r ∷ []) ≡-refl
hunk ./Data/Digit.agda 125
-  helper .(x * base + toℕ r) rec | result x@(suc _) r ≡-refl
-    with rec x (lem₁ x k (toℕ r) (s≤s z≤n))
-  helper .(x * base + toℕ r) rec | result (suc m) r ≡-refl
+  helper .(toℕ r + x * base) rec | result x@(suc _) r ≡-refl
+    with rec x (lem (pred x) k (toℕ r))
+  helper .(toℕ r + x * base) rec | result (suc m) r ≡-refl
hunk ./Data/Digit.agda 129
-    exists (r ∷ rs) (lem₂ (suc m) (toℕ r) base eq)
+    exists (r ∷ rs) (≡-cong (\x -> toℕ r + x * base) eq)
hunk ./Data/Nat.agda 69
-  mul _+_ n x = fold 0# (\s -> s + x) n
+  mul _+_ n x = fold 0# (\s -> x + s) n
hunk ./Data/Nat.agda 95
-suc m * n = m * n + n
+suc m * n = n + m * n
hunk ./Data/Nat.agda 116
-2* zero    = zero
-2* (suc n) = 2 + 2* n
+2* n = n * 2
hunk ./Data/Nat/DivMod.agda 32
-           dividend ≡ n * divisor + toℕ r ->
+           dividend ≡ toℕ r + n * divisor ->
hunk ./Data/Nat/DivMod.agda 49
-    result 0 (inject k (fromℕ m)) (inject-lemma m k)
+    result 0 (inject k (fromℕ m)) lemma
+    where
+    lemma = begin
+      m
+        ≡⟨ inject-lemma m k ⟩
+      toℕ (inject k (fromℕ m))
+        ≡⟨ (let X = var fz in
+           prove (toℕ (inject k (fromℕ m)) ∷ []) X (X :+ con 0) ≡-refl) ⟩
+      toℕ (inject k (fromℕ m)) + 0
+        ∎
hunk ./Data/Nat/DivMod.agda 80
-      suc n + (x * suc n + toℕ r)
-        ≡⟨ (let A = var fz; B = var (fs fz); C = var (fs (fs fz)) in
-            prove (suc n ∷ x * suc n ∷ toℕ r ∷ [])
-                  (A :+ (B :+ C)) ((B :+ A) :+ C)
+      suc n + (toℕ r + x * suc n)
+        ≡⟨ (let N = var fz; R = var (fs fz); X = var (fs (fs fz)) in
+            prove (suc n ∷ toℕ r ∷ x ∷ [])
+                  (N :+ (R :+ X :* N)) (R :+ (con 1 :+ X) :* N)
hunk ./Data/Nat/DivMod.agda 85
-      (x * suc n + suc n) + toℕ r
+      toℕ r + suc x * suc n
hunk ./Data/Nat/Properties.agda 61
-      m * suc n + suc n
-    ≈⟨ m+1+n≡1+m+n (m * suc n) n ⟩
-      suc (m * suc n + n)
-    ≈⟨ ≡-cong (\x -> suc (x + n)) (m*1+n≡m+mn m n) ⟩
-      suc (m +  m * n + n)
-    ≈⟨ ≡-cong suc (+-assoc m (m * n) n) ⟩
-      suc (m + (m * n + n))
+      suc n + m * suc n
+    ≈⟨ ≡-cong (\x -> suc n + x) (m*1+n≡m+mn m n) ⟩
+      suc n + (m + m * n)
+    ≈⟨ byDef ⟩
+      suc (n + (m + m * n))
+    ≈⟨ ≡-cong suc (≡-sym $ +-assoc n m (m * n)) ⟩
+      suc (n + m + m * n)
+    ≈⟨ ≡-cong (\x -> suc (x + m * n)) (+-comm n m) ⟩
+      suc (m + n + m * n)
+    ≈⟨ ≡-cong suc (+-assoc m n (m * n)) ⟩
+      suc (m + (n + m * n))
hunk ./Data/Nat/Properties.agda 81
-    n*0≡0 (suc n) =
-      begin
-        suc n * 0
-      ≈⟨ byDef ⟩
-        n * 0 + 0
-      ≈⟨ proj₂ +-identity _ ⟩
-        n * 0
-      ≈⟨ n*0≡0 n ⟩
-        0
-      ∎
+    n*0≡0 (suc n) = n*0≡0 n
hunk ./Data/Nat/Properties.agda 89
-      m * n + n
-    ≈⟨ ≡-cong (\x -> x + n) (*-comm m n) ⟩
-      n * m + n
-    ≈⟨ +-comm (n * m) n ⟩
+      n + m * n
+    ≈⟨ ≡-cong (\x -> n + x) (*-comm m n) ⟩
hunk ./Data/Nat/Properties.agda 105
-      m * (n + o) + (n + o)
-                                 ≈⟨ ≡-cong (\x -> x + (n + o)) (distˡ m n o) ⟩
-      (m * n + m * o) + (n + o)
-                                 ≈⟨ +-assoc (m * n) (m * o) (n + o) ⟩
-      m * n + (m * o + (n + o))
-                                 ≈⟨ ≡-cong (\x -> (m * n) + x) $ ≡-sym $ +-assoc (m * o) n o ⟩
-      m * n + ((m * o + n) + o)
-                                 ≈⟨ ≡-cong (\x -> (m * n) + (x + o)) $ +-comm (m * o) n ⟩
-      m * n + ((n + m * o) + o)
-                                 ≈⟨ ≡-cong (\x -> (m * n) + x) $ +-assoc n (m * o) o ⟩
-      m * n + (n + (m * o + o))
-                                 ≈⟨ ≡-sym $ +-assoc (m * n) n (m * o + o) ⟩
-      (m * n + n) + (m * o + o)
+      (n + o) + m * (n + o)
+                                 ≈⟨ ≡-cong (\x -> (n + o) + x) (distˡ m n o) ⟩
+      (n + o) + (m * n + m * o)
+                                 ≈⟨ ≡-sym $ +-assoc (n + o) (m * n) (m * o) ⟩
+      ((n + o) + m * n) + m * o
+                                 ≈⟨ ≡-cong (\x -> x + (m * o)) $ +-assoc n o (m * n) ⟩
+      (n + (o + m * n)) + m * o
+                                 ≈⟨ ≡-cong (\x -> (n + x) + m * o) $ +-comm o (m * n) ⟩
+      (n + (m * n + o)) + m * o
+                                 ≈⟨ ≡-cong (\x -> x + (m * o)) $ ≡-sym $ +-assoc n (m * n) o ⟩
+      ((n + m * n) + o) + m * o
+                                 ≈⟨ +-assoc (n + m * n) o (m * o) ⟩
+      (n + m * n) + (o + m * o)
hunk ./Data/Nat/Properties.agda 140
-    (m * n + n) * o
-                         ≈⟨ proj₂ distrib-*-+ o (m * n) n ⟩
-    (m * n) * o + n * o
-                         ≈⟨ ≡-cong (\x -> x + n * o) $ *-assoc m n o ⟩
-    m * (n * o) + n * o
+    (n + m * n) * o
+                         ≈⟨ proj₂ distrib-*-+ o n (m * n) ⟩
+    n * o + (m * n) * o
+                         ≈⟨ ≡-cong (\x -> n * o + x) $ *-assoc m n o ⟩
+    n * o + m * (n * o)
hunk ./Data/Nat/Properties.agda 150
-  *-identity = (\_ -> byDef) , n*1≡n
+  *-identity = proj₂ +-identity , n*1≡n
hunk ./Data/Nat/Properties.agda 159
+        n + 0
+      ≈⟨ proj₂ +-identity n ⟩
hunk ./Data/Vec.agda 29
-  lem₁ : forall n k -> n * k + k ≡ k + n * k
-  lem₁ n k = prove (n ∷ k ∷ [])
-                   (N :* K :+ K)
-                   (K :+ N :* K)
-                   ≡-refl
-    where N = var fz; K = var (fs fz)
-
-  lem₂ : forall m n -> m + n * m ≡ n * m + m
-  lem₂ m n = prove (m ∷ n ∷ [])
-                   (M :+ N :* M)
-                   (N :* M :+ M)
-                   ≡-refl
-    where M = var fz; N = var (fs fz)
-
hunk ./Data/Vec.agda 86
-concat                 []                   = []
-concat {a = a} {m = m} (_∷_ {n = n} xs xss) =
-  cast (lem₂ m n) (xs ++ concat xss)
+concat []         = []
+concat (xs ∷ xss) = xs ++ concat xss
hunk ./Data/Vec.agda 105
-group         {n = zero}  k [] = []
-group {a = a} {n = suc n} k xs
-  with splitAt k (cast (lem₁ n k) xs)
+group {n = zero}  k [] = []
+group {n = suc n} k xs with splitAt k xs