internlm/Lean-Github huggingface dataset:
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
⊢ f x1 = f x2 → x1 = x2
Tactic:
intro a2
Proof state after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
⊢ x1 = x2
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x1_mem : x1 = xs_hd ∨ x1 ∈ xs_tl
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
⊢ x1 = x2
Tactic:
cases x1_mem
Proof state after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
h✝ : x1 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
h✝ : x1 ∈ xs_tl
⊢ x1 = x2
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_left : x1 = xs_hd
⊢ x1 = x2
Tactic:
case inl x1_mem_left =>
  contradiction
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr x1_mem_right =>
  cases x2_mem
  case inl x2_mem_left =>
    contradiction
  case inr x2_mem_right =>
    simp only [List.InjOn] at a1_left
    apply a1_left x1_mem_right x2_mem_right a2
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_left : x1 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
x2_mem : x2 = xs_hd ∨ x2 ∈ xs_tl
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
⊢ x1 = x2
Tactic:
cases x2_mem
Proof state after:
case inl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
h✝ : x2 = xs_hd
⊢ x1 = x2

case inr
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
h✝ : x2 ∈ xs_tl
⊢ x1 = x2
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_left : x2 = xs_hd
⊢ x1 = x2
Tactic:
case inl x2_mem_left =>
  contradiction
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
case inr x2_mem_right =>
  simp only [List.InjOn] at a1_left
  apply a1_left x1_mem_right x2_mem_right a2
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_left : x2 = xs_hd
⊢ x1 = x2
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
simp only [List.InjOn] at a1_left
Proof state after:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : ∀ ⦃x₁ : α⦄, x₁ ∈ xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_tl → f x₁ = f x₂ → x₁ = x₂
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : ∀ ⦃x₁ : α⦄, x₁ ∈ xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_tl → f x₁ = f x₂ → x₁ = x₂
a1_right : map f xs_tl = ys_tl
x1 x2 : α
c1 : ¬x1 = xs_hd
c2 : ¬x2 = xs_hd
a2 : f x1 = f x2
x1_mem_right : x1 ∈ xs_tl
x2_mem_right : x2 ∈ xs_tl
⊢ x1 = x2
Tactic:
apply a1_left x1_mem_right x2_mem_right a2
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Tactic:
constructor
Proof state after:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd

case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ Function.updateITE f xs_hd ys_hd xs_hd = ys_hd
Tactic:
simp only [Function.updateITE]
Proof state after:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (if True then ys_hd else f xs_hd) = ys_hd
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right.left
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (if True then ys_hd else f xs_hd) = ys_hd
Tactic:
simp
Proof state after:
no goals
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl
Tactic:
simp only [← a1_right]
Proof state after:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = map f xs_tl
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right.right
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ map (Function.updateITE f xs_hd ys_hd) xs_tl = map f xs_tl
Tactic:
apply Function.updateITE_not_mem_list
Proof state after:
case right.right.h1
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ xs_hd ∉ xs_tl
Theorem: List.nodup_eq_len_imp_exists_bijon
Proof state before:
case right.right.h1
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ xs_hd ∉ xs_tl
Tactic:
exact h2_left
Proof state after:
no goals
Theorem: nodup_eq_len_imp_eqv
Proof state before:
α : Type
inst✝ : DecidableEq α
xs ys : List α
h1 : xs.length = ys.length
h2 : xs.Nodup
h3 : ys.Nodup
⊢ ∃ f, List.map (⇑f) xs = ys
Tactic:
sorry
Proof state after:
no goals
Theorem: DFA.mem_accepts
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
D : DFA α σ
input : List α
⊢ D.accepts input ↔ D.eval_from D.starting_state input ∈ D.accepting_state_list
Tactic:
rfl
Proof state after:
no goals
Theorem: NFA_to_DFA_is_equiv
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
⊢ N.to_DFA.accepts = N.accepts
Tactic:
ext cs
Proof state after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.accepts cs ↔ N.accepts cs
Theorem: NFA_to_DFA_is_equiv
Proof state before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.accepts cs ↔ N.accepts cs
Tactic:
simp only [DFA.mem_accepts]
Proof state after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔ N.accepts cs
Theorem: NFA_to_DFA_is_equiv
Proof state before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔ N.accepts cs
Tactic:
simp only [NFA.mem_accepts]
Proof state after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Theorem: NFA_to_DFA_is_equiv
Proof state before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Tactic:
simp only [NFA.to_DFA]
Proof state after:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ { step := N.eval_one, starting_state := N.starting_state_list,
            accepting_state_list := sorryAx (List (List σ)) }.eval_from
        N.starting_state_list cs ∈
      sorryAx (List (List σ)) ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Theorem: NFA_to_DFA_is_equiv
Proof state before:
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ { step := N.eval_one, starting_state := N.starting_state_list,
            accepting_state_list := sorryAx (List (List σ)) }.eval_from
        N.starting_state_list cs ∈
      sorryAx (List (List σ)) ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list
Tactic:
sorry
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
F : Formula
vs : List VarName
v : VarName
Γ : List (VarName × MetaVarName)
h1 : NoMetaVarAndAllFreeInList vs F
h2 : v ∉ vs
⊢ NotFree Γ v F
Tactic:
induction F generalizing vs
Proof state after:
case meta_var_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ a✝)

case pred_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : PredName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ a✝¹ a✝)

case eq_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (eq_ a✝¹ a✝)

case true_
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_

case not_
v : VarName
Γ : List (VarName × MetaVarName)
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs a✝.not_
h2 : v ∉ vs
⊢ NotFree Γ v a✝.not_

case imp_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝¹ → v ∉ vs → NotFree Γ v a✝¹
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (a✝¹.imp_ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (a✝¹.imp_ a✝)

case forall_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs a✝ → v ∉ vs → NotFree Γ v a✝
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (forall_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (forall_ a✝¹ a✝)

case def_
v : VarName
Γ : List (VarName × MetaVarName)
a✝¹ : DefName
a✝ vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ a✝¹ a✝)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ a✝¹ a✝)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ X)
Tactic:
case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
case pred_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  tauto
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_
Tactic:
case true_ =>
  unfold NotFree
  simp
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
h2 : v ∉ vs
⊢ NotFree Γ v phi.not_
Tactic:
case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  exact phi_ih vs h1 h2
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (def_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (def_ X xs)
Tactic:
case def_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  tauto
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ X)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h2 : v ∉ vs
h1 : False
⊢ NotFree Γ v (meta_var_ X)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h2 : v ∉ vs
h1 : False
⊢ NotFree Γ v (meta_var_ X)
Tactic:
contradiction
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (pred_ X xs)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (pred_ X xs)
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs
Tactic:
tauto
Proof state after:
no goals
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (eq_ x y)
h2 : v ∉ vs
⊢ NotFree Γ v (eq_ x y)
Tactic:
unfold NoMetaVarAndAllFreeInList at h1
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ NotFree Γ v (eq_ x y)
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ NotFree Γ v (eq_ x y)
Tactic:
unfold NotFree
Proof state after:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Tactic:
cases h1
Proof state after:
case intro
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
left✝ : x ∈ vs
right✝ : y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v ∧ ¬y = v
Tactic:
constructor
Proof state after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v

case right
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬y = v
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v
Tactic:
intro contra
Proof state after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ False
Theorem: MM0.all_free_in_list_and_not_in_list_imp_not_free
Proof state before:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ False
Tactic:
apply h2
Proof state after:
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ v ∈ vs