[Changed the definition of _*_. Nils Anders Danielsson **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