Documentation

Acmoi.Exercise1_9

axiom alpha :

structure NA' (α : Type) (σ : Type) :

step : σ → α → Set σ
start : σ
accept : σ

Instances For

instance NA'.instInhabitedFinAlpha {σ : Type} [Inhabited σ] :

Inhabited (NA' (Fin alpha) σ)

Equations

NA'.instInhabitedFinAlpha = { default := { step := fun (x : σ) (x : Fin alpha) => ∅, start := default, accept := default } }

def NA'.step_set {σ : Type} (M : NA' (Fin alpha) σ) (S : Set σ) (a : Fin alpha) :

Set σ

Equations

M.step_set S a = ⋃ s ∈ S, M.step s a

Instances For

def NA'.eval_from {σ : Type} (M : NA' (Fin alpha) σ) (start : Set σ) :

List (Fin alpha) → Set σ

Equations

M.eval_from start = List.foldl M.step_set start

Instances For

def NA'.eval {σ : Type} (M : NA' (Fin alpha) σ) :

List (Fin alpha) → Set σ

Equations

M.eval = M.eval_from {M.start}

Instances For

def NA'.accepts {σ : Type} (M : NA' (Fin alpha) σ) :

Language (Fin alpha)

Equations

M.accepts x = (M.accept ∈ M.eval x)

Instances For

theorem NA'.step_set_empty {σ : Type} (M : NA' (Fin alpha) σ) {a : Fin alpha} :

M.step_set ∅ a = ∅

