Coding theory basic proofs

ArkLib/Data/CodingTheory/Basic.lean

@@ -47,7 +47,6 @@ notation "‖" u "‖₀" => hammingNorm u
 
 /-- The Hamming distance of a code `C` is the minimum Hamming distance between any two distinct
   elements of the code.
-cd
 We formalize this as the infimum `sInf` over all `d : ℕ` such that there exist `u v : n → R` in the
 code with `u ≠ v` and `hammingDist u v ≤ d`. If none exists, then we define the distance to be `0`.
 -/
@@ -189,12 +188,121 @@ theorem codeDist'_subsingleton [Subsingleton C] : ‖C‖₀' = ⊤ := by
 theorem dist'_eq_dist : ‖C‖₀'.toNat = ‖C‖₀ := by
   by_cases h : Subsingleton C
   · simp
-  · simp [dist, dist']
-    have : dist' C ≠ ⊤ := by sorry
-    sorry
-    -- apply (ENat.toNat_eq_iff this).mp
-    -- apply Finset.min_eq_top.mp
-    -- simp [this]
+  · -- Extract two distinct codewords u,v ∈ C
+    simp at h
+    unfold Set.Nontrivial at h
+    obtain ⟨u, hu, v, hv, huv⟩ := h
+    -- The filtered pair set is nonempty
+    have hPairs_nonempty :
+        (((@Finset.univ (C × C) _).filter (fun p => p.1 ≠ p.2))).Nonempty := by
+      refine ⟨(⟨u, hu⟩, ⟨v, hv⟩), ?_⟩
+      simp [huv]
+
+    set pairs : Finset (C × C) :=
+      ((@Finset.univ (C × C) _).filter (fun p => p.1 ≠ p.2)) with hpairs
+    set vals : Finset ℕ :=
+      pairs.image (fun ⟨u, v⟩ => hammingDist u.1 v.1) with hvals
+
+    have hVals_nonempty : vals.Nonempty := by
+      rcases hPairs_nonempty with ⟨p, hp⟩
+      rcases p with ⟨u', v'⟩
+      exact ⟨hammingDist u'.1 v'.1, Finset.mem_image.mpr ⟨(u', v'), hp, rfl⟩⟩
+
+    -- Let d* be the minimum realized distance among distinct pairs
+    set dStar : ℕ := vals.min' (by simpa [hvals] using hVals_nonempty) with hdstar
+
+    -- Show the computable distance's toNat equals this minimum
+    have h_toNat_eq_min' : ‖C‖₀'.toNat = dStar := by
+      -- First, rewrite ‖C‖₀' as the minimum of `vals` in `ℕ∞`.
+      have hmin_coe : ‖C‖₀' = (vals.min : ℕ∞) := by
+        simp only [dist', hvals, hpairs]
+      -- Next, show `(vals.min : ℕ∞) = dStar` by sandwiching with ≤.
+      have hmem_min' : dStar ∈ vals := by
+        simpa [hdstar] using
+          (Finset.min'_mem (s := vals)
+            (by simpa [hvals] using hVals_nonempty))
+      -- `vals.min ≤ dStar` since `dStar ∈ vals`.
+      have h_le : vals.min ≤ (dStar : ℕ∞) := by
+        simpa using (Finset.min_le hmem_min')
+      -- `dStar ≤ a` for all `a ∈ vals`, hence `dStar ≤ vals.min`.
+      have h_ge : (dStar : ℕ∞) ≤ vals.min := by
+        -- Use the universal lower-bound property of `min'`.
+        refine Finset.le_min (s := vals) (m := (dStar : ℕ∞)) ?_;
+        intro a ha; exact
+          (show (dStar : ℕ∞) ≤ (a : ℕ∞) from
+            by
+              -- `dStar ≤ a` in `ℕ`, then coerce.
+              have h' : dStar ≤ a := by
+                -- `min' ≤ any element`.
+                have hleast := (Finset.isLeast_min' (s := vals)
+                                  (H := by simpa [hvals] using hVals_nonempty))
+                exact hleast.2 ha
+              simpa using h')
+      -- Conclude equality in `ℕ∞` and take `toNat`.
+      have : (vals.min : ℕ∞) = dStar := le_antisymm h_le h_ge
+      simpa only [hmin_coe, this, hdstar]
+
+    -- Now prove that the abstract distance equals the same minimum
+    -- Define the set used in sInf
+    let S : Set ℕ := {d | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v ≤ d}
+
+    -- First inequality: dist C ≤ dStar using a minimizing pair
+    have h_le_dStar : dist C ≤ dStar := by
+      -- obtain a pair (u,v) attaining the minimum distance dStar
+      have hmem_min : dStar ∈ vals := by
+        simpa [hdstar] using
+          (Finset.min'_mem (s := vals)
+            (by simpa [hvals] using hVals_nonempty))
+      rcases Finset.mem_image.mp hmem_min with ⟨p, hpairs_mem, hp_eq⟩
+      rcases p with ⟨u', v'⟩
+      have hneq_sub : u' ≠ v' := (Finset.mem_filter.mp hpairs_mem).2
+      -- Lift inequality on subtypes to inequality on values
+      have hneq : (↑u' : n → R) ≠ ↑v' := by
+        intro h
+        apply hneq_sub
+        exact Subtype.ext (by simpa using h)
+      -- Show dStar ∈ S using the minimizing pair
+      have hdist_le_dstar : hammingDist u'.1 v'.1 ≤ dStar := by
+        simp only [hp_eq, le_refl]
+      have hmemS : dStar ∈ S := by
+        change ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v ≤ dStar
+        exact ⟨u'.1, u'.2, v'.1, v'.2, hneq, hdist_le_dstar⟩
+      -- Therefore sInf S ≤ dStar
+      have := Nat.sInf_le (s := S) hmemS
+      simpa [Code.dist, S] using this
+
+    -- Second inequality: dStar ≤ dist C using lower-bound argument
+    have h_dStar_le : dStar ≤ dist C := by
+      -- Show dStar is a lower bound of S
+      have hLB : ∀ d ∈ S, dStar ≤ d := by
+        intro d hd
+        rcases hd with ⟨u, hu, v, hv, hne, hle⟩
+        -- The realized distance appears in vals, hence ≥ dStar
+        have hmem : hammingDist u v ∈ vals := by
+          -- show (⟨u,hu⟩,⟨v,hv⟩) ∈ pairs
+          have hp : (⟨⟨u, hu⟩, ⟨v, hv⟩⟩ : C × C) ∈ pairs := by
+            simp [hpairs, hne]
+          -- then its image is in vals
+          exact Finset.mem_image.mpr ⟨⟨⟨u, hu⟩, ⟨v, hv⟩⟩, hp, rfl⟩
+        -- min' ≤ any member of vals
+        have : dStar ≤ hammingDist u v := by
+          -- Using the `IsLeast` property of `min'`.
+          have hleast := (Finset.isLeast_min' (s := vals)
+                            (H := by simpa [hvals] using hVals_nonempty))
+          have := hleast.2 hmem
+          simpa [hdstar] using this
+        exact le_trans this hle
+      -- The set S is nonempty since C is non-subsingleton
+      have hS_nonempty : S.Nonempty := by
+        refine ⟨hammingDist u v, ?_⟩
+        exact ⟨u, hu, v, hv, huv, le_rfl⟩
+      -- Greatest lower bound property on ℕ
+      have := sInf.le_sInf_of_LB (S := S) hS_nonempty hLB
+      simpa [Code.dist, S] using this
+
+    -- Assemble inequalities and replace toNat of ‖C‖₀' by dStar
+    have : ‖C‖₀ = dStar := le_antisymm h_le_dStar h_dStar_le
+    simp [this, h_toNat_eq_min']
 
 section
 
@@ -607,20 +715,37 @@ noncomputable def byCheckMatrix [CommRing F] (H : Matrix ι κ F) : LinearCode 
 noncomputable def disFromHammingNorm [Semiring F] [DecidableEq F] (LC : LinearCode ι F) : ℕ :=
   sInf {d | ∃ u ∈ LC, u ≠ 0 ∧ hammingNorm u ≤ d}
 
--- Require `[CommRing R]`
-theorem dist_eq_dist_from_HammingNorm [Semiring F] [DecidableEq F] (LC : LinearCode ι F) :
+theorem dist_eq_dist_from_HammingNorm [CommRing F] [DecidableEq F] (LC : LinearCode ι F) :
     Code.dist LC.carrier = disFromHammingNorm LC := by
   simp [Code.dist, disFromHammingNorm]
   congr; unfold setOf; funext d
-  apply Eq.propIntro <;> intro h
-  · obtain ⟨u, hu, v, hv, huv, hDist⟩ := h
-    -- let w := u - v
-    -- have hw : w ∈ C := by simp [Submodule.add_mem]
-    -- refine ⟨w, And.intro hw ⟨v, And.intro hv ⟨huv, ?_⟩⟩⟩
-    sorry
-  · obtain ⟨u, hu, hNorm, hDist⟩ := h
-    -- refine ⟨u, And.intro hu ⟨v, And.intro hv ⟨huv, ?_⟩⟩⟩
-    sorry
+  apply propext
+  constructor
+  · intro h
+    rcases h with ⟨u, hu, v, hv, huv, hle⟩
+    -- Consider the difference w = u - v ∈ LC, w ≠ 0, and ‖w‖₀ = Δ₀(u,v)
+    refine ⟨u - v, ?_, ?_, ?_⟩
+    · -- membership
+      have : (u - v) ∈ LC := by
+        simpa [sub_eq_add_neg] using LC.add_mem hu (LC.neg_mem hv)
+      simpa using this
+    · -- nonzero
+      intro hzero
+      have : u = v := sub_eq_zero.mp hzero
+      exact huv this
+    · -- norm bound via `hammingDist_eq_hammingNorm`
+      have hEq : hammingNorm (u - v) = hammingDist u v := by
+        simpa using (hammingDist_eq_hammingNorm u v).symm
+      simpa [hEq] using hle
+  · intro h
+    rcases h with ⟨w, hw, hw_ne, hle⟩
+    -- Take v = 0, u = w
+    refine ⟨w, hw, (0 : ι → F), LC.zero_mem, ?_, ?_⟩
+    · exact by simpa using hw_ne
+    · -- Δ₀(w, 0) = ‖w‖₀
+      have hEq : hammingDist w 0 = hammingNorm w := by
+        simp [hammingDist, hammingNorm]
+      simpa [hEq] using hle
 
 /--
 The dimension of a linear code.
@@ -685,8 +810,118 @@ lemma dist_UB [CommRing F] {LC : LinearCode ι F} :
   exact sInf.sInf_UB_of_le_UB fun s ⟨_, _, _, s_def⟩ ↦
           s_def ▸ le_trans (card_le_card (subset_univ _)) (le_refl _)
 
-theorem singletonBound [Semiring F] (LC : LinearCode ι F) :
-  dim LC ≤ length LC - Code.minDist (LC : Set (ι → F)) + 1 := by sorry
+-- Restriction to a finite set of coordinates as a linear map
+noncomputable def restrictLinear [Semiring F] (S : Finset ι) :
+  (ι → F) →ₗ[F] (S → F) :=
+{ toFun := fun f i => f i.1,
+  map_add' := by intro f g; ext i; simp,
+  map_smul' := by intro a f; ext i; simp }
+
+theorem singletonBound [CommRing F] [StrongRankCondition F]
+  (LC : LinearCode ι F) :
+  dim LC ≤ length LC - Code.minDist (LC : Set (ι → F)) + 1 := by
+  classical
+  -- abbreviations
+  set d := Code.minDist (LC : Set (ι → F)) with hd
+  -- trivial case when d = 0
+  by_cases h0 : d = 0
+  · -- dim LC ≤ card ι ≤ card ι - 0 + 1
+    have h_le_top : Module.finrank F LC ≤ Module.finrank F (ι → F) :=
+      (Submodule.finrank_le (R := F) (M := (ι → F)) LC)
+    have h_top : Module.finrank F (ι → F) = Fintype.card ι := Module.finrank_pi (R := F)
+    have hfin : Module.finrank F LC ≤ Fintype.card ι := by simpa [h_top] using h_le_top
+    have hfin' : Module.finrank F LC ≤ Fintype.card ι + 1 := hfin.trans (Nat.le_add_right _ _)
+    have : Module.finrank F LC ≤ 1 + (Fintype.card ι - d) := by
+      simpa [h0, Nat.sub_zero, Nat.add_comm] using hfin'
+    simpa [dim, length, hd, Nat.add_comm] using this
+  -- main case: d ≥ 1
+  · have hd_pos : 1 ≤ d := by omega
+    -- choose a set S of coordinates with |S| = |ι| - (d - 1)
+    have h_le : Fintype.card ι - (d - 1) ≤ Fintype.card ι := by
+      exact Nat.sub_le _ _
+    obtain ⟨S, -, hScard⟩ :=
+      (Finset.le_card_iff_exists_subset_card (α := ι) (s := (Finset.univ : Finset ι))
+        (n := Fintype.card ι - (d - 1))).1 h_le
+    -- restriction linear map to S, restricted to the code LC
+    let res : LC →ₗ[F] (S → F) := (restrictLinear (F := F) (ι := ι) S).comp LC.subtype
+    -- show ker res = ⊥ via the minimum distance property
+    have hker : LinearMap.ker res = ⊥ := by
+      classical
+      refine LinearMap.ker_eq_bot'.2 ?_
+      intro x hx
+      -- x : LC, `res x = 0` hence all S-coordinates vanish
+      have hxS : ∀ i ∈ S, (x : ι → F) i = 0 := by
+        intro i hi
+        have := congrArg (fun (f : (S → F)) => f ⟨i, hi⟩) (by simpa using hx)
+        -- simp at this
+        simpa using this
+      -- bound the weight of x by |Sᶜ|
+      let A : Finset ι := Finset.univ.filter (fun i => (x : ι → F) i ≠ 0)
+      have hA_subset_compl : A ⊆ Sᶜ := by
+        intro i hi
+        rcases Finset.mem_filter.mp hi with ⟨-, hne⟩
+        have : i ∉ S := by
+          intro hiS; have := hxS i hiS; exact hne (by simpa using this)
+        simpa [Finset.mem_compl] using this
+      have h_wt_le : Code.wt (x : ι → F) ≤ (Sᶜ).card := by
+        have : Code.wt (x : ι → F) = A.card := by
+          simp [Code.wt, A]
+        simpa [this] using (Finset.card_le_card hA_subset_compl)
+      -- and |Sᶜ| = d - 1 using the chosen size of S
+      have hS_card : S.card = Fintype.card ι - (d - 1) := by simpa using hScard
+      have h_wt_le' : Code.wt (x : ι → F) ≤ d - 1 := by
+        -- (Sᶜ).card = card ι - S.card = d - 1
+        have hcardcompl : (Sᶜ : Finset ι).card = Fintype.card ι - S.card := by
+          simpa using (Finset.card_compl (s := S))
+        -- compute |Sᶜ| from hS_card
+        have h_d_le_len : d ≤ Fintype.card ι := by
+          have h := (dist_UB (LC := LC)); simpa [hd, length] using h
+        have h_d1_le_len : d - 1 ≤ Fintype.card ι :=
+          le_trans (Nat.sub_le d 1) h_d_le_len
+        have hlen_sub : Fintype.card ι - S.card = d - 1 := by
+          have : Fintype.card ι - S.card = Fintype.card ι - (Fintype.card ι - (d - 1)) := by
+            simp [hS_card]
+          simpa [Nat.sub_sub_self h_d1_le_len] using this
+        have hcompl_le : (Sᶜ : Finset ι).card ≤ d - 1 := by simp [hcardcompl, hlen_sub]
+        exact h_wt_le.trans hcompl_le
+      -- if x ≠ 0 then d ≤ wt x, contradiction
+      have hx0 : (x : ι → F) = 0 := by
+        by_contra hx0
+        have hx_mem : Code.wt (x : ι → F) ∈ {w | ∃ c ∈ LC, c ≠ 0 ∧ Code.wt c = w} := by
+          exact ⟨x, x.property, by simpa using hx0, rfl⟩
+        have hmin_le : d ≤ Code.wt (x : ι → F) := by
+          -- d = sInf of weights of nonzero codewords
+          have hmin_eq : Code.minDist (LC : Set (ι → F)) = minWtCodewords LC :=
+            dist_eq_minWtCodewords (LC := LC)
+          have hsInf : sInf {w | ∃ c ∈ LC, c ≠ 0 ∧ Code.wt c = w} ≤ Code.wt (x : ι → F) :=
+            Nat.sInf_le (s := {w | ∃ c ∈ LC, c ≠ 0 ∧ Code.wt c = w}) hx_mem
+          have hd_def : d = sInf {w | ∃ c ∈ LC, c ≠ 0 ∧ Code.wt c = w} := by
+            simp [hd, minWtCodewords, hmin_eq]
+          simpa [hd_def] using hsInf
+        have hcontra : d ≤ d - 1 := le_trans hmin_le h_wt_le'
+        have hsucc_le : d + 1 ≤ d := by
+          have := Nat.add_le_add_right hcontra 1
+          simp [Nat.sub_add_cancel hd_pos, Nat.add_comm] at this
+        exact (Nat.not_succ_le_self d) hsucc_le
+      -- conclude x = 0 in LC
+      apply Subtype.ext
+      simpa using hx0
+    -- Using injectivity, compare finranks
+    have hinj : Function.Injective res := by
+      simpa [LinearMap.ker_eq_bot] using hker
+    have hrange : Module.finrank F (LinearMap.range res) = Module.finrank F LC :=
+      LinearMap.finrank_range_of_inj hinj
+    have hcod_le : Module.finrank F (LinearMap.range res) ≤ Module.finrank F (S → F) :=
+      Submodule.finrank_le (LinearMap.range res)
+    have hcod : Module.finrank F (S → F) = S.card := by
+      simp [Module.finrank_pi (R := F) (ι := {x // x ∈ S})]
+    have : Module.finrank F LC ≤ S.card := by
+      simpa [hrange, hcod] using hcod_le
+    -- turn S.card bound into the target bound via arithmetic: a - (d - 1) ≤ 1 + (a - d)
+    have hS_to_target : S.card ≤ 1 + (Fintype.card ι - d) := by
+      simpa [hScard] using (by omega : Fintype.card ι - (d - 1) ≤ 1 + (Fintype.card ι - d))
+    have hfin : Module.finrank F LC ≤ 1 + (Fintype.card ι - d) := this.trans hS_to_target
+    simpa [dim, length, hd, Nat.add_comm] using hfin
 
 
 /-- The interleaving of a linear code `LC` over index set `ι` is the submodule spanned by
@@ -706,9 +941,39 @@ def Function.interleave₂ {α β : Type*} (u v : α → β) : (Fin 2) × α →
 notation:20 u "⋈" v => Function.interleave₂ u v
 
 /-- **Singleton bound** for linear codes -/
-theorem singleton_bound_linear [Semiring F] (LC : LinearCode ι F) :
-    Module.finrank F LC ≤ card n - (Code.dist LC.carrier) + 1 := by sorry
-  -- have : (ofFinite C).card = (ofFinite R).card ^ (Module.finrank R C) := by
+theorem singleton_bound_linear [CommRing F] [StrongRankCondition F]
+    (LC : LinearCode ι F) :
+    Module.finrank F LC ≤ card ι - (Code.dist LC.carrier) + 1 := by
+  classical
+  -- From the min-distance version and `Code.dist ≤ Code.minDist`.
+  have h1 : Module.finrank F LC ≤ card ι - Code.minDist (LC : Set (ι → F)) + 1 :=
+    singletonBound (LC := LC)
+  -- `dist ≤ minDist` since `= d` implies `≤ d` for witnesses
+  have hdist_le_min : Code.dist LC.carrier ≤ Code.minDist (LC : Set (ι → F)) := by
+    classical
+    let S₁ : Set ℕ := {d | ∃ u ∈ LC, ∃ v ∈ LC, u ≠ v ∧ hammingDist u v ≤ d}
+    let S₂ : Set ℕ := {d | ∃ u ∈ LC, ∃ v ∈ LC, u ≠ v ∧ hammingDist u v = d}
+    have hsub : S₂ ⊆ S₁ := by
+      intro d hd; rcases hd with ⟨u, hu, v, hv, hne, heq⟩; exact ⟨u, hu, v, hv, hne, by simp [heq]⟩
+    by_cases hne : (S₂ : Set ℕ).Nonempty
+    · have hLB : ∀ m ∈ S₂, sInf S₁ ≤ m := fun m hm => Nat.sInf_le (s := S₁) (hsub hm)
+      have := sInf.le_sInf_of_LB (S := S₂) hne hLB
+      simpa [Code.dist, Code.minDist, S₁, S₂] using this
+    · -- S₂ empty ⇒ S₁ empty as well
+      have hS₂empty : S₂ = (∅ : Set ℕ) := (Set.not_nonempty_iff_eq_empty).1 (by simpa using hne)
+      have hS₁empty : S₁ = (∅ : Set ℕ) := by
+        apply (Set.eq_empty_iff_forall_notMem).2
+        intro m hm
+        rcases hm with ⟨u, hu, v, hv, hne, hle⟩
+        have : hammingDist u v ∈ S₂ := ⟨u, hu, v, hv, hne, rfl⟩
+        simpa [hS₂empty, this]
+      simp [Code.dist, Code.minDist, S₁, S₂, hS₁empty, hS₂empty, Nat.sInf_empty]
+  -- Since a - b is antitone in b, add 1 afterwards
+  have hmono' : card ι - Code.minDist (LC : Set (ι → F)) + 1 ≤
+                 card ι - (Code.dist LC.carrier) + 1 := by
+    simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
+      (Nat.add_le_add_right (Nat.sub_le_sub_left hdist_le_min _) 1)
+  exact h1.trans hmono'
 
 end
 

ArkLib/Data/CodingTheory/Prelims.lean

@@ -83,6 +83,14 @@ lemma sInf_UB_of_le_UB {S : Set ℕ} {i : ℕ} : (∀ s ∈ S, s ≤ i) → sInf
     aesop
   · aesop (add simp (show S = ∅ by aesop (add simp Set.Nonempty)))
 
+lemma le_sInf_of_LB {S : Set ℕ} (hne : S.Nonempty) {i : ℕ}
+    (hLB : ∀ s ∈ S, i ≤ s) : i ≤ sInf S := by
+  rw [Nat.sInf_def hne]
+  contrapose hLB
+  simp at hLB ⊢
+  rcases hLB with ⟨s, hsS, hsle⟩
+  exact ⟨s, hsle, hsS⟩
+
 end sInf
 
 @[simp]