Lower bound on number of DFA states

Stream: general

[Frederick Pu]

Hi all, am proving a lower bound on the number of DFA states for a dfa that accepts the following language

$$L = \{w | \text{$w$ has a $1$ at the $k$th from the last character} \}$$

I have sketched the proof below in lean but need help filling in some of the sorries

import Mathlib.Computability.RegularExpressions
import Mathlib.Data.Finite.Defs
import Mathlib.Data.Set.Finite.Basic
import Mathlib.Data.Finite.Prod
import Mathlib.Logic.Function.Defs
import Mathlib.Tactic
import Mathlib.Computability.DFA
import Mathlib.Data.Set.Card
import Mathlib.Data.Finite.Defs

-- a)
-- pigeonhole princinple that we're using
example {α β : Type*} (A : Set α) (hA : A.Finite) (B : Set β) (hB : B.Finite) (f : α → β) (hf : Set.MapsTo f A B): A.ncard > B.ncard → ∃ a₁ ∈ A, ∃ a₂ ∈ A, a₁ ≠ a₂ ∧ f a₁ = f a₂ := by
  exact fun a => Set.exists_ne_map_eq_of_ncard_lt_of_maps_to a hf hB


#eval List.replicate 0 0
example {α : Type*} (k : ℕ) (d : DFA (Fin 2) α) (Hd : d.accepts = {w : List (Fin 2) | w.length ≥ k ∧ w.get! (w.length - k) = 1}) :
  (Set.univ : Set α).Finite → 2^k ≤ (Set.univ : Set α).ncard := by
{
  intro hf
  apply by_contradiction
  intro HC
  simp at HC

  let S := {w : List (Fin 2) | w.length = k}
  have : ∃ w₁ ∈ S, ∃ w₂ ∈ S, w₁ ≠ w₂ ∧ d.eval w₁ = d.eval w₂ := by
  {
    have : S.ncard = 2^k := by
      simp [S]
      sorry -- this cane be proven via induction
    rw [← this] at HC
    exact Set.exists_ne_map_eq_of_ncard_lt_of_maps_to HC (fun a a => trivial) hf
  }
  match this with
  | ⟨w₁, hw1, w₂, hw2, h, HH⟩ => {
    simp [S] at hw2
    simp [S] at hw1
    have : ∃ i, w₁.get! i ≠ w₂.get! i := by {
      have : w₁.length = w₂.length := by linarith
      sorry
    }
    match this with
    | ⟨i, hi⟩ => {
      have : w₁ ++ List.replicate i 0 ∈ d.accepts ↔ w₂ ++ List.replicate i 0 ∉ d.accepts := by {
        have crux₁ : (w₁ ++ List.replicate i 0).get! ((w₁ ++ List.replicate i 0).length - k) = w₁.get! i := by {
          simp only [Fin.isValue, List.length_append, List.length_replicate]
          rw [hw1]
          simp only [Fin.isValue, add_tsub_cancel_left]
          have : i < w₁.length := sorry
          sorry
        }
        have crux₂ : (w₂ ++ List.replicate i 0).get! ((w₂ ++ List.replicate i 0).length - k) = w₂.get! i := by {
          simp only [Fin.isValue, List.length_append, List.length_replicate]
          rw [hw2]
          simp only [Fin.isValue, add_tsub_cancel_left]
          have : i < w₂.length := sorry
          sorry
        }
        have : (w₁ ++ List.replicate i 0).length ≥ k := sorry
        have : (w₂ ++ List.replicate i 0).length ≥ k := sorry

        match hii : w₁.get! i with
        | 0 => {
          rw [hii] at hi
          have : w₂.get! i  = 1 := Fin.eq_one_of_neq_zero (w₂.get! i) (id (Ne.symm hi))
          rw [Hd]
          rw [Set.mem_def, Set.mem_def, setOf]
          have o : (w₁ ++ List.replicate i 0).get! ((w₁ ++ List.replicate i 0).length - k) ≠ 1 := by
            rw [crux₁, hii]
            exact Fin.zero_ne_one
          have oo : (w₂ ++ List.replicate i 0).get! ((w₂ ++ List.replicate i 0).length - k) = 1 := by
            rw [crux₂]
            assumption
          tauto
        }
        | 1 => {
          rw [hii] at hi
          have : w₂.get! i = 0 := sorry
          rw [Hd]
          rw [Set.mem_def, Set.mem_def, setOf]
          have o : (w₁ ++ List.replicate i 0).get! ((w₁ ++ List.replicate i 0).length - k) = 1 := by
            rw [crux₁, hii]
          have oo : (w₂ ++ List.replicate i 0).get! ((w₂ ++ List.replicate i 0).length - k) ≠ 1 := by
            rw [crux₂]
            exact id (Ne.symm hi)
          tauto
        }
      }
      have hd1 : d.eval (w₁ ++ List.replicate i 0) ∈ d.accept ↔ w₁ ++ List.replicate i 0 ∈ d.accepts := Set.mem_def
      have hd2 : d.eval (w₂ ++ List.replicate i 0) ∈ d.accept ↔ w₂ ++ List.replicate i 0 ∈ d.accepts := Set.mem_def
      have hdd : d.eval (w₁ ++ List.replicate i 0) =  d.eval (w₂ ++ List.replicate i 0) := sorry
      rw [hdd] at hd1
      tauto
    }
  }
}

[Daniel Weber]

For the first sorry you should extract it to a separate theorem and try to prove it:

theorem extracted_1 (k : ℕ) : {w : List (Fin 2) | w.length = k}.ncard = 2 ^ k := sorry

[Daniel Weber]

The second sorry can be filled by

contrapose! h
simp only [List.get!_eq_getElem!] at h
exact List.ext_getElem! this h

[Daniel Weber]

However, you should try and avoid using [x]! in proofs, it's likely easier to use either [] or []?

[Daniel Weber]

You can also avoid using {} everywhere, the indentation already takes care of that

[Mario Carneiro]

you seem to have an off by one error, for w.get! (w.length - k) to evaluate to something sensible you need k > 0

[Frederick Pu]

w is the in the set of words of length k

[Frederick Pu]

oh you mean in the theorem statment, yee ig the theorem only holds for k > 0

[Frederick Pu]

also is there any way to have []? without getting a bunch of annoying coecersions?