Theorem: F_goes_down (Pdl/Unfold.lean)

State before:
φ : Formula
α : Program
ℓ : TP α
⊢ φ ∈ F α ℓ → lengthOfFormula φ < lengthOfProgram α
Tactic:
intro φ_in
State after:
φ : Formula
α : Program
ℓ : TP α
φ_in : φ ∈ F α ℓ
⊢ lengthOfFormula φ < lengthOfProgram α

State before:
φ : Formula
α : Program
ℓ : TP α
φ_in : φ ∈ F α ℓ
⊢ lengthOfFormula φ < lengthOfProgram α
Tactic:
cases α
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✝)

State before:
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✝)
Tactic:
all_goals
  simp only [F, List.mem_union_iff, lengthOfProgram] at *
State after:
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F a✝ fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝

State before:
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1
Tactic:
case atom_prog =>
  simp only [List.empty_eq, List.not_mem_nil] at φ_in
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case sequence α β =>
  cases φ_in
  case inl φ_in_Fα =>
    have IHα := F_goes_down φ_in_Fα
    linarith
  case inr φ_in_Fβ =>
    have IHβ := F_goes_down φ_in_Fβ
    linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case union α β =>
  cases φ_in
  case inl φ_in_Fα =>
    have IHα := F_goes_down φ_in_Fα
    linarith
  case inr φ_in_Fβ =>
    have IHβ := F_goes_down φ_in_Fβ
    linarith
State after:
no goals

State before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
case star α =>
  have IHα := F_goes_down φ_in
  linarith
State after:
no goals

State before:
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)
Tactic:
simp only [F, List.mem_union_iff, lengthOfProgram] at *
State after:
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝

State before:
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1
Tactic:
simp only [List.empty_eq, List.not_mem_nil] at φ_in
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases φ_in
State after:
case inl
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl φ_in_Fα =>
  have IHα := F_goes_down φ_in_Fα
  linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr φ_in_Fβ =>
  have IHβ := F_goes_down φ_in_Fβ
  linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHα := F_goes_down φ_in_Fα
State after:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHβ := F_goes_down φ_in_Fβ
State after:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases φ_in
State after:
case inl
φ : Formula
α β : Program
ℓ : TP (α⋓β)
h✝ : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
φ : Formula
α β : Program
ℓ : TP (α⋓β)
h✝ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl φ_in_Fα =>
  have IHα := F_goes_down φ_in_Fα
  linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr φ_in_Fβ =>
  have IHβ := F_goes_down φ_in_Fβ
  linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHα := F_goes_down φ_in_Fα
State after:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fα : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IHβ := F_goes_down φ_in_Fβ
State after:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
have IHα := F_goes_down φ_in
State after:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α

State before:
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
Tactic:
linarith
State after:
no goals

State before:
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
State after:
case inl
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ

case inr
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ

State before:
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
⊢ τ ∈ testsOfProgram (?'τ)
Tactic:
simp [testsOfProgram]
State after:
no goals

State before:
case inl
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
simp_all
State after:
no goals

State before:
case inr
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
Tactic:
simp_all
State after:
no goals