123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869-------------------------------------------------------------------------- The Agda standard library---- Some extra lemmas about natural numbers only needed for-- Data.Integer.Properties (for distributivity)------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Integer.Properties.NatLemmas where open import Data.Nat.Base using (ℕ; _+_; _*_; suc)open import Data.Nat.Properties using (*-distribʳ-+; *-assoc; +-assoc; +-comm; +-suc)open import Function.Base using (_∘_)open import Relation.Binary.PropositionalEquality using (_≡_; cong; cong₂; sym; module ≡-Reasoning) open ≡-Reasoning inner-assoc : ∀ m n o → o + (n + m * suc n) * suc o ≡ o + n * suc o + m * suc (o + n * suc o)inner-assoc m n o = begin o + (n + m * suc n) * suc o ≡⟨ cong (o +_) (begin (n + m * suc n) * suc o ≡⟨ *-distribʳ-+ (suc o) n (m * suc n) ⟩ n * suc o + m * suc n * suc o ≡⟨ cong (n * suc o +_) (*-assoc m (suc n) (suc o)) ⟩ n * suc o + m * suc (o + n * suc o) ∎) ⟩ o + (n * suc o + m * suc (o + n * suc o)) ≡⟨ +-assoc o _ _ ⟨ o + n * suc o + m * suc (o + n * suc o) ∎ private assoc-comm : ∀ a b c d → a + b + c + d ≡ (a + c) + (b + d) assoc-comm a b c d = begin a + b + c + d ≡⟨ cong (_+ d) (+-assoc a b c) ⟩ a + (b + c) + d ≡⟨ cong (λ z → a + z + d) (+-comm b c) ⟩ a + (c + b) + d ≡⟨ cong (_+ d) (+-assoc a c b) ⟨ (a + c) + b + d ≡⟨ +-assoc (a + c) b d ⟩ (a + c) + (b + d) ∎ assoc-comm′ : ∀ a b c d → a + (b + (c + d)) ≡ a + c + (b + d) assoc-comm′ a b c d = begin a + (b + (c + d)) ≡⟨ cong (a +_) (+-assoc b c d) ⟨ a + (b + c + d) ≡⟨ cong (λ z → a + (z + d)) (+-comm b c) ⟩ a + (c + b + d) ≡⟨ cong (a +_) (+-assoc c b d) ⟩ a + (c + (b + d)) ≡⟨ +-assoc a c _ ⟨ a + c + (b + d) ∎ assoc₁ : ∀ m n o → (2 + n + o) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)assoc₁ m n o = begin (2 + n + o) * (1 + m) ≡⟨ cong (_* (1 + m)) (assoc-comm 1 1 n o) ⟩ ((1 + n) + (1 + o)) * (1 + m) ≡⟨ *-distribʳ-+ (1 + m) (1 + n) (1 + o) ⟩ (1 + n) * (1 + m) + (1 + o) * (1 + m) ∎ assoc₂ : ∀ m n o → (1 + n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)assoc₂ m n o = *-distribʳ-+ (1 + m) (1 + n) (1 + o) assoc₃ : ∀ m n o → m + (n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))assoc₃ m n o = begin m + (n + (1 + o)) * (1 + m) ≡⟨ cong (m +_) (*-distribʳ-+ (1 + m) n (1 + o)) ⟩ m + (n * (1 + m) + (1 + o) * (1 + m)) ≡⟨ +-assoc m _ _ ⟨ (m + n * (1 + m)) + (1 + o) * (1 + m) ≡⟨ +-suc _ _ ⟩ (1 + n) * (1 + m) + (m + o * (1 + m)) ∎ assoc₄ : ∀ m n o → m + (1 + m + (n + o) * (1 + m)) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))assoc₄ m n o = begin m + (1 + m + (n + o) * (1 + m)) ≡⟨ +-suc _ _ ⟩ 1 + m + (m + (n + o) * (1 + m)) ≡⟨ cong (λ z → suc (m + (m + z))) (*-distribʳ-+ (suc m) n o) ⟩ 1 + m + (m + (n * (1 + m) + o * (1 + m))) ≡⟨ cong suc (assoc-comm′ m m _ _) ⟩ (1 + n) * (1 + m) + (m + o * (1 + m)) ∎