[GOAL]
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
a : α
⊢ evalFrom M s (x ++ [a]) = step M (evalFrom M s x) a
[PROOFSTEP]
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ accepts M ↔ evalFrom M M.start x ∈ M.accept
[PROOFSTEP]
rfl
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
obtain ⟨n, m, hneq, heq⟩ :=
  Fintype.exists_ne_map_eq_of_card_lt (fun n : Fin (Fintype.card σ + 1) => M.evalFrom s (x.take n)) (by norm_num)
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
⊢ Fintype.card σ < Fintype.card (Fin (Fintype.card σ + 1))
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
wlog hle : (n : ℕ) ≤ m
[GOAL]
case intro.intro.intro.inr
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
this :
  ∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α} {s t : σ},
    Fintype.card σ ≤ List.length x →
      evalFrom M s x = t →
        ∀ (n m : Fin (Fintype.card σ + 1)),
          n ≠ m →
            evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x) →
              ↑n ≤ ↑m →
                ∃ q a b c,
                  x = a ++ b ++ c ∧
                    List.length a + List.length b ≤ Fintype.card σ ∧
                      b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
hle : ¬↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle)
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ ∃ q a b c,
    x = a ++ b ++ c ∧
      List.length a + List.length b ≤ Fintype.card σ ∧
        b ≠ [] ∧ evalFrom M s a = q ∧ evalFrom M q b = q ∧ evalFrom M q c = t
[PROOFSTEP]
refine' ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by rfl, _⟩
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M s (List.take (↑n) (List.take (↑m) x)) = evalFrom M s (List.take (↑n) (List.take (↑m) x))
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ x = List.take (↑n) (List.take (↑m) x) ++ List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x
[PROOFSTEP]
rw [List.take_append_drop, List.take_append_drop]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ List.length (List.take (↑n) (List.take (↑m) x)) + List.length (List.drop (↑n) (List.take (↑m) x)) ≤ Fintype.card σ
[PROOFSTEP]
simp only [List.length_drop, List.length_take]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ min (↑n) (min (↑m) (List.length x)) + (min (↑m) (List.length x) - ↑n) ≤ Fintype.card σ
[PROOFSTEP]
rw [min_eq_left (hm.trans hlen), min_eq_left hle, add_tsub_cancel_of_le hle]
[GOAL]
case refine'_2
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ ↑m ≤ Fintype.card σ
[PROOFSTEP]
exact hm
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ List.drop (↑n) (List.take (↑m) x) ≠ []
[PROOFSTEP]
intro h
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
⊢ False
[PROOFSTEP]
have hlen' := congr_arg List.length h
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : List.length (List.drop (↑n) (List.take (↑m) x)) = List.length []
⊢ False
[PROOFSTEP]
simp only [List.length_drop, List.length, List.length_take] at hlen'
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : min (↑m) (List.length x) - ↑n = 0
⊢ False
[PROOFSTEP]
rw [min_eq_left, tsub_eq_zero_iff_le] at hlen'
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ False
[PROOFSTEP]
apply hneq
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ n = m
[PROOFSTEP]
apply le_antisymm
[GOAL]
case refine'_3.a
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ n ≤ m
case refine'_3.a
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : ↑m ≤ ↑n
⊢ m ≤ n
[PROOFSTEP]
assumption'
[GOAL]
case refine'_3
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
h : List.drop (↑n) (List.take (↑m) x) = []
hlen' : min (↑m) (List.length x) - ↑n = 0
⊢ ↑m ≤ List.length x
[PROOFSTEP]
exact hm.trans hlen
[GOAL]
case refine'_4
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      evalFrom M s (List.take (↑n) (List.take (↑m) x)) ∧
    evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) = M.evalFrom s ((x.take m).take n) := by
  rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← List.take_take, min_eq_left hle,
    List.take_append_drop]
[GOAL]
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
[PROOFSTEP]
rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ← List.take_take, min_eq_left hle,
  List.take_append_drop]
[GOAL]
case refine'_4
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
hq :
  evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      evalFrom M s (List.take (↑n) (List.take (↑m) x)) ∧
    evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
use hq
[GOAL]
case right
α✝ : Type u
σ✝ : Type v
M✝ : DFA α✝ σ✝
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ List.length x
hx : evalFrom M s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : evalFrom M s (List.take (↑n) x) = evalFrom M s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hm : ↑m ≤ Fintype.card σ
hq :
  evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    evalFrom M s (List.take (↑n) (List.take (↑m) x))
