From 33288963ff149e0b27aecd62d2f327c473988959 Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:02:11 +0100 Subject: [PATCH 01/11] divergence of sets - final version --- ArkLib/Data/CodingTheory/DivergenceOfSets.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean b/ArkLib/Data/CodingTheory/DivergenceOfSets.lean index b252e8836..b6ede0714 100644 --- a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean +++ b/ArkLib/Data/CodingTheory/DivergenceOfSets.lean @@ -1,5 +1,15 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import ArkLib.Data.CodingTheory.RelativeHammingDistance +/- +Proved definiton for divergence of an arbitrary set `U` from an arbitrary set `V`. +-/ + namespace DivergenceOfSets noncomputable section @@ -11,7 +21,7 @@ variable {ι : Type*} [Fintype ι] {U V C : Set (ι → F)} /-- -`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V` +`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V`. -/ def d_U [Nonempty ι] (U V : Set (ι → F)) : Set ℚ := { d : ℚ | ∃ u ∈ U, δᵣ(u,V) = d } @@ -26,7 +36,7 @@ lemma finite_d_U [Nonempty ι] : (d_U U V).Finite := Set.Finite.subset RelativeHamming.finite_relHammingDistRange d_U_subset_relHammingDistRange /-- -divergence of the arbitrary set `U` to the arbitrary set `V` +divergence of an arbitrary set `U` from an arbitrary set `V`. -/ def div_U_from_V [Nonempty ι] (U : Set (ι → F)) (V : Set (ι → F)) : ℚ := have : Fintype (d_U U V) := @Fintype.ofFinite _ finite_d_U From 2da095b5596401880fb1019744df6cf1b2dbe16c Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:13:57 +0100 Subject: [PATCH 02/11] Interleaved Codes - final version --- .../Data/CodingTheory/InterleavedCodes.lean | 36 ++++++++++++++----- 1 file changed, 27 insertions(+), 9 deletions(-) diff --git a/ArkLib/Data/CodingTheory/InterleavedCodes.lean b/ArkLib/Data/CodingTheory/InterleavedCodes.lean index c0dde66cc..38d6329db 100644 --- a/ArkLib/Data/CodingTheory/InterleavedCodes.lean +++ b/ArkLib/Data/CodingTheory/InterleavedCodes.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši +-/ + import Mathlib.Algebra.Module.Submodule.Defs import Mathlib.Data.Matrix.Defs import Mathlib.Data.Matrix.RowCol @@ -9,30 +15,39 @@ import ArkLib.Data.CodingTheory.LinearCodes import ArkLib.Data.CodingTheory.ReedSolomon import ArkLib.Data.CodingTheory.Prelims + open Classical LinearCodes noncomputable section +/- +Definition of a `κ`-interleaved code `IC` of a linear code `LC` over a semiring `F`. +Definition of distances for interleaved codes and statement for the relation between the minimal +distance of an interleaved code and its underlying linear code. +Statements of proximity results for Reed Solomon codes +(`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5` from Ligero) with proximity parameter less than +the minimal code distance divided by `3`. +-/ + variable {F : Type*} [Semiring F] {κ ι: ℕ} {LC : LinearCode ι F} namespace InterleavedCodes --- Question: in the abbrev, do we need to add the condition which makes a submodule of --- the given type an interleaved code? (it's in the def below) - -/-- - @KATY: Probably a bad name, I just followed the 'Submodule F (Fin ι → F)' for 'LinearCode' exmpl. - Feel free to either remove this altogether or name this better :). --/ abbrev MatrixSubmodule.{u} (κ ι : ℕ) (F : Type u) [Semiring F] : Type u := Submodule F (Matrix (Fin κ) (Fin ι) F) +/-- +The data needed to construct an interleaved code +-/ structure InterleavedCode (κ ι : ℕ) (F : Type*) [Semiring F] where MF : MatrixSubmodule κ ι F LC : LinearCode ι F +/-- +The condition making the InterleavedCode structure an interleaved code. +-/ def InterleavedCode.isInterleaved (IC : InterleavedCode κ ι F) := ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC @@ -46,10 +61,13 @@ def codeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : InterleavedCode κ ι F { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC } lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by sorry - + def lawfulInterleavedCodeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : LawfulInterleavedCode κ ι F := ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩ +/-- +distance between codewords `U` and `V` in a `κ`-interleaved code. + -/ def distCodewords (U V : Matrix (Fin κ) (Fin ι) F) : ℕ := (Matrix.neqCols U V).card @@ -62,7 +80,7 @@ def minDist (IC : MatrixSubmodule κ ι F) : ℕ := sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, distCodewords U V = d } /-- -`Δ IC` is the min distance of an interleaved code `IC` +`Δ IC` is the min distance of an interleaved code `IC`. -/ notation "Δ" IC => minDist IC From 8e44d7e9148a508017e9a081ebb1dd5552683215 Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:17:14 +0100 Subject: [PATCH 03/11] preliminary notions --- ArkLib/Data/CodingTheory/Prelims.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean index 0fec94527..c3e449376 100644 --- a/ArkLib/Data/CodingTheory/Prelims.lean +++ b/ArkLib/Data/CodingTheory/Prelims.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši +-/ + import Mathlib.Algebra.Module.Submodule.Defs import Mathlib.Data.Matrix.Defs import Mathlib.Data.Matrix.RowCol @@ -85,5 +91,3 @@ def line [Ring F] (u v : Fin ι → F) : Set (Fin ι → F) := {x | ∃ γ : F, x = γ • u + (1 - γ) • v} end Affine - -end From 0af744f46034023ce9b6b7c3617c1ba713bbf810 Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:19:01 +0100 Subject: [PATCH 04/11] preliminary notions, minor edits --- ArkLib/Data/CodingTheory/Prelims.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean index c3e449376..569ca764b 100644 --- a/ArkLib/Data/CodingTheory/Prelims.lean +++ b/ArkLib/Data/CodingTheory/Prelims.lean @@ -85,7 +85,7 @@ end Embedding namespace Affine /-- -Affine line between two vectors with coefficients in a semiring. +affine line between vectors `u` and `v`. -/ def line [Ring F] (u v : Fin ι → F) : Set (Fin ι → F) := {x | ∃ γ : F, x = γ • u + (1 - γ) • v} From e6a6d9e1975e17490cdb8a81091e46bebf4f4f0f Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:27:14 +0100 Subject: [PATCH 05/11] Proposed generalisation for RS codes defn: from a field F to a semiring F --- ArkLib/Data/CodingTheory/ReedSolomon.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/ArkLib/Data/CodingTheory/ReedSolomon.lean b/ArkLib/Data/CodingTheory/ReedSolomon.lean index 62f781e3a..22fe9d2db 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomon.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomon.lean @@ -17,7 +17,6 @@ import Mathlib.Data.FinEnum list-decoding. -/ - namespace ReedSolomon open Polynomial From 4a9262f85866c26810b9b39c2d76637fc0f4b4a9 Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Mon, 5 May 2025 16:27:42 +0100 Subject: [PATCH 06/11] relative Hamming dist - final --- .../CodingTheory/RelativeHammingDistance.lean | 23 +++++++++++++++---- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean b/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean index 084fbabc1..e60648659 100644 --- a/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean +++ b/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean @@ -1,6 +1,16 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import Mathlib.InformationTheory.Hamming import Mathlib.Analysis.Normed.Field.Lemmas +/-! +proved definitions of relative Hamming distance and related notions for a linear code `LC`, +including corner cases. +-/ open Classical variable {ι : Type*} [Fintype ι] @@ -23,7 +33,7 @@ section variable [Nonempty ι] /-- - relative Hamming distance between vectors `u` and `v` + relative Hamming distance between vectors `u` and `v`. -/ def dist (u v : ι → F) : ℚ := (hammingDist u v : ℚ) / (Fintype.card ι : ℚ) @@ -43,10 +53,13 @@ lemma zero_le_relHammingDist : 0 ≤ dist u v := by end /-- -`δᵣ(u,v)` denotes the relative Hamming distance between vectors `u` and `v` +`δᵣ(u,v)` denotes the relative Hamming distance between vectors `u` and `v`. -/ notation "δᵣ(" u ", " v ")" => dist u v +/-- +the range of the relative Hamming distance function. +-/ def distRange (ι : Type*) [Fintype ι] : Set ℚ := { d : ℚ | ∃ d' : ℕ, d' ≤ Fintype.card ι ∧ d = d' / Fintype.card ι } @@ -72,7 +85,7 @@ lemma finite_relHammingDistRange [Nonempty ι] : (distRange ι).Finite := by lemma finite_offDiag [Finite F] : C.offDiag.Finite := Set.Finite.offDiag (Set.toFinite _) /-- -The set of possible distances between distinct codewords of `C` +The set of possible distances between distinct codewords of `C`. -/ def d_C (C : Set (ι → F)) : Set ℚ := { d : ℚ | ∃ p ∈ Set.offDiag C, δᵣ(p.1, p.2) = d } @@ -90,7 +103,7 @@ lemma finite_d_C [Nonempty ι] : (d_C C).Finite := end /-- -relative Hamming Distance of a code C over a semiring F +relative Hamming Distance of a code `C`. -/ def minDistCode [Nonempty ι] (C : Set (ι → F)) : ℚ := have : Fintype (d_C C) := @Fintype.ofFinite _ finite_d_C @@ -120,7 +133,7 @@ lemma finite_d_w [Nonempty ι] : (d_w w C).Finite := instance [Nonempty ι] : Fintype (d_w w C) := @Fintype.ofFinite _ finite_d_w /-- -relative Hamming distance between a vector `w` and a code `C` +relative Hamming distance between a vector `w` and a code `C`. -/ def distToCode [Nonempty ι] (w : ι → F) (C : Set (ι → F)) : ℚ := if h : (d_w w C).Nonempty From a5873d6b1d5e38b1c09e0f791b08e7856a6ae2dc Mon Sep 17 00:00:00 2001 From: Katy Hristova Date: Tue, 6 May 2025 11:42:03 +0100 Subject: [PATCH 07/11] linear codes defs and lemmas --- ArkLib/Data/CodingTheory/LinearCodes.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/ArkLib/Data/CodingTheory/LinearCodes.lean b/ArkLib/Data/CodingTheory/LinearCodes.lean index 4376c47fd..2f8f7a2f4 100644 --- a/ArkLib/Data/CodingTheory/LinearCodes.lean +++ b/ArkLib/Data/CodingTheory/LinearCodes.lean @@ -1,9 +1,22 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import Mathlib.Data.Matrix.Rank import Mathlib.InformationTheory.Hamming import Mathlib.LinearAlgebra.Matrix.ToLin import Mathlib.Algebra.Module.Submodule.Range import Mathlib.Algebra.Module.Submodule.Defs +/-! + Definition of a linear code, minimal distance of a linear code, length, dimension and rate. + Linear codes defined by a generator matrices and rephrase of dimension in this framework. + Definition of the weight of a vector, statement and proof of the fact that the minimal + distance of a linear code equals the minimal weight taken over the set of codewords. +-/ + open Classical open Finset @@ -76,6 +89,9 @@ lemma minDist_eq_minWtCodewords {LC : LinearCode ι F} : minDist LC = minWtCodew refine congrArg _ (Set.ext fun _ ↦ ⟨fun ⟨u, _, v, _⟩ ↦ ⟨u - v, ?p₁⟩, fun _ ↦ ⟨0, ?p₂⟩⟩) <;> aesop (add simp [hammingDist_eq_wt_sub, sub_eq_zero]) +/-- +Singleton Bound Theorem. +-/ theorem singletonBound (LC : LinearCode ι F) : dim LC ≤ length LC - minDist LC + 1 := by sorry From e1e0b2a88d03e950acb4aae64cd7935e00ab7485 Mon Sep 17 00:00:00 2001 From: Frantisek Silvasi Date: Tue, 6 May 2025 15:43:47 +0200 Subject: [PATCH 08/11] Cleanup RS lemmas, introduce auxiliary lemmas and definitions. --- .../Data/CodingTheory/ReedSolomonCodes.lean | 169 +++++++++--------- 1 file changed, 84 insertions(+), 85 deletions(-) diff --git a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean index 20df0a691..1d412510a 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean @@ -13,11 +13,17 @@ variable {ι : ℕ} noncomputable section namespace Vandermonde + /-- A non-square Vandermonde matrix. -/ def nonsquare [Semiring F] (deg : ℕ) (α : Fin ι ↪ F) : Matrix (Fin ι) (Fin deg) F := - Matrix.of (fun i j => (α i) ^ j.1) + Matrix.of fun i j => (α i) ^ j.1 + +lemma nonsquare_mulVecLin [CommSemiring F] + {deg : ℕ} {α₁ : Fin ι ↪ F} {α₂ : Fin deg → F} {i : Fin ι} : + (nonsquare deg α₁).mulVecLin α₂ i = ∑ x, α₂ x * α₁ i ^ (↑x : ℕ) := by + simp [nonsquare, Matrix.mulVecLin_apply, Matrix.mulVec_eq_sum] /-- The transpose of a non-square Vandermonde matrix. @@ -79,96 +85,86 @@ lemma rank_nonsquare_rows_eq_min [CommRing F] [IsDomain F] {deg : ℕ} {α : Fin aesop (add simp [rank_nonsquare_eq_deg_of_ι_le, rank_nonsquare_eq_deg_of_deg_le]) (add safe forward le_of_lt) -theorem eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials +theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials {deg : ℕ} [CommRing F] {v : Fin ι ↪ F} {p : F[X]} (h_deg : p.natDegree ≤ deg) : (Vandermonde.nonsquare (deg + 1) v).mulVecLin (p.coeff ∘ Fin.val) = - (fun i => (p.eval (v i))) := by - rw [Matrix.mulVecLin_apply] - unfold Matrix.mulVec Vandermonde.nonsquare dotProduct - simp only [Matrix.of_apply, Function.comp_apply] - funext i - rw [Polynomial.eval_eq_sum, sum_def] - apply Eq.symm - apply Finset.sum_of_injOn (Fin.ofNat' (deg + 1)) - · unfold Set.InjOn - intro x₁ h₁ x₂ h₂ h - have h₁' : x₁ < deg + 1 := by - have := Polynomial.le_natDegree_of_mem_supp _ h₁ - linarith - have h₂' : x₂ < deg + 1 := by - have := Polynomial.le_natDegree_of_mem_supp _ h₂ - linarith - have : (Fin.ofNat' (deg + 1) x₁ : ℕ) = (Fin.ofNat' (deg + 1) x₁ : ℕ) := by rfl - rw (occs := .pos [2]) [h] at this - rw [Fin.val_ofNat', Fin.val_ofNat', Nat.mod_eq_of_lt h₁', Nat.mod_eq_of_lt h₂'] at this - exact this - · unfold Set.MapsTo - intros x h - simp - · intros i _ h - simp only [Fin.ofNat'_eq_cast, Set.mem_image, Finset.mem_coe, mem_support_iff, ne_eq, - not_exists, not_and] at h - specialize h i.val - simp only [Fin.cast_val_eq_self, not_true_eq_false, imp_false, Decidable.not_not] at h - rw [h, mul_zero] - · intros i h - rw [Fin.val_ofNat'] - have : i < deg + 1 := by - apply lt_of_le_of_lt (Polynomial.le_natDegree_of_mem_supp i h) - linarith - rw [Nat.mod_eq_of_lt this] - ring + fun i => p.eval (v i) := by + ext i + simp only [ + nonsquare_mulVecLin, Finset.sum_fin_eq_sum_range, eval_eq_sum + ] + refine Eq.symm (Finset.sum_of_injOn (·%(deg + 1)) ?p₁ ?p₂ (fun i _ h ↦ ?p₃) (fun i _ ↦ ?p₄)) + · aesop (add simp [Set.InjOn]) + (add safe forward [Polynomial.le_natDegree_of_mem_supp, le_trans, Nat.lt_add_one_of_le]) + (add 10% apply (show ∀ {a b c : ℕ}, a < c → b < c → a % c = b % c → a = b from + fun h₁ h₂ ↦ by aesop (add simp Nat.mod_eq_of_lt))) + (erase simp mem_support_iff) + · aesop (add simp Set.MapsTo) (add safe apply Nat.mod_lt) + · aesop (add safe (by specialize h i)) (add simp Nat.mod_eq_of_lt) + · have : i < deg + 1 := by aesop (add safe forward Polynomial.le_natDegree_of_mem_supp) + (erase simp mem_support_iff) + (add safe (by omega)) + aesop (add simp Nat.mod_eq_of_lt) (add safe (by ring)) end Vandermonde namespace ReedSolomonCode -lemma degree_lt [Semiring F] {p : F[X]} {deg : ℕ} [NeZero deg] : - (∀ i, i ≥ deg → p.coeff i = 0) → p.natDegree < deg := by - intro h - by_contra! h' - specialize h p.natDegree h' - simp_all only - [ - coeff_natDegree, leadingCoeff_eq_zero, natDegree_zero, - nonpos_iff_eq_zero, neZero_zero_iff_false - ] +lemma natDegree_lt_of_lbounded_zero_coeff [Semiring F] {p : F[X]} {deg : ℕ} [NeZero deg] + (h : ∀ i, deg ≤ i → p.coeff i = 0) : p.natDegree < deg := by + aesop (add unsafe [(by by_contra), (by specialize h p.natDegree)]) -lemma exists_poly_of_coeffs [Semiring F] (deg : ℕ) [NeZero deg] (coeffs : Fin deg → F) : - ∃ p : F[X], coeffs = p.coeff ∘ Fin.val ∧ p.natDegree < deg := by - have : Function.Injective (Fin.val : Fin deg → ℕ) := by - unfold Function.Injective - aesop - let support := Finset.map ⟨Fin.val, this⟩ (Finset.filter (fun i ↦ coeffs i ≠ 0) Finset.univ) - let p : F[X] := - ⟨ - support, - fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, - by - dsimp [support] - intros a - simp_all only - [ - Finset.mem_map, Finset.mem_filter, Finset.mem_univ, - true_and, Function.Embedding.coeFn_mk, - dite_eq_right_iff, not_forall, support - ] - apply Iff.intro - · intro a_1 - obtain ⟨w, h⟩ := a_1 - obtain ⟨left, right⟩ := h - subst right - simp_all only [Fin.eta, not_false_eq_true, Fin.is_lt, exists_const, support] - · intro a_1 - obtain ⟨w, h⟩ := a_1 - exists ⟨a, w⟩ - ⟩ - exists p - simp only [coeff_ofFinsupp, Finsupp.coe_mk, support, p] - apply And.intro - · aesop - · apply degree_lt; aesop +def polynomialOfCoeffs [Semiring F] {deg : ℕ} [NeZero deg] (coeffs : Fin deg → F) : F[X] := + ⟨ + Finset.map ⟨Fin.val, Fin.val_injective⟩ {i | coeffs i ≠ 0}, + fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, + fun a ↦ by aesop (add safe (by existsi a)) + (add simp [Fin.natCast_def, Nat.mod_eq_of_lt]) + ⟩ + +lemma natDegree_polynomialOfCoeffs_deg_lt_deg + [Semiring F] {deg : ℕ} [NeZero deg] {coeffs : Fin deg → F} : + (polynomialOfCoeffs coeffs).natDegree < deg := by + aesop (add simp polynomialOfCoeffs) + (add safe apply natDegree_lt_of_lbounded_zero_coeff) + +lemma coeff_polynomialOfCoeffs_eq_coeffs + [Semiring F] {deg : ℕ} [NeZero deg] {coeffs : Fin deg → F} : + (polynomialOfCoeffs coeffs).coeff ∘ Fin.val = coeffs:= by -- NOTE TO SELF: `liftF' coeffs`! + aesop (add simp polynomialOfCoeffs) + +-- lemma exists_poly_of_coeffs [Semiring F] (deg : ℕ) [NeZero deg] (coeffs : Fin deg → F) : +-- ∃ p : F[X], coeffs = p.coeff ∘ Fin.val ∧ p.natDegree < deg := by +-- let p : F[X] := +-- ⟨ +-- Finset.map ⟨Fin.val, Fin.val_injective⟩ {i | coeffs i ≠ 0}, +-- fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, -- NOTE TO SELF: Use `liftF` I implemented +-- -- in some of the BW cleanups? +-- by +-- dsimp +-- intros a +-- simp_all only +-- [ +-- Finset.mem_map, Finset.mem_filter, Finset.mem_univ, +-- true_and, Function.Embedding.coeFn_mk, +-- dite_eq_right_iff, not_forall +-- ] +-- apply Iff.intro +-- · intro a_1 +-- obtain ⟨w, h⟩ := a_1 +-- obtain ⟨left, right⟩ := h +-- subst right +-- simp_all only [Fin.eta, not_false_eq_true, Fin.is_lt, exists_const,] +-- · intro a_1 +-- obtain ⟨w, h⟩ := a_1 +-- exists ⟨a, w⟩ +-- ⟩ +-- exists p +-- simp only [coeff_ofFinsupp, Finsupp.coe_mk, support, p] +-- apply And.intro +-- · aesop +-- · apply natDegree_lt_of_lbounded_zero_coeff; aesop /-- The generator matrix of a Reed-Solomon code is a Vandermonde matrix. @@ -182,8 +178,11 @@ lemma genMatIsVandermonde [Field F] {deg : ℕ} [inst : NeZero deg] (α : Fin ι · intros h rw [LinearMap.mem_range] at h rcases h with ⟨coeffs, h⟩ - rcases exists_poly_of_coeffs deg coeffs with ⟨p, h', p_deg⟩ - rw [h'] at h + let p := polynomialOfCoeffs coeffs + have p_deg : p.natDegree < deg := natDegree_polynomialOfCoeffs_deg_lt_deg + have h' : p.coeff ∘ Fin.val = coeffs := coeff_polynomialOfCoeffs_eq_coeffs + -- rcases exists_poly_of_coeffs deg coeffs with ⟨p, h', p_deg⟩ + rw [←h'] at h match deg_def : deg with | .zero => aesop | deg + 1 => @@ -213,7 +212,7 @@ lemma genMatIsVandermonde [Field F] {deg : ℕ} [inst : NeZero deg] (α : Fin ι | .zero => aesop | deg + 1 => rw [Polynomial.mem_degreeLT] at h - rw [Vandermonde.eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials, ←h.2] + rw [Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials, ←h.2] unfold ReedSolomon.evalOnPoints simp only [LinearMap.coe_mk, AddHom.coe_mk] by_cases p_ne_zero : p ≠ 0 From f54f0b6b320cbc0cc218e6227b1483c43a34d735 Mon Sep 17 00:00:00 2001 From: Frantisek Silvasi Date: Wed, 7 May 2025 14:07:44 +0200 Subject: [PATCH 09/11] minDist - basic proof sketch --- ArkLib/Data/CodingTheory/ReedSolomonCodes.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean index 1d412510a..d57bdfe11 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean @@ -254,8 +254,15 @@ lemma rate [Field F] {deg : ℕ} [NeZero deg] {α : Fin ι ↪ F} (h : deg ≤ /-- The minimal code distance of a Reed-Solomon given by the degree and domain size. -/ -lemma minDist [Field F] {deg : ℕ} {α : Fin ι ↪ F} : - LinearCodes.minDist (ReedSolomon.code α deg) = ι - deg + 1 := by sorry +lemma minDist [Field F] {deg : ℕ} {α : Fin ι ↪ F} [NeZero deg] (h : deg ≤ ι) : + LinearCodes.minDist (ReedSolomon.code α deg) = ι - deg + 1 := by + have : NeZero ι := by constructor; aesop + refine le_antisymm ?p₁ ?p₂ + case p₁ => sorry + case p₂ => + choose c hc using show ∃ c, c ∈ ReedSolomon.code α deg by sorry + let p := polynomialOfCoeffs c + sorry From 47794952a45586e9280b9076d9fe9edc2a8069ea Mon Sep 17 00:00:00 2001 From: Frantisek Silvasi Date: Thu, 8 May 2025 12:05:59 +0200 Subject: [PATCH 10/11] auxiliary lemmas and definitions, clenup proofs --- .../Data/CodingTheory/ReedSolomonCodes.lean | 178 ++++++------------ 1 file changed, 61 insertions(+), 117 deletions(-) diff --git a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean index d57bdfe11..58a7d5f7c 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean @@ -86,36 +86,42 @@ lemma rank_nonsquare_rows_eq_min [CommRing F] [IsDomain F] {deg : ℕ} {α : Fin (add safe forward le_of_lt) theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials - {deg : ℕ} [CommRing F] {v : Fin ι ↪ F} - {p : F[X]} (h_deg : p.natDegree ≤ deg) : - (Vandermonde.nonsquare (deg + 1) v).mulVecLin (p.coeff ∘ Fin.val) = + {deg : ℕ} [NeZero deg] [CommRing F] {v : Fin ι ↪ F} + {p : F[X]} (h_deg : p.natDegree < deg) : + (Vandermonde.nonsquare deg v).mulVecLin (p.coeff ∘ Fin.val) = -- NOTE: Use `liftF`. fun i => p.eval (v i) := by ext i simp only [ nonsquare_mulVecLin, Finset.sum_fin_eq_sum_range, eval_eq_sum ] - refine Eq.symm (Finset.sum_of_injOn (·%(deg + 1)) ?p₁ ?p₂ (fun i _ h ↦ ?p₃) (fun i _ ↦ ?p₄)) + refine Eq.symm (Finset.sum_of_injOn (·%deg) ?p₁ ?p₂ (fun i _ h ↦ ?p₃) (fun i _ ↦ ?p₄)) · aesop (add simp [Set.InjOn]) - (add safe forward [Polynomial.le_natDegree_of_mem_supp, le_trans, Nat.lt_add_one_of_le]) + (add safe forward [le_natDegree_of_mem_supp, lt_of_le_of_lt, Nat.lt_add_one_of_le]) (add 10% apply (show ∀ {a b c : ℕ}, a < c → b < c → a % c = b % c → a = b from fun h₁ h₂ ↦ by aesop (add simp Nat.mod_eq_of_lt))) (erase simp mem_support_iff) - · aesop (add simp Set.MapsTo) (add safe apply Nat.mod_lt) + · aesop (add simp Set.MapsTo) (add safe apply Nat.mod_lt) (add 1% cases Nat) · aesop (add safe (by specialize h i)) (add simp Nat.mod_eq_of_lt) - · have : i < deg + 1 := by aesop (add safe forward Polynomial.le_natDegree_of_mem_supp) - (erase simp mem_support_iff) - (add safe (by omega)) + · have : i < deg := by aesop (add safe forward le_natDegree_of_mem_supp) + (erase simp mem_support_iff) + (add safe (by omega)) aesop (add simp Nat.mod_eq_of_lt) (add safe (by ring)) end Vandermonde namespace ReedSolomonCode -lemma natDegree_lt_of_lbounded_zero_coeff [Semiring F] {p : F[X]} {deg : ℕ} [NeZero deg] +section + +variable [Semiring F] {p : F[X]} + {deg : ℕ} [NeZero deg] + {coeffs : Fin deg → F} + +lemma natDegree_lt_of_lbounded_zero_coeff (h : ∀ i, deg ≤ i → p.coeff i = 0) : p.natDegree < deg := by aesop (add unsafe [(by by_contra), (by specialize h p.natDegree)]) -def polynomialOfCoeffs [Semiring F] {deg : ℕ} [NeZero deg] (coeffs : Fin deg → F) : F[X] := +def polynomialOfCoeffs (coeffs : Fin deg → F) : F[X] := ⟨ Finset.map ⟨Fin.val, Fin.val_injective⟩ {i | coeffs i ≠ 0}, fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, @@ -123,138 +129,76 @@ def polynomialOfCoeffs [Semiring F] {deg : ℕ} [NeZero deg] (coeffs : Fin deg (add simp [Fin.natCast_def, Nat.mod_eq_of_lt]) ⟩ -lemma natDegree_polynomialOfCoeffs_deg_lt_deg - [Semiring F] {deg : ℕ} [NeZero deg] {coeffs : Fin deg → F} : - (polynomialOfCoeffs coeffs).natDegree < deg := by +@[simp] +lemma natDegree_polynomialOfCoeffs_deg_lt_deg : (polynomialOfCoeffs coeffs).natDegree < deg := by aesop (add simp polynomialOfCoeffs) (add safe apply natDegree_lt_of_lbounded_zero_coeff) -lemma coeff_polynomialOfCoeffs_eq_coeffs - [Semiring F] {deg : ℕ} [NeZero deg] {coeffs : Fin deg → F} : - (polynomialOfCoeffs coeffs).coeff ∘ Fin.val = coeffs:= by -- NOTE TO SELF: `liftF' coeffs`! +@[simp] +lemma degree_polynomialOfCoeffs_deg_lt_deg : (polynomialOfCoeffs coeffs).degree < deg := by + aesop (add simp [polynomialOfCoeffs, degree_lt_iff_coeff_zero]) + +@[simp] +lemma coeff_polynomialOfCoeffs_eq_coeffs : + (polynomialOfCoeffs coeffs).coeff ∘ Fin.val = coeffs := by -- NOTE TO SELF: `liftF' coeffs`! aesop (add simp polynomialOfCoeffs) --- lemma exists_poly_of_coeffs [Semiring F] (deg : ℕ) [NeZero deg] (coeffs : Fin deg → F) : --- ∃ p : F[X], coeffs = p.coeff ∘ Fin.val ∧ p.natDegree < deg := by --- let p : F[X] := --- ⟨ --- Finset.map ⟨Fin.val, Fin.val_injective⟩ {i | coeffs i ≠ 0}, --- fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, -- NOTE TO SELF: Use `liftF` I implemented --- -- in some of the BW cleanups? --- by --- dsimp --- intros a --- simp_all only --- [ --- Finset.mem_map, Finset.mem_filter, Finset.mem_univ, --- true_and, Function.Embedding.coeFn_mk, --- dite_eq_right_iff, not_forall --- ] --- apply Iff.intro --- · intro a_1 --- obtain ⟨w, h⟩ := a_1 --- obtain ⟨left, right⟩ := h --- subst right --- simp_all only [Fin.eta, not_false_eq_true, Fin.is_lt, exists_const,] --- · intro a_1 --- obtain ⟨w, h⟩ := a_1 --- exists ⟨a, w⟩ --- ⟩ --- exists p --- simp only [coeff_ofFinsupp, Finsupp.coe_mk, support, p] --- apply And.intro --- · aesop --- · apply natDegree_lt_of_lbounded_zero_coeff; aesop +@[simp] +lemma polynomialOfCoeffs_mem_degreeLT : polynomialOfCoeffs coeffs ∈ degreeLT F deg := by + aesop (add simp Polynomial.mem_degreeLT) + +lemma natDegree_lt_of_mem_degreeLT (h : p ∈ degreeLT F deg) : p.natDegree < deg := by + by_cases p = 0 + · cases deg <;> aesop + · aesop (add simp [natDegree_lt_iff_degree_lt, mem_degreeLT]) + +end + +section + +variable {deg : ℕ} [Field F] {α : Fin ι ↪ F} /-- The generator matrix of a Reed-Solomon code is a Vandermonde matrix. -/ -lemma genMatIsVandermonde [Field F] {deg : ℕ} [inst : NeZero deg] (α : Fin ι ↪ F) : +lemma genMatIsVandermonde [NeZero deg] : LinearCodes.genMat_mul (Vandermonde.nonsquare deg α) = ReedSolomon.code α deg := by unfold LinearCodes.genMat_mul ReedSolomon.code - apply Submodule.ext - intros x - apply Iff.intro - · intros h - rw [LinearMap.mem_range] at h - rcases h with ⟨coeffs, h⟩ - let p := polynomialOfCoeffs coeffs - have p_deg : p.natDegree < deg := natDegree_polynomialOfCoeffs_deg_lt_deg - have h' : p.coeff ∘ Fin.val = coeffs := coeff_polynomialOfCoeffs_eq_coeffs - -- rcases exists_poly_of_coeffs deg coeffs with ⟨p, h', p_deg⟩ - rw [←h'] at h - match deg_def : deg with - | .zero => aesop - | deg + 1 => - rw [Vandermonde.eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials (by linarith)] at h - rw [←h, Submodule.mem_map] - exists p - apply And.intro - · rw [Polynomial.mem_degreeLT] - by_cases p_ne_zero : p ≠ 0 - · rw - [ - Polynomial.degree_eq_natDegree p_ne_zero, - Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe - ] - exact p_deg - · simp only [ne_eq, Decidable.not_not] at p_ne_zero - rw [p_ne_zero, Polynomial.degree_zero, Nat.cast_withBot] - simp - decide - · simp only [ReedSolomon.evalOnPoints, LinearMap.coe_mk, AddHom.coe_mk] - · intros h - rw [Submodule.mem_map] at h - rcases h with ⟨p, h⟩ - rw [LinearMap.mem_range] - exists (p.coeff ∘ Fin.val) - match def_def : deg with - | .zero => aesop - | deg + 1 => - rw [Polynomial.mem_degreeLT] at h - rw [Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials, ←h.2] - unfold ReedSolomon.evalOnPoints - simp only [LinearMap.coe_mk, AddHom.coe_mk] - by_cases p_ne_zero : p ≠ 0 - · rw - [ - Polynomial.degree_eq_natDegree p_ne_zero, - Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe - ] at h - linarith - · aesop + ext x; rw [LinearMap.mem_range, Submodule.mem_map] + refine ⟨ + fun ⟨coeffs, h⟩ ↦ ⟨polynomialOfCoeffs coeffs, h.symm ▸ ?p₁⟩, + fun ⟨p, h⟩ ↦ ⟨p.coeff ∘ Fin.val, ?p₂⟩ + ⟩ + · rw [ + ←coeff_polynomialOfCoeffs_eq_coeffs (coeffs := coeffs), + Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials (by simp) + ] + simp [ReedSolomon.evalOnPoints] + · exact h.2 ▸ Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials + (natDegree_lt_of_mem_degreeLT h.1) -- for RS codes we know `deg ≤ ι ≤ |F|`. `ι ≤ |F|` is clear from the embedding. -- Check : is `deg ≤ ι` implemented in Quang's defn? Answer: not explicitly. Worth mentioning?? -/-- -The dimension of a Reed-Solomon code is the maximal degree of the polynomials. --/ -lemma dim_eq_deg [Field F] {deg : ℕ} [NeZero deg] {α : Fin ι ↪ F} (h : deg ≤ ι) : +lemma dim_eq_deg [NeZero deg] (h : deg ≤ ι) : LinearCodes.dim (ReedSolomon.code α deg) = deg := by rw [←genMatIsVandermonde, ←LinearCodes.dimEqRankGenMat] aesop -/-- -The length of a Reed-Solomon code is the domain size. --/ -lemma length_eq_domain_size [Field F] {deg : ℕ} {α : Fin ι ↪ F} : +@[simp] +lemma length_eq_domain_size : LinearCodes.length (ReedSolomon.code α deg) = ι := by - rw[LinearCodes.length] + rw [LinearCodes.length] simp -/-- -The rate of a Reed-Solomon code. --/ -lemma rate [Field F] {deg : ℕ} [NeZero deg] {α : Fin ι ↪ F} (h : deg ≤ ι) : +lemma rate [NeZero deg] (h : deg ≤ ι) : LinearCodes.rate (ReedSolomon.code α deg) = deg / ι := by - rw[LinearCodes.rate, dim_eq_deg, length_eq_domain_size] - exact h + rwa [LinearCodes.rate, dim_eq_deg, length_eq_domain_size] /-- The minimal code distance of a Reed-Solomon given by the degree and domain size. -/ -lemma minDist [Field F] {deg : ℕ} {α : Fin ι ↪ F} [NeZero deg] (h : deg ≤ ι) : +lemma minDist [NeZero deg] (h : deg ≤ ι) : LinearCodes.minDist (ReedSolomon.code α deg) = ι - deg + 1 := by have : NeZero ι := by constructor; aesop refine le_antisymm ?p₁ ?p₂ @@ -264,7 +208,7 @@ lemma minDist [Field F] {deg : ℕ} {α : Fin ι ↪ F} [NeZero deg] (h : deg let p := polynomialOfCoeffs c sorry - +end end ReedSolomonCode end From bacd8e186e5a37d9097eccedb971d0a50d5dff28 Mon Sep 17 00:00:00 2001 From: Frantisek Silvasi Date: Fri, 9 May 2025 12:57:11 +0200 Subject: [PATCH 11/11] minor cleanup --- ArkLib/Data/CodingTheory/ReedSolomonCodes.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean index 58a7d5f7c..08aff9394 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean @@ -183,7 +183,7 @@ lemma genMatIsVandermonde [NeZero deg] : lemma dim_eq_deg [NeZero deg] (h : deg ≤ ι) : LinearCodes.dim (ReedSolomon.code α deg) = deg := by rw [←genMatIsVandermonde, ←LinearCodes.dimEqRankGenMat] - aesop + simpa @[simp] lemma length_eq_domain_size :