theorem eval.from_empty {σ : Type} (M : NA' (Fin alpha) σ) (y : List (Fin alpha)) :

M.eval_from ∅ y = ∅

theorem eval.eval_from_subset {γ : Type} (M : NA' (Fin alpha) γ) (w : List (Fin alpha)) (S : Set γ) (T : Set γ) :

S ⊆ T → M.eval_from S w ⊆ M.eval_from T w

theorem eval.step_singleton {σ : Type} (M : NA' (Fin alpha) σ) (q : σ) (a : Fin alpha) :

M.step_set {q} a = M.step q a

theorem eval.eval_from_set_cons {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {y : List (Fin alpha)} {F : Set σ} {a : Fin alpha} (h_given : ∃ r ∈ M.step_set F a, q ∈ M.eval_from {r} y) :

∃ s ∈ F, q ∈ M.eval_from {s} (a :: y)

theorem eval.singleton_member_of_set {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} (F : Set σ) :

q ∈ M.eval_from F l → ∃ r ∈ F, q ∈ M.eval_from {r} l

theorem eval.set_of_singleton_member {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} {F : Set σ} (hsome : ∃ r ∈ F, q ∈ M.eval_from {r} l) :

q ∈ M.eval_from F l

theorem eval.set_iff_singleton_member {σ : Type} {M : NA' (Fin alpha) σ} {q : σ} {l : List (Fin alpha)} (F : Set σ) :

q ∈ M.eval_from F l ↔ ∃ r ∈ F, q ∈ M.eval_from {r} l

instance my_sum_inst {δ : Type} (u : Fintype δ) :

Fintype (Unit ⊕ δ)

Equations

my_sum_inst u = instFintypeSum Unit δ

noncomputable instance instDecidableEqFinAlpha (a : Fin alpha) (b : Fin alpha) :

Decidable (a = b)

Equations

instDecidableEqFinAlpha a b = Classical.dec (a = b)

def hd.trafo {δ : Type} :

Fintype δ → NA' (Fin alpha) δ → Fin alpha → NA' (Fin alpha) (Unit ⊕ δ)

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem hd.lift_to {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} :

let M := hd.trafo u N a; ∀ (q1 q2 : δ), q2 ∈ N.eval_from {q1} t → Sum.inr q2 ∈ M.eval_from {Sum.inr q1} t

theorem hd.accept_self {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} :

N.accepts t → (hd.trafo u N a).accepts (a :: t)

theorem hd.stay_old {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {b : Fin alpha} {q : δ} {q' : Unit ⊕ δ} :

let M := hd.trafo u N a; q' ∈ M.step_set {Sum.inr q} b → ∃ (q_ : δ), q' = Sum.inr q_

theorem hd.remove_step {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {q : δ} {q_ : δ} {a : Fin alpha} {b : Fin alpha} (hq1 : Sum.inr q_ ∈ (hd.trafo u N a).step_set {Sum.inr q} b) :

q_ ∈ N.step_set {q} b

theorem hd.remove_accept {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {q : δ} {a : Fin alpha} {b : Fin alpha} {z : List (Fin alpha)} :

(∃ q' ∈ (hd.trafo u N a).step_set {Sum.inr q} b, (hd.trafo u N a).accept ∈ (hd.trafo u N a).eval_from {q'} z) → ∃ (q_ : δ), Sum.inr q_ ∈ (hd.trafo u N a).step_set {Sum.inr q} b ∧ (hd.trafo u N a).accept ∈ (hd.trafo u N a).eval_from {Sum.inr q_} z

theorem hd.remove {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {y : List (Fin alpha)} :

let M := hd.trafo u N a; ∀ (q : δ), M.accept ∈ M.eval_from {Sum.inr q} y → N.accept ∈ N.eval_from {q} y

theorem hd.accepts_only {δ : Type} [u : Fintype δ] {N : NA' (Fin alpha) δ} {a : Fin alpha} {t : List (Fin alpha)} :

(hd.trafo u N a).accepts t → ∃ (s : List (Fin alpha)), t = a :: s ∧ N.accepts s

theorem hd.regex {δ : Type} {u : Fintype δ} {N : NA' (Fin alpha) δ} {a : Fin alpha} (t : List (Fin alpha)) :

(hd.trafo u N a).accepts t ↔ ∃ (s : List (Fin alpha)), t = a :: s ∧ N.accepts s

def accepts_exactly {δ : Type} (M : NA' (Fin alpha) δ) (x : List (Fin alpha)) :

Equations

accepts_exactly M x = ∀ (y : List (Fin alpha)), y.length = x.length → (M.accepts y ↔ y = x)

Instances For

def A_N_word_bounded_by (x : List (Fin alpha)) (n : ℕ) :

Equations

A_N_word_bounded_by x n = ∃ (δ : Type) (u : Fintype δ), Fintype.elems.card ≤ n ∧ ∃ (M : NA' (Fin alpha) δ), accepts_exactly M x

Instances For

theorem A_N_word_finite_prelim (x : List (Fin alpha)) :

∃ (δ : Type) (x_1 : Fintype δ) (M : NA' (Fin alpha) δ), accepts_exactly M x

theorem A_N_word_finite (x : List (Fin alpha)) :

∃ (n : ℕ), A_N_word_bounded_by x n

noncomputable def A_N_word :

List (Fin alpha) → ℕ

Equations

A_N_word x = Nat.find ⋯

Instances For

theorem Fintype_card_sum_typesafe {δ : Type} {u : Fintype δ} :

Fintype.elems.card = Fintype.card Unit + Fintype.elems.card

theorem autocomplex_bound_nil :

∃ (δ : Type) (u : Fintype δ), Fintype.elems.card ≤ [].length.succ ∧ ∃ (M : NA' (Fin alpha) δ), accepts_exactly M []

theorem A_N_word_nil_bound_length_succ :

A_N_word [] ≤ 1

theorem nonempty_of_mem {α : Type} {a : α} {s : Finset α} :

a ∈ s → s.Nonempty

theorem lower_bound (x : List (Fin alpha)) :

1 ≤ A_N_word x

theorem A_N_word_nil :

A_N_word [] = 1

theorem accepts_exactly_hd {δ : Type} (N : NA' (Fin alpha) δ) (y : List (Fin alpha)) (a : Fin alpha) (u : Fintype δ) (hae : accepts_exactly N y) :

let M := hd.trafo u N a; accepts_exactly M (a :: y)

theorem hd_card (δ : Type) (u : Fintype δ) :

Fintype.elems.card = Fintype.elems.card.succ

theorem hd_card_my (δ : Type) (u : Fintype δ) :

Fintype.elems.card = Fintype.elems.card.succ

theorem iterative_bound (x : List (Fin alpha)) (a : Fin alpha) :

A_N_word (a :: x) ≤ (A_N_word x).succ

theorem subword_inequality (x : List (Fin alpha)) (y : List (Fin alpha)) :

A_N_word (x ++ y) ≤ x.length + A_N_word y

theorem A_N_word_bound_length_succ' (x : List (Fin alpha)) :

A_N_word x ≤ x.length.succ