⊢ evalFrom M (evalFrom M s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
[PROOFSTEP]
rwa [← hq, ← evalFrom_of_append, ← evalFrom_of_append, ← List.append_assoc, List.take_append_drop,
  List.take_append_drop]
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : y ∈ {x}∗
⊢ evalFrom M s y = s
[PROOFSTEP]
rw [Language.mem_kstar] at hy
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
x y : List α
s : σ
hx : evalFrom M s x = s
hy : ∃ L, y = List.join L ∧ ∀ (y : List α), y ∈ L → y ∈ {x}
⊢ evalFrom M s y = s
[PROOFSTEP]
rcases hy with ⟨S, rfl, hS⟩
[GOAL]
case intro.intro
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ {x}
⊢ evalFrom M s (List.join S) = s
[PROOFSTEP]
induction' S with a S ih
[GOAL]
case intro.intro.nil
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S : List (List α)
hS✝ : ∀ (y : List α), y ∈ S → y ∈ {x}
hS : ∀ (y : List α), y ∈ [] → y ∈ {x}
⊢ evalFrom M s (List.join []) = s
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
have ha := hS a (List.mem_cons_self _ _)
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a ∈ {x}
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
rw [Set.mem_singleton_iff] at ha
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join (a :: S)) = s
[PROOFSTEP]
rw [List.join, evalFrom_of_append, ha, hx]
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ evalFrom M s (List.join S) = s
[PROOFSTEP]
apply ih
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
⊢ ∀ (y : List α), y ∈ S → y ∈ {x}
[PROOFSTEP]
intro z hz
[GOAL]
case intro.intro.cons
α : Type u
σ : Type v
M : DFA α σ
x : List α
s : σ
hx : evalFrom M s x = s
S✝ : List (List α)
hS✝ : ∀ (y : List α), y ∈ S✝ → y ∈ {x}
a : List α
S : List (List α)
ih : (∀ (y : List α), y ∈ S → y ∈ {x}) → evalFrom M s (List.join S) = s
hS : ∀ (y : List α), y ∈ a :: S → y ∈ {x}
ha : a = x
z : List α
hz : z ∈ S
⊢ z ∈ {x}
[PROOFSTEP]
exact hS z (List.mem_cons_of_mem a hz)
[GOAL]
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ accepts M
hlen : Fintype.card σ ≤ List.length x
⊢ ∃ a b c, x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split hlen rfl
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
⊢ ∃ a b c, x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
use a, b, c, hx, hlen, hnil
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
⊢ {a} * {b}∗ * {c} ≤ accepts M
[PROOFSTEP]
intro y hy
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
y : List α
hy : y ∈ {a} * {b}∗ * {c}
⊢ y ∈ accepts M
[PROOFSTEP]
rw [Language.mem_mul] at hy
[GOAL]
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
y : List α
hy : ∃ a_1 b_1, a_1 ∈ {a} * {b}∗ ∧ b_1 ∈ {c} ∧ a_1 ++ b_1 = y
⊢ y ∈ accepts M
[PROOFSTEP]
rcases hy with ⟨ab, c', hab, hc', rfl⟩
[GOAL]
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
ab c' : List α
hab : ab ∈ {a} * {b}∗
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ accepts M
[PROOFSTEP]
rw [Language.mem_mul] at hab
[GOAL]
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
ab c' : List α
hab : ∃ a_1 b_1, a_1 ∈ {a} ∧ b_1 ∈ {b}∗ ∧ a_1 ++ b_1 = ab
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ accepts M
[PROOFSTEP]
rcases hab with ⟨a', b', ha', hb', rfl⟩
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
c' : List α
hc' : c' ∈ {c}
a' b' : List α
ha' : a' ∈ {a}
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
rw [Set.mem_singleton_iff] at ha' hc'
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
a b c : List α
hx : x = a ++ b ++ c
hlen : List.length a + List.length b ≤ Fintype.card σ
hnil : b ≠ []
hb : evalFrom M (evalFrom M ?m.8103 a) b = evalFrom M ?m.8103 a
hc : evalFrom M (evalFrom M ?m.8103 a) c = evalFrom M ?m.8103 x
c' : List α
hc' : c' = c
a' b' : List α
ha' : a' = a
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
substs ha' hc'
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : List.length a' + List.length b ≤ Fintype.card σ
hb : evalFrom M (evalFrom M ?m.8103 a') b = evalFrom M ?m.8103 a'
hx : x = a' ++ b ++ c'
hc : evalFrom M (evalFrom M ?m.8103 a') c' = evalFrom M ?m.8103 x
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
have h := M.evalFrom_of_pow hb hb'
[GOAL]
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ accepts M
hlen✝ : Fintype.card σ ≤ List.length x
b : List α
hnil : b ≠ []
c' a' b' : List α
hb' : b' ∈ {b}∗
hlen : List.length a' + List.length b ≤ Fintype.card σ
hb : evalFrom M (evalFrom M ?m.8103 a') b = evalFrom M ?m.8103 a'
hx : x = a' ++ b ++ c'
hc : evalFrom M (evalFrom M ?m.8103 a') c' = evalFrom M ?m.8103 x
h : evalFrom M (evalFrom M ?m.8103 a') b' = evalFrom M ?m.8103 a'
⊢ a' ++ b' ++ c' ∈ accepts M
[PROOFSTEP]
rwa [mem_accepts, evalFrom_of_append, evalFrom_of_append, h, hc]


[GOAL]
α : Type u
e : Encoding α
⊢ Function.Injective e.encode
[PROOFSTEP]
refine' fun _ _ h => Option.some_injective _ _
[GOAL]
α : Type u
e : Encoding α
x✝¹ x✝ : α
h : encode e x✝¹ = encode e x✝
⊢ some x✝¹ = some x✝
[PROOFSTEP]
rw [← e.decode_encode, ← e.decode_encode, h]
[GOAL]
⊢ Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Γ'),
    x ∈
      { val := {blank, bit true, bit false, bra, ket, comma},
        nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
intro
[GOAL]
x✝ : Γ'
⊢ x✝ ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
cases_type* Γ' Bool
[GOAL]
case blank
⊢ blank ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bit.false
⊢ bit false ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bit.true
⊢ bit true ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case bra
⊢ bra ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case ket
⊢ ket ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
case comma
⊢ comma ∈
    { val := {blank, bit true, bit false, bra, ket, comma},
      nodup := (_ : Multiset.Nodup {blank, bit true, bit false, bra, ket, comma}) }
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (n : PosNum), decodePosNum (encodePosNum n) = n
[PROOFSTEP]
intro n
[GOAL]
n : PosNum
⊢ decodePosNum (encodePosNum n) = n
[PROOFSTEP]
induction' n with m hm m hm
[GOAL]
case one
⊢ decodePosNum (encodePosNum PosNum.one) = PosNum.one
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ decodePosNum (encodePosNum (PosNum.bit1 m)) = PosNum.bit1 m
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ decodePosNum (encodePosNum (PosNum.bit0 m)) = PosNum.bit0 m
[PROOFSTEP]
unfold encodePosNum decodePosNum
[GOAL]
case one
⊢ (if [] = [] then PosNum.one else PosNum.bit1 (decodePosNum [])) = PosNum.one
[PROOFSTEP]
rfl
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 (decodePosNum (encodePosNum m))) = PosNum.bit1 m
[PROOFSTEP]
rw [hm]
[GOAL]
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 m) = PosNum.bit1 m
[PROOFSTEP]
exact if_neg (encodePosNum_nonempty m)
[GOAL]
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ PosNum.bit0 (decodePosNum (encodePosNum m)) = PosNum.bit0 m
[PROOFSTEP]
exact congr_arg PosNum.bit0 hm
[GOAL]
⊢ ∀ (n : Num), decodeNum (encodeNum n) = n
[PROOFSTEP]
intro n
[GOAL]
n : Num
⊢ decodeNum (encodeNum n) = n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
⊢ decodeNum (encodeNum Num.zero) = Num.zero
[PROOFSTEP]
unfold encodeNum decodeNum
[GOAL]
case pos
n : PosNum
⊢ decodeNum (encodeNum (Num.pos n)) = Num.pos n
[PROOFSTEP]
unfold encodeNum decodeNum
[GOAL]
case zero
⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero
[PROOFSTEP]
rfl
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
[PROOFSTEP]
rw [decode_encodePosNum n]
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
[PROOFSTEP]
rw [PosNum.cast_to_num]
[GOAL]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
[PROOFSTEP]
exact if_neg (encodePosNum_nonempty n)
[GOAL]
⊢ ∀ (n : ℕ), decodeNat (encodeNat n) = n
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ decodeNat (encodeNat n) = n
[PROOFSTEP]
conv_rhs => rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
| n
[PROOFSTEP]
rw [← Num.to_of_nat n]
[GOAL]
n : ℕ
⊢ decodeNat (encodeNat n) = ↑↑n
[PROOFSTEP]
exact congr_arg ((↑) : Num → ℕ) (decode_encodeNum n)
[GOAL]
x : ℕ
⊢ decodeNat (List.map sectionΓ'Bool ((fun x => List.map inclusionBoolΓ' (encodeNat x)) x)) = x
[PROOFSTEP]
rw [List.map_map, leftInverse_section_inclusion.id, List.map_id, decode_encodeNat]
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ #α ≤ ℵ₀
[PROOFSTEP]
refine' Cardinal.lift_le.1 (e.card_le_card_list.trans _)
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ lift #(List e.Γ) ≤ lift ℵ₀
[PROOFSTEP]
simp only [Cardinal.lift_aleph0, Cardinal.lift_le_aleph0]
[GOAL]
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
cases' isEmpty_or_nonempty e.Γ with h h
[GOAL]
case inl
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : IsEmpty e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
simp only [Cardinal.mk_le_aleph0]
[GOAL]
case inr
α : Type u
e : Encoding α
inst✝ : Encodable e.Γ
h : Nonempty e.Γ
⊢ #(List e.Γ) ≤ ℵ₀
[PROOFSTEP]
rw [Cardinal.mk_list_eq_aleph0]