internlm/Lean-Github huggingface dataset:
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof state before:
case h.right.h.d.derivation
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Grammar.Derivation G [Sum.inl G.start] ?h.right.h.d.w'

case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = ?h.right.h.d.w'

case h.right.h.d.w'
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
Tactic:
assumption
Proof state after:
case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = Sum.inr <$> w
Theorem: RegularGrammar.lang_subs_toNFA_lang
Proof state before:
case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = Sum.inr <$> w
Tactic:
rfl
Proof state after:
no goals
Theorem: RegularGrammar.lang_eq_toNFA_lang
Proof state before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ Grammar.GeneratedLanguage G = NFA.AcceptedLanguage (toNFA G)
Tactic:
apply Set.ext
Proof state after:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ ∀ (x : Word { x // x ∈ G.Z }), x ∈ Grammar.GeneratedLanguage G ↔ x ∈ NFA.AcceptedLanguage (toNFA G)
Theorem: RegularGrammar.lang_eq_toNFA_lang
Proof state before:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ ∀ (x : Word { x // x ∈ G.Z }), x ∈ Grammar.GeneratedLanguage G ↔ x ∈ NFA.AcceptedLanguage (toNFA G)
Tactic:
intro
Proof state after:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G ↔ x✝ ∈ NFA.AcceptedLanguage (toNFA G)
Theorem: RegularGrammar.lang_eq_toNFA_lang
Proof state before:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G ↔ x✝ ∈ NFA.AcceptedLanguage (toNFA G)
Tactic:
constructor
Proof state after:
case h.mp
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G → x✝ ∈ NFA.AcceptedLanguage (toNFA G)

case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Theorem: RegularGrammar.lang_eq_toNFA_lang
Proof state before:
case h.mp
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G → x✝ ∈ NFA.AcceptedLanguage (toNFA G)

case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Tactic:
apply RegularGrammar.lang_subs_toNFA_lang
Proof state after:
case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Theorem: RegularGrammar.lang_eq_toNFA_lang
Proof state before:
case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Tactic:
apply RegularGrammar.toNFA_lang_subs_lang
Proof state after:
no goals
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
⊢ decode (encode []) = []
Tactic:
simp [encode, decode]
Proof state after:
no goals
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
⊢ decode (encode (x :: xs)) = x :: xs
Tactic:
have ih := encodek xs
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ decode (encode (x :: xs)) = x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ decode (encode (x :: xs)) = x :: xs
Tactic:
simp [encode, decode, Nat.fin_mod, FinDenumerable.decode_fin]
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ Option.get (Encodable.decode ((encode xs * Fintype.card α + Encodable.encode x) % Fintype.card α)) ⋯ ::
      decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) =
    x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ Option.get (Encodable.decode ((encode xs * Fintype.card α + Encodable.encode x) % Fintype.card α)) ⋯ ::
      decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) =
    x :: xs
Tactic:
simp [<- Nat.mod_add_mod, Nat.mod_eq_of_lt $ inst.encode_lt_card x]
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) = x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode ((encode xs * Fintype.card α + Encodable.encode x) / Fintype.card α) = x :: xs
Tactic:
simp [Nat.add_div inst.card_pos, Nat.div_eq_of_lt $ inst.encode_lt_card x]
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x ::
      decode
        (encode xs * Fintype.card α / Fintype.card α +
          if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) =
    x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x ::
      decode
        (encode xs * Fintype.card α / Fintype.card α +
          if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) =
    x :: xs
Tactic:
simp [Nat.mul_div_cancel (encode xs) inst.card_pos]
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) = x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if Fintype.card α ≤ Encodable.encode x % Fintype.card α then 1 else 0) = x :: xs
Tactic:
rw [<- ite_not _]
Proof state after:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if ¬Fintype.card α ≤ Encodable.encode x % Fintype.card α then 0 else 1) = x :: xs
Theorem: Word.encodek
Proof state before:
α : Type u_1
inst : Alphabet α
x : α
xs : List α
ih : decode (encode xs) = xs
⊢ x :: decode (encode xs + if ¬Fintype.card α ≤ Encodable.encode x % Fintype.card α then 0 else 1) = x :: xs
Tactic:
simp [Nat.not_le_of_lt _, Nat.mod_lt _ inst.card_pos, ih]
Proof state after:
no goals
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
⊢ encode (decode 0) = 0
Tactic:
simp [encode, decode]
Proof state after:
no goals
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
⊢ encode (decode (Nat.succ n)) = Nat.succ n
Tactic:
have ih := @decodenk α _ (n / inst.card)
Proof state after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (Nat.succ n)) = Nat.succ n
Tactic:
simp [decode, FinDenumerable.decode_fin]
Proof state after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯ :: decode (n / Fintype.card α)) = Nat.succ n
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯ :: decode (n / Fintype.card α)) = Nat.succ n
Tactic:
simp [encode, inst.decode_fin_is_some (Nat.fin_mod _ _)]
Proof state after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (n / Fintype.card α)) * Fintype.card α +
      Encodable.encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯) =
    n
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ encode (decode (n / Fintype.card α)) * Fintype.card α +
      Encodable.encode (Option.get (Encodable.decode ↑(Nat.fin_mod n ⋯)) ⋯) =
    n
