Theorem: repl_in_list_non_occ_eq (Pdl/Substitution.lean)

State before:
x : ℕ
ρ : Formula
F : List Formula
⊢ x ∉ voc F → List.map (repl_in_F x ρ) F = F
Tactic:
intro nonOcc
State after:
x : ℕ
ρ : Formula
F : List Formula
nonOcc : x ∉ voc F
⊢ List.map (repl_in_F x ρ) F = F

State before:
x : ℕ
ρ : Formula
F : List Formula
nonOcc : x ∉ voc F
⊢ List.map (repl_in_F x ρ) F = F
Tactic:
induction F
State after:
case nil
x : ℕ
ρ : Formula
nonOcc : x ∉ voc []
⊢ List.map (repl_in_F x ρ) [] = []

case cons
x : ℕ
ρ head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∉ voc tail✝ → List.map (repl_in_F x ρ) tail✝ = tail✝
nonOcc : x ∉ voc (head✝ :: tail✝)
⊢ List.map (repl_in_F x ρ) (head✝ :: tail✝) = head✝ :: tail✝

State before:
case nil
x : ℕ
ρ : Formula
nonOcc : x ∉ voc []
⊢ List.map (repl_in_F x ρ) [] = []
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) (φ :: F) = φ :: F
Tactic:
simp only [List.map_cons, List.cons.injEq]
State after:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ ∧ List.map (repl_in_F x ρ) F = F

State before:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ ∧ List.map (repl_in_F x ρ) F = F
Tactic:
constructor
State after:
case left
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ

case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) F = F

State before:
case left
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ
Tactic:
apply repl_in_F_non_occ_eq
State after:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc φ

State before:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc φ
Tactic:
simp [voc,vocabOfProgram,vocabOfListFormula] at *
State after:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula φ

State before:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula φ
Tactic:
exact nonOcc.left
State after:
no goals

State before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) F = F
Tactic:
apply IH
State after:
case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F

State before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F
Tactic:
clear IH
State after:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F

State before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F
Tactic:
simp [voc,vocabOfProgram,vocabOfListFormula] at *
State after:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1

State before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
Tactic:
intro d d_in
State after:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
d : Formula
d_in : d ∈ F
⊢ x ∉ vocabOfFormula d

State before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
d : Formula
d_in : d ∈ F
⊢ x ∉ vocabOfFormula d
Tactic:
simp_all
State after:
no goals