From 9e0f5d15f0521fa6bcd09f81b2e3666a051cf386 Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 23:24:32 -0700 Subject: [PATCH 1/8] =?UTF-8?q?Add=20m=E2=89=A20=E2=88=A7n=E2=89=A20?= =?UTF-8?q?=E2=87=92m*n=E2=89=A20=20to=20Data.Nat.Properties?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 5 +++++ src/Data/Nat/Properties.agda | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index d729b2b122..63a360a680 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -379,6 +379,11 @@ Other minor additions * `Data.Nat.Binary.Induction` now re-exports `Acc` and `acc` from `Induction.WellFounded`. +* Added new properties to `Data.Nat.Properties`: + ```agda + m≢0∧n≢0⇒m*n≢0 : m ≢ 0 → n ≢ 0 → m * n ≢ 0 + ``` + * Added new properties to `Data.Nat.Binary.Properties`: ```agda +-isSemigroup : IsSemigroup _+_ diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index afbbbfc7bb..e787b0ddef 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -839,6 +839,11 @@ m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0 m*n≡0⇒m≡0∨n≡0 zero {n} eq = inj₁ refl m*n≡0⇒m≡0∨n≡0 (suc m) {zero} eq = inj₂ refl +m≢0∧n≢0⇒m*n≢0 : ∀ {m n} → m ≢ 0 → n ≢ 0 → m * n ≢ 0 +m≢0∧n≢0⇒m*n≢0 {zero} {n} m≢0 n≢0 = contradiction refl m≢0 +m≢0∧n≢0⇒m*n≢0 {suc m} {zero} m≢0 n≢0 = contradiction refl n≢0 +m≢0∧n≢0⇒m*n≢0 {suc m} {suc n} m≢0 n≢0 = 1+n≢0 + m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1 m*n≡1⇒m≡1 (suc zero) n _ = refl m*n≡1⇒m≡1 (suc (suc m)) (suc zero) () From 7fc6065df5df90c340489ff384de50503523d44b Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 18:09:30 -0700 Subject: [PATCH 2/8] Add last and init to Data.Table.Base --- CHANGELOG.md | 7 +++++++ src/Data/Table/Base.agda | 6 ++++++ 2 files changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 63a360a680..527eac48c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -497,6 +497,13 @@ Other minor additions words : String → List String ``` +* Added definitions to `Data.Table.Base`: + ```agda + last : ∀ {n} → Table A (suc n) → A + init : ∀ {n} → Table A (suc n) → Table A n + ``` + + * Added new proofs to `Data.Tree.Binary.Properties`: ```agda map-compose : map (f₁ ∘ f₂) (g₁ ∘ g₂) ≗ map f₁ g₁ ∘ map f₂ g₂ diff --git a/src/Data/Table/Base.agda b/src/Data/Table/Base.agda index a7b282bd38..5b02d613bd 100644 --- a/src/Data/Table/Base.agda +++ b/src/Data/Table/Base.agda @@ -50,6 +50,12 @@ uncons t = head t , tail t remove : ∀ {n} → Fin (suc n) → Table A (suc n) → Table A n remove i t = tabulate (lookup t ∘ punchIn i) +last : ∀ {n} → Table A (suc n) → A +last {n = n} t = lookup t (fromℕ n) + +init : ∀ {n} → Table A (suc n) → Table A n +init t = tabulate (lookup t ∘ inject₁) + ------------------------------------------------------------------------ -- Operations for transforming tables From a861e3547136745f795b6353341f089e1cc71bf9 Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 18:15:16 -0700 Subject: [PATCH 3/8] Add several properties to Data.Fin.Properties --- CHANGELOG.md | 8 ++++++++ src/Data/Fin/Properties.agda | 27 +++++++++++++++++++++++++++ 2 files changed, 35 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 527eac48c8..f00c0e6895 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -262,6 +262,14 @@ Other minor additions splitAt-< : splitAt m {n} i ≡ inj₁ (fromℕ< i Date: Sat, 29 Aug 2020 18:17:36 -0700 Subject: [PATCH 4/8] Added left distribution to Algebra.Structures.IsSemiringWithoutOne --- CHANGELOG.md | 5 +++++ src/Algebra/Structures.agda | 2 ++ 2 files changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f00c0e6895..ba807c97bd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -240,6 +240,11 @@ Other minor additions IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1# ``` +* Added declarations to `Algebra.Structures.IsSemiringWithoutOne`: + ```agda + distribˡ : * DistributesOverˡ + + ``` + * Added new proof to `Data.Fin.Induction`: ```agda <-wellFounded : WellFounded _<_ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 4c2ce39da9..fd6343de69 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -313,6 +313,8 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where open IsNearSemiring isNearSemiring public hiding (+-isMonoid; zeroˡ; *-isSemigroup) + distribˡ : * DistributesOverˡ + + distribˡ = proj₁ distrib record IsCommutativeSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where From 0857b35448dc9e29a524e77aaaee1f29c9b634c7 Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 18:19:39 -0700 Subject: [PATCH 5/8] =?UTF-8?q?Added=20sum=E2=82=9C-init=20to=20Algebra.Pr?= =?UTF-8?q?operties.CommutativeMonoid?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 5 +++++ src/Algebra/Properties/CommutativeMonoid.agda | 18 ++++++++++++++++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ba807c97bd..0e2718163f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -240,6 +240,11 @@ Other minor additions IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1# ``` +* Added proofs to `Algebra.Properties.CommutativeMonoid`: + ```agda + sumₜ-init : sumₜ t ≈ sumₜ (init t) + lookup t (fromℕ n) + ``` + * Added declarations to `Algebra.Structures.IsSemiringWithoutOne`: ```agda distribˡ : * DistributesOverˡ + diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda index 19dafdcdd0..5a1ce083ac 100644 --- a/src/Algebra/Properties/CommutativeMonoid.agda +++ b/src/Algebra/Properties/CommutativeMonoid.agda @@ -19,10 +19,10 @@ open import Algebra.Solver.CommutativeMonoid M open import Relation.Binary as B using (_Preserves_⟶_) open import Function open import Function.Equality using (_⟨$⟩_) -open import Data.Product +open import Data.Product hiding (_×_) open import Data.Bool.Base using (Bool; true; false) open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Fin.Base using (Fin; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; fromℕ) open import Data.List.Base as List using ([]; _∷_) import Data.Fin.Properties as FP open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ˡ_; _⟨$⟩ʳ_) @@ -73,6 +73,20 @@ sumₜ-remove {suc n} {suc i} t′ = ∑t = sumₜ t ∑t′ = sumₜ (remove i t) +-- When summing over a function from a finite set, we can pull out last element + +sumₜ-init : ∀ {n} (t : Table Carrier (suc n)) → sumₜ t ≈ sumₜ (init t) + lookup t (fromℕ n) +sumₜ-init {zero} t = +-comm (lookup t zero) 0# +sumₜ-init {suc n} t = begin + t₀ + ∑t ≈⟨ +-congˡ (sumₜ-init (tail t)) ⟩ + t₀ + (∑t′ + tₗ) ≈˘⟨ +-assoc _ _ _ ⟩ + (t₀ + ∑t′) + tₗ ∎ + where + t₀ = head t + tₗ = last t + ∑t = sumₜ (tail t) + ∑t′ = sumₜ (tail (init t)) + -- '_≈_' is a congruence over 'sumTable n'. sumₜ-cong-≈ : ∀ {n} → sumₜ {n} Preserves _≋_ ⟶ _≈_ From 76763979d8051478b609e0f0ff424bf12822f5fc Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 18:46:53 -0700 Subject: [PATCH 6/8] Add Data.Fin.Combinatorics and Data.Nat.Combinatorics --- CHANGELOG.md | 6 +++ src/Data/Fin/Combinatorics.agda | 91 +++++++++++++++++++++++++++++++++ src/Data/Nat/Combinatorics.agda | 31 +++++++++++ 3 files changed, 128 insertions(+) create mode 100644 src/Data/Fin/Combinatorics.agda create mode 100644 src/Data/Nat/Combinatorics.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e2718163f..4d929efea7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -144,6 +144,12 @@ New modules Data.Nat.Binary.Subtraction ``` +* Combinatorics operations + ``` + Data.Fin.Combinatorics + Data.Nat.Combinatorics + ``` + * A predicate for vectors in which every pair of elements is related. ``` Data.Vec.Relation.Unary.AllPairs diff --git a/src/Data/Fin/Combinatorics.agda b/src/Data/Fin/Combinatorics.agda new file mode 100644 index 0000000000..24192b8854 --- /dev/null +++ b/src/Data/Fin/Combinatorics.agda @@ -0,0 +1,91 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Combinatorics operations +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Fin.Combinatorics where + +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; lower₁; _ℕ-ℕ_) +open import Data.Fin.Properties using (toℕ Date: Sat, 29 Aug 2020 18:49:15 -0700 Subject: [PATCH 7/8] Add Algebra.Properties.SemiringWithoutOne --- CHANGELOG.md | 5 ++ .../Properties/SemiringWithoutOne.agda | 61 +++++++++++++++++++ 2 files changed, 66 insertions(+) create mode 100644 src/Algebra/Properties/SemiringWithoutOne.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 4d929efea7..318d0185fc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -133,6 +133,11 @@ New modules Function.Identity.Instances ``` +* Algerbaic properties: + ```agda + Algebra.Properties.SemiringWithoutOne + ``` + * Predicate for lists that are sorted with respect to a total order ``` Data.List.Relation.Unary.Sorted.TotalOrder diff --git a/src/Algebra/Properties/SemiringWithoutOne.agda b/src/Algebra/Properties/SemiringWithoutOne.agda new file mode 100644 index 0000000000..3f25f2a275 --- /dev/null +++ b/src/Algebra/Properties/SemiringWithoutOne.agda @@ -0,0 +1,61 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some derivable properties +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles + +module Algebra.Properties.SemiringWithoutOne + {g₁ g₂} (M : SemiringWithoutOne g₁ g₂) where + +open SemiringWithoutOne M +open import Algebra.Definitions _≈_ +open import Algebra.Operations.CommutativeMonoid +-commutativeMonoid +open import Data.Nat.Base using (ℕ; suc; zero) +import Data.Fin.Base as Fin +open import Data.Fin.Base using (Fin; suc) +open import Data.Fin.Combinatorics using (_C_) +open import Relation.Binary.Reasoning.Setoid setoid + +*-distribˡ-∑ : ∀ n (f : Fin n → Carrier) x → x * (∑[ i < n ] f i) ≈ ∑[ i < n ] (x * (f i)) +*-distribˡ-∑ zero f x = zeroʳ x +*-distribˡ-∑ (suc n) f x = begin + (x * (f₀ + ∑f)) ≈⟨ distribˡ _ _ _ ⟩ + (x * f₀ + x * ∑f) ≈⟨ +-congˡ (*-distribˡ-∑ n _ _) ⟩ + (x * f₀ + ∑xf) ∎ + where + f₀ = f Fin.zero + ∑f = ∑[ i < n ] f (suc i) + ∑xf = ∑[ i < n ] (x * f (suc i)) + +*-distribʳ-∑ : ∀ n (f : Fin n → Carrier) x → (∑[ i < n ] f i) * x ≈ ∑[ i < n ] ((f i) * x) +*-distribʳ-∑ zero f x = zeroˡ x +*-distribʳ-∑ (suc n) f x = begin + ((f₀ + ∑f) * x) ≈⟨ distribʳ _ _ _ ⟩ + (f₀ * x + ∑f * x) ≈⟨ +-congˡ (*-distribʳ-∑ n _ _) ⟩ + (f₀ * x + ∑fx) ∎ + where + f₀ = f Fin.zero + ∑f = ∑[ i < n ] f (suc i) + ∑fx = ∑[ i < n ] (f (suc i) * x) + +×-comm : ∀ n x y → x * (n × y) ≈ n × (x * y) +×-comm zero x y = zeroʳ x +×-comm (suc n) x y = begin + x * (suc n × y) ≡⟨⟩ + x * (y + n × y) ≈⟨ distribˡ _ _ _ ⟩ + x * y + x * (n × y) ≈⟨ +-congˡ (×-comm n _ _) ⟩ + x * y + n × (x * y) ≡⟨⟩ + suc n × (x * y) ∎ + +×-assoc : ∀ n x y → (n × x) * y ≈ n × (x * y) +×-assoc zero x y = zeroˡ y +×-assoc (suc n) x y = begin + (suc n × x) * y ≡⟨⟩ + (x + n × x) * y ≈⟨ distribʳ _ _ _ ⟩ + x * y + (n × x) * y ≈⟨ +-congˡ (×-assoc n _ _) ⟩ + x * y + n × (x * y) ≡⟨⟩ + suc n × (x * y) ∎ From c645e5444e1a4808e6d961a9fc85c82e153f613c Mon Sep 17 00:00:00 2001 From: Maciej Piechotka Date: Sat, 29 Aug 2020 18:52:02 -0700 Subject: [PATCH 8/8] Add Algebra.Properties.CommutativeSemiring --- CHANGELOG.md | 1 + .../Properties/CommutativeSemiring.agda | 157 ++++++++++++++++++ 2 files changed, 158 insertions(+) create mode 100644 src/Algebra/Properties/CommutativeSemiring.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 318d0185fc..bcfb5671ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -135,6 +135,7 @@ New modules * Algerbaic properties: ```agda + Algebra.Properties.CommutativeSemiring Algebra.Properties.SemiringWithoutOne ``` diff --git a/src/Algebra/Properties/CommutativeSemiring.agda b/src/Algebra/Properties/CommutativeSemiring.agda new file mode 100644 index 0000000000..ca525ff223 --- /dev/null +++ b/src/Algebra/Properties/CommutativeSemiring.agda @@ -0,0 +1,157 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some basic properties of Rings +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +-- Disabled to prevent warnings from deprecated Table +{-# OPTIONS --warn=noUserWarning #-} + +open import Algebra + +module Algebra.Properties.CommutativeSemiring {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where + +open CommutativeSemiring R +open import Algebra.Properties.CommutativeMonoid +-commutativeMonoid +open import Algebra.Properties.SemiringWithoutOne semiringWithoutOne +open import Algebra.Operations.Semiring semiring + +import Data.Nat.Base as ℕ +open import Data.Nat.Base using (ℕ; suc) +import Data.Nat.Properties as ℕ +open import Data.Nat.Properties using (≤-refl) +import Data.Fin.Base as Fin +open import Data.Fin.Base using (Fin; fromℕ; toℕ; punchIn; lower₁; inject₁; _ℕ-ℕ_) +open import Data.Fin.Properties using (_≟_; toℕ[k]≡n⇒k≡fromℕ[n]; k≡fromℕ[n]⇒toℕ[k]≡n; toℕ-inject₁-≢; lower₁-inject₁′; suc-injective; lower₁-irrelevant; toℕ-lower₁) +open import Data.Fin.Combinatorics using (_C_; nCn≡1) +open import Data.Table.Base using (lookup; tabulate) + +open import Function using (_∘_) + +open import Relation.Binary.Reasoning.Setoid setoid +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) +open import Relation.Nullary using (yes; no) +open import Relation.Nullary.Negation using (contradiction) + +------------------------------------------------------------------------ +-- Properties of _^_ + +binomial : ∀ n x y → ((x + y) ^ n) ≈ ∑[ i < suc n ] ((n C i) × (x ^ toℕ i) * (y ^ (n ℕ-ℕ i))) +binomial ℕ.zero x y = begin + ((x + y) ^ 0) ≡⟨⟩ + 1# ≈˘⟨ *-identityʳ 1# ⟩ + (1# * 1#) ≈˘⟨ *-congʳ (+-identityʳ 1#) ⟩ + (1 × 1# * 1#) ≡⟨⟩ + (1 × (x ^ ℕ.zero) * (y ^ ℕ.zero)) ≈˘⟨ +-identityʳ _ ⟩ + ((0 C Fin.zero) × (x ^ ℕ.zero) * (y ^ ℕ.zero)) + 0# ≡⟨⟩ + (∑[ i < 1 ] ((0 C i) × (x ^ toℕ i) * (y ^ (0 ℕ-ℕ i)))) ∎ +binomial (suc n) x y = begin + ((x + y) ^ suc n) ≡⟨⟩ + (x + y) * (x + y) ^ n ≈⟨ *-congˡ (binomial n x y) ⟩ + (x + y) * ∑[ i < suc n ] bt n i ≈⟨ distribʳ _ _ _ ⟩ + x * ∑[ i < suc n ] bt n i + y * ∑[ i < suc n ] bt n i ≈⟨ +-cong lemma₃ lemma₄ ⟩ + ∑[ i < suc (suc n) ] bt₁ n i + ∑[ i < suc (suc n) ] bt₂ n i ≈˘⟨ ∑-distrib-+ _ (bt₁ n) (bt₂ n) ⟩ + ∑[ i < suc (suc n) ] (bt₁ n i + bt₂ n i) ≈⟨ sumₜ-cong-≈ lemma₈ ⟩ + ∑[ i < suc (suc n) ] bt (suc n) i ∎ + where + bt : (n : ℕ) → (k : Fin (suc n)) → Carrier + bt n k = ((n C k) × (x ^ toℕ k) * (y ^ (n ℕ-ℕ k))) + bt₁ : (n : ℕ) → (k : Fin (suc (suc n))) → Carrier + bt₁ n Fin.zero = 0# + bt₁ n (Fin.suc k) = x * bt n k + bt₂ : (n : ℕ) → (k : Fin (suc (suc n))) → Carrier + bt₂ n k with k ≟ fromℕ (suc n) + ... | yes k≡1+n = 0# + ... | no k≢1+n = y * bt n (lower₁ k (λ 1+n≡k → contradiction (toℕ[k]≡n⇒k≡fromℕ[n] (suc n) k (≡-sym 1+n≡k)) k≢1+n)) + bbt : (n : ℕ) → (k : Fin (suc n)) → Carrier + bbt n k = (x ^ toℕ k) * (y ^ (n ℕ-ℕ k)) + lemma₁ : ∀ k → y * bt n k ≈ bt₂ n (inject₁ k) + lemma₁ k with (inject₁ k) ≟ fromℕ (suc n) + ... | yes k≡1+n = contradiction (k≡fromℕ[n]⇒toℕ[k]≡n (suc n) (inject₁ k) k≡1+n) (toℕ-inject₁-≢ k ∘ ≡-sym) + ... | no k≢1+n = sym (reflexive (cong (λ h → y * bt n h) (lower₁-inject₁′ k _))) + lemma₂ : 0# ≈ bt₂ n (fromℕ (suc n)) + lemma₂ with fromℕ (suc n) ≟ fromℕ (suc n) + ... | yes 1+n≡1+n = refl + ... | no 1+n≢1+n = contradiction ≡-refl 1+n≢1+n + lemma₃ : x * ∑[ i < suc n ] bt n i ≈ ∑[ i < suc (suc n) ] bt₁ n i + lemma₃ = begin + (x * ∑[ i < suc n ] bt n i) ≈⟨ *-distribˡ-∑ (suc n) (bt n) x ⟩ + ∑[ i < suc n ] (x * bt n i) ≈˘⟨ +-identityˡ _ ⟩ + (0# + ∑[ i < suc n ] (x * bt n i)) ≡⟨⟩ + (0# + ∑[ i < suc n ] bt₁ n (punchIn Fin.zero i)) ≡⟨⟩ + (∑[ i < suc (suc n) ] bt₁ n i) ∎ + lemma₄ : y * ∑[ i < suc n ] bt n i ≈ ∑[ i < suc (suc n) ] bt₂ n i + lemma₄ = begin + (y * ∑[ i < suc n ] bt n i) ≈⟨ *-distribˡ-∑ (suc n) (bt n) y ⟩ + ∑[ i < suc n ] (y * bt n i) ≈˘⟨ +-identityʳ _ ⟩ + (∑[ i < suc n ] (y * bt n i) + 0#) ≈⟨ +-cong (sumₜ-cong-≈ lemma₁) lemma₂ ⟩ + ((∑[ i < suc n ] bt₂ n (inject₁ i)) + bt₂ n (fromℕ (suc n))) ≈˘⟨ sumₜ-init (tabulate (bt₂ n)) ⟩ + sumₜ (tabulate (bt₂ n)) ≡⟨⟩ + ∑[ i < suc (suc n) ] bt₂ n i ∎ + lemma₅ : ∀ k → x * bt n k ≈ (n C k) × bbt (suc n) (Fin.suc k) + lemma₅ k = begin + (x * bt n k) ≡⟨⟩ + (x * ((n C k) × x ^ toℕ k * y ^ (n ℕ-ℕ k))) ≈˘⟨ *-assoc x ((n C k) × x ^ toℕ k) (y ^ (n ℕ-ℕ k)) ⟩ + ((x * (n C k) × x ^ toℕ k) * y ^ (n ℕ-ℕ k)) ≈⟨ *-congʳ (×-comm (n C k) _ _) ⟩ + (((n C k) × x ^ toℕ (Fin.suc k)) * y ^ (suc n ℕ-ℕ Fin.suc k)) ≈⟨ ×-assoc (n C k) _ _ ⟩ + (n C k) × (x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k)) ≡⟨⟩ + (n C k) × bbt (suc n) (Fin.suc k) ∎ + lemma₆ : ∀ k 1+n≢1+k → y * bt n (lower₁ (Fin.suc k) 1+n≢1+k) ≈ (n C lower₁ (Fin.suc k) 1+n≢1+k) × bbt (suc n) (Fin.suc k) + lemma₆ k 1+n≢1+k = begin + (y * bt n 1+k) ≡⟨⟩ + (y * ((n C 1+k) × x ^ toℕ 1+k * y ^ (n ℕ-ℕ 1+k))) ≈⟨ *-comm _ _ ⟩ + (((n C 1+k) × x ^ toℕ 1+k * y ^ (n ℕ-ℕ 1+k)) * y) ≈⟨ *-assoc _ _ _ ⟩ + ((n C 1+k) × x ^ toℕ 1+k * (y ^ (n ℕ-ℕ 1+k) * y)) ≈⟨ *-congˡ (*-comm _ _) ⟩ + ((n C 1+k) × x ^ toℕ 1+k * y ^ suc (n ℕ-ℕ 1+k)) ≡⟨ cong (λ h → (n C 1+k) × x ^ h * y ^ suc (n ℕ-ℕ 1+k)) (toℕ-lower₁ (Fin.suc k) 1+n≢1+k) ⟩ + ((n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ suc (n ℕ-ℕ 1+k)) ≡⟨ cong (λ h → (n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ h) (1+[n-[1+k]]≡[1+n]-[1+k] n k 1+n≢1+k) ⟩ + ((n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k)) ≈⟨ ×-assoc (n C 1+k) _ _ ⟩ + ((n C 1+k) × (x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k))) ≡⟨⟩ + ((n C 1+k) × bbt (suc n) (Fin.suc k)) ∎ + where + 1+k = lower₁ (Fin.suc k) 1+n≢1+k + 1+[n-[1+k]]≡[1+n]-[1+k] : ∀ n k 1+n≢1+k → suc (n ℕ-ℕ lower₁ (Fin.suc k) 1+n≢1+k) ≡ suc n ℕ-ℕ Fin.suc k + 1+[n-[1+k]]≡[1+n]-[1+k] ℕ.zero Fin.zero 1+n≢1+k = contradiction ≡-refl 1+n≢1+k + 1+[n-[1+k]]≡[1+n]-[1+k] (suc n) Fin.zero 1+n≢1+k = ≡-refl + 1+[n-[1+k]]≡[1+n]-[1+k] (suc n) (Fin.suc k) 1+n≢1+k = 1+[n-[1+k]]≡[1+n]-[1+k] n k (1+n≢1+k ∘ cong suc) + lemma₇ : ∀ k 1+n≢1+k → n C k ℕ.+ n C (lower₁ (Fin.suc k) 1+n≢1+k) ≡ (suc n C Fin.suc k) + lemma₇ k 1+n≢1+k with suc n ℕ.≟ toℕ (Fin.suc k) + ... | yes 1+n≡1+k = contradiction 1+n≡1+k 1+n≢1+k + ... | no _ = cong (λ h → n C k ℕ.+ n C Fin.suc h) (lower₁-irrelevant k _ _) + lemma₈ : ∀ k → bt₁ n k + bt₂ n k ≈ bt (suc n) k + lemma₈ Fin.zero with Fin.zero ≟ fromℕ (suc n) + ... | yes () + ... | no 0≢1+n = begin + bt₁ n Fin.zero + bt₂ n Fin.zero ≡⟨⟩ + 0# + y * (1 × 1# * (y ^ n)) ≈⟨ +-identityˡ _ ⟩ + y * (1 × 1# * (y ^ n)) ≈˘⟨ *-assoc _ _ _ ⟩ + ((y * 1 × 1#) * y ^ n) ≈⟨ *-congʳ (*-comm _ _) ⟩ + ((1 × 1# * y) * y ^ n) ≈⟨ *-assoc _ _ _ ⟩ + (1 × 1# * (y * y ^ n)) ≡⟨⟩ + (1 × 1# * (y ^ suc n)) ≡⟨⟩ + bt (suc n) Fin.zero ∎ + lemma₈ (Fin.suc k) with Fin.suc k ≟ fromℕ (suc n) + ... | yes 1+k≡1+n = begin + (x * bt n k) + 0# ≈⟨ +-identityʳ _ ⟩ + (x * bt n k) ≡⟨ cong (λ h → x * bt n h) (suc-injective 1+k≡1+n) ⟩ + (x * bt n (fromℕ n)) ≡⟨⟩ + (x * ((n C fromℕ n) × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n)))) ≡⟨ cong (λ h → x * (h × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n)))) (nCn≡1 n) ⟩ + (x * (1 × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n)))) ≈⟨ *-congˡ (*-congʳ (+-identityʳ _)) ⟩ + (x * ((x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n)))) ≈˘⟨ *-assoc x _ _ ⟩ + (x * (x ^ toℕ (fromℕ n))) * (y ^ (n ℕ-ℕ fromℕ n)) ≈˘⟨ *-congʳ (+-identityʳ _) ⟩ + (1 × (x * (x ^ (toℕ (fromℕ n)))) * (y ^ (n ℕ-ℕ fromℕ n))) ≡˘⟨ cong (λ h → h × (x ^ toℕ (fromℕ (suc n))) * (y ^ (n ℕ-ℕ fromℕ n))) (nCn≡1 (suc n)) ⟩ + ((suc n C fromℕ (suc n)) × (x ^ toℕ (fromℕ (suc n))) * (y ^ (suc n ℕ-ℕ fromℕ (suc n)))) ≡⟨⟩ + bt (suc n) (fromℕ (suc n)) ≡˘⟨ cong (λ h → bt (suc n) h) 1+k≡1+n ⟩ + bt (suc n) (Fin.suc k) ∎ + ... | no 1+k≢1+n = begin + x * bt n k + y * bt n 1+k′ ≈⟨ +-cong (lemma₅ k) (lemma₆ k laux) ⟩ + (n C k) × bbt (suc n) (Fin.suc k) + (n C 1+k′) × bbt (suc n) (Fin.suc k) ≈˘⟨ ×-homo-+ (bbt (suc n) (Fin.suc k)) (n C k) (n C 1+k′) ⟩ + (n C k ℕ.+ n C 1+k′) × bbt (suc n) (Fin.suc k) ≡⟨ cong (λ h → h × (bbt (suc n) (Fin.suc k))) (lemma₇ k laux) ⟩ + (suc n C Fin.suc k) × bbt (suc n) (Fin.suc k) ≈˘⟨ ×-assoc (suc n C Fin.suc k) (x ^ toℕ (Fin.suc k)) (y ^ (suc n ℕ-ℕ Fin.suc k)) ⟩ + bt (suc n) (Fin.suc k) ∎ + where + laux : suc n ≢ toℕ (Fin.suc k) + laux 1+n≡1+k = contradiction (toℕ[k]≡n⇒k≡fromℕ[n] (suc n) (Fin.suc k) (≡-sym 1+n≡1+k)) 1+k≢1+n + 1+k′ : Fin (suc n) + 1+k′ = lower₁ (Fin.suc k) laux