internlm/Lean-Github huggingface dataset:
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic β) <;> cases em (isStar β)
Proof state after:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α : Program
ℓ : TP (∗α)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
cases δ
Proof state after:
case nil
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case cons
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case nil =>
  exfalso; cases γ_in
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case cons =>
  simp_all only [false_or]
  rcases δ_in with ⟨αs, αs_in, def_δ⟩
  subst_eqs
  cases em (γ ∈ αs)
  case inl γ_in =>
    have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr γ_not_in =>
    have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
    subst_eqs
    simp
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
exfalso
Proof state after:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ False
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ False
Tactic:
cases γ_in
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
simp_all only [false_or]
Proof state after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
rcases δ_in with ⟨αs, αs_in, def_δ⟩
Proof state after:
case intro.intro
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
case intro.intro
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
cases em (γ ∈ αs)
Proof state after:
case intro.intro.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
h✝ : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case intro.intro.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
h✝ : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case inl γ_in =>
  have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case inr γ_not_in =>
  have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
  subst_eqs
  simp
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
Proof state after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
Proof state after:
case inl.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inl.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
case inl.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inl.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
(simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
simp_all
Proof state after:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
try linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
Proof state after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
this : γ = (∗α)
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
this : γ = (∗α)
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
subst_eqs
Proof state after:
case refl
α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : (∗α) ∈ head✝ :: tail✝
γ_not_in : (∗α) ∉ αs
⊢ lengthOfProgram (∗α) ≤ 1 + lengthOfProgram α
Theorem: P_goes_down
Proof state before:
case refl
α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : (∗α) ∈ head✝ :: tail✝
γ_not_in : (∗α) ∉ αs
⊢ lengthOfProgram (∗α) ≤ 1 + lengthOfProgram α
Tactic:
simp
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)
Tactic:
rw [← def_δ] at γ_in
Proof state after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in : γ ∈ αs ++ [∗α]
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in : γ ∈ αs ++ [∗α]
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)
Tactic:
simp at γ_in
Proof state after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
γ_in : γ ∈ αs ∨ γ = (∗α)
⊢ γ = (∗α)
Theorem: P_goes_down
Proof state before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
γ_in : γ ∈ αs ∨ γ = (∗α)
⊢ γ = (∗α)
Tactic:
tauto
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
⊢ τ ∈ testsOfProgram (?'τ)
Tactic:
simp [testsOfProgram]
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
simp_all
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
simp_all
Proof state after:
no goals
Theorem: F_goes_down
Proof state before:
φ : Formula
α : Program
ℓ : TP α
⊢ φ ∈ F α ℓ → lengthOfFormula φ < lengthOfProgram α
Tactic:
intro φ_in
Proof state after:
φ : Formula
α : Program
ℓ : TP α
φ_in : φ ∈ F α ℓ
⊢ lengthOfFormula φ < lengthOfProgram α
Theorem: F_goes_down
Proof state before:
φ : Formula
α : Program
ℓ : TP α
φ_in : φ ∈ F α ℓ
⊢ lengthOfFormula φ < lengthOfProgram α
Tactic:
cases α
Proof state after:
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ F (·a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (·a✝)

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : φ ∈ F (a✝¹;'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹;'a✝)

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : φ ∈ F (a✝¹⋓a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹⋓a✝)

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F (∗a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (∗a✝)

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)