Tactic:
simp [ih, FinDenumerable.decode_fin_eq_option_get]
Proof state after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + Encodable.encode (FinDenumerable.decode_fin (Nat.fin_mod n ⋯)) = n
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + Encodable.encode (FinDenumerable.decode_fin (Nat.fin_mod n ⋯)) = n
Tactic:
rw [<- inst.encode_fin_eq_encode _, inst.decodenk]
Proof state after:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + ↑(Nat.fin_mod n ⋯) = n
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n : ℕ
ih : encode (decode (n / Fintype.card α)) = n / Fintype.card α
⊢ n / Fintype.card α * Fintype.card α + ↑(Nat.fin_mod n ⋯) = n
Tactic:
simp [Nat.fin_mod, Nat.mul_comm, Nat.div_add_mod n inst.card]
Proof state after:
no goals
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n / Fintype.card α) (Nat.succ n)
Tactic:
simp [InvImage]
Proof state after:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ WellFoundedRelation.rel (n / Fintype.card α) (Nat.succ n)
Theorem: Word.decodenk
Proof state before:
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ WellFoundedRelation.rel (n / Fintype.card α) (Nat.succ n)
Tactic:
apply Nat.lt_of_le_of_lt
Proof state after:
case h₁
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ sizeOf (n / Fintype.card α) ≤ ?m

case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ?m < sizeOf (Nat.succ n)

case m
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ℕ
Theorem: Word.decodenk
Proof state before:
case h₁
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ sizeOf (n / Fintype.card α) ≤ ?m

case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ?m < sizeOf (Nat.succ n)

case m
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ ℕ
Tactic:
exact Nat.div_le_self n inst.card
Proof state after:
case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ n < sizeOf (Nat.succ n)
Theorem: Word.decodenk
Proof state before:
case h₂
α : Type u_1
inst : Alphabet α
n✝ : ℕ
a✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y n✝ → encode (decode y) = y
n : ℕ
x✝ : ∀ (y : ℕ), (invImage (fun a => a) instWellFoundedRelation).1 y (Nat.succ n) → encode (decode y) = y
⊢ n < sizeOf (Nat.succ n)
Tactic:
simp
Proof state after:
no goals
Theorem: Word.eps_eq_nil
Proof state before:
α : Type u_1
⊢ ε = []
Tactic:
rfl
Proof state after:
no goals
Theorem: Word.cons_eps
Proof state before:
α✝ : Type u_1
w : α✝
⊢ w :: ε = [w]
Tactic:
simp
Proof state after:
α✝ : Type u_1
w : α✝
⊢ ε = []
Theorem: Word.cons_eps
Proof state before:
α✝ : Type u_1
w : α✝
⊢ ε = []
Tactic:
rfl
Proof state after:
no goals
Theorem: Word.mul_eps
Proof state before:
α✝ : Type u_1
w : Word α✝
⊢ w * ε = w
Tactic:
simp
Proof state after:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1
Theorem: Word.mul_eps
Proof state before:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Word.eps_mul
Proof state before:
α✝ : Type u_1
w : Word α✝
⊢ ε * w = w
Tactic:
simp
Proof state after:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1
Theorem: Word.eps_mul
Proof state before:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Variable.eq
Proof state before:
v₁ v₂ : Variable
⊢ v₁ = v₂ ↔ v₁.index = v₂.index
Tactic:
constructor
Proof state after:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index

case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Theorem: Variable.eq
Proof state before:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index

case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
. intro; congr
Proof state after:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Theorem: Variable.eq
Proof state before:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
. intro h
  cases v₁; cases v₂
  dsimp at h; rw [h]
Proof state after:
no goals
Theorem: Variable.eq
Proof state before:
case mp
v₁ v₂ : Variable
⊢ v₁ = v₂ → v₁.index = v₂.index
Tactic:
intro
Proof state after:
case mp
v₁ v₂ : Variable
a✝ : v₁ = v₂
⊢ v₁.index = v₂.index
Theorem: Variable.eq
Proof state before:
case mp
v₁ v₂ : Variable
a✝ : v₁ = v₂
⊢ v₁.index = v₂.index
Tactic:
congr
Proof state after:
no goals
Theorem: Variable.eq
Proof state before:
case mpr
v₁ v₂ : Variable
⊢ v₁.index = v₂.index → v₁ = v₂
Tactic:
intro h
Proof state after:
case mpr
v₁ v₂ : Variable
h : v₁.index = v₂.index
⊢ v₁ = v₂
Theorem: Variable.eq
Proof state before:
case mpr
v₁ v₂ : Variable
h : v₁.index = v₂.index
⊢ v₁ = v₂
Tactic:
cases v₁
Proof state after:
case mpr.mk
v₂ : Variable
index✝ : ℕ
h : { index := index✝ }.index = v₂.index
⊢ { index := index✝ } = v₂
Theorem: Variable.eq
Proof state before:
case mpr.mk
v₂ : Variable
index✝ : ℕ
h : { index := index✝ }.index = v₂.index
⊢ { index := index✝ } = v₂
Tactic:
cases v₂
Proof state after:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }
Theorem: Variable.eq
Proof state before:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }
Tactic:
dsimp at h
Proof state after:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : index✝¹ = index✝
⊢ { index := index✝¹ } = { index := index✝ }
Theorem: Variable.eq
Proof state before:
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : index✝¹ = index✝
⊢ { index := index✝¹ } = { index := index✝ }
Tactic:
rw [h]
Proof state after:
no goals
Theorem: LoopProgram.len_gt_zero
Proof state before:
⊢ ∀ (p : LoopProgram), len p > 0
Tactic:
intro p
Proof state after:
p : LoopProgram
⊢ len p > 0
Theorem: LoopProgram.len_gt_zero
Proof state before:
p : LoopProgram
⊢ len p > 0
Tactic:
cases p <;> unfold len <;> simp_arith
Proof state after:
no goals
Theorem: LoopProgram.lenOne_complete
Proof state before:
⊢ ∀ (p : LoopProgram), len p = 1 → p ∈ lenOne
Tactic:
intro p h
Proof state after:
p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Theorem: LoopProgram.lenOne_complete
Proof state before:
p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Tactic:
cases p <;> simp [len] at h <;> simp [h, lenOne, Variable.eq]
Proof state after:
case concat
p₁✝ p₂✝ : LoopProgram
h : len p₁✝ = 0 ∧ len p₂✝ = 0
⊢ False

case loop
x✝ : Variable
p✝ : LoopProgram
h : len p✝ = 0 ∧ x✝.index = 0
⊢ False
Theorem: LoopProgram.lenOne_complete
Proof state before:
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ False
Tactic:
case concat p =>
  apply Nat.not_le_of_gt
  apply LoopProgram.len_gt_zero p
  apply Nat.le_of_eq
  exact h.right
Proof state after:
no goals
Theorem: LoopProgram.lenOne_complete
Proof state before:
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ False
Tactic:
case loop p =>
  apply Nat.not_le_of_gt
  apply LoopProgram.len_gt_zero p
  apply Nat.le_of_eq
  exact h.left
Proof state after:
no goals
Theorem: LoopProgram.lenOne_complete
Proof state before:
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ False
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n > ?m

case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n ≤ ?m

case n
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ

case m
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ
Theorem: LoopProgram.lenOne_complete
Proof state before:
case h
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n > ?m

case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n ≤ ?m

case n
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ

case m
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ
Tactic:
apply LoopProgram.len_gt_zero p
Proof state after:
case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p ≤ 0
Theorem: LoopProgram.lenOne_complete
Proof state before:
case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p ≤ 0
Tactic:
apply Nat.le_of_eq
Proof state after:
case a.p
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p = 0
Theorem: LoopProgram.lenOne_complete
Proof state before:
case a.p
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p = 0
Tactic:
exact h.right
Proof state after:
no goals
Theorem: LoopProgram.lenOne_complete
Proof state before:
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ False
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n > ?m

case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n ≤ ?m

case n
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

case m
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ
Theorem: LoopProgram.lenOne_complete
Proof state before:
case h
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n > ?m

case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n ≤ ?m

case n
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

case m
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ
Tactic:
apply LoopProgram.len_gt_zero p
Proof state after:
case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p ≤ 0
Theorem: LoopProgram.lenOne_complete
Proof state before:
case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p ≤ 0
Tactic:
apply Nat.le_of_eq
Proof state after:
case a.p
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p = 0
Theorem: LoopProgram.lenOne_complete
Proof state before:
case a.p
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p = 0
Tactic:
exact h.left
Proof state after:
no goals
Theorem: LoopProgram.ofLen_contains_extendLenOne_image
Proof state before:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ p' ∈
    Finset.fold (fun a b => a ∪ b) ∅ extendLenOne
      ((fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯)
Tactic:
apply Finset.mem_fold_union_iff.mpr
Proof state after:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ ∃
    x ∈
      (fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯,
    p' ∈ extendLenOne x