Theorem: substitutionLemma (Pdl/Substitution.lean)

State before:
σ : Substitution
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
Tactic:
cases φ
State after:
case bottom
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom

case atom_prop
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ (M, w)⊨subst_in_F σ (·a✝) ↔ (subst_in_model σ M, w)⊨·a✝

case neg
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (~a✝) ↔ (subst_in_model σ M, w)⊨(~a✝)

case and
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (a✝¹⋀a✝) ↔ (subst_in_model σ M, w)⊨a✝¹⋀a✝

case box
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ : Program
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈a✝¹⌉a✝) ↔ (subst_in_model σ M, w)⊨⌈a✝¹⌉a✝

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom
Tactic:
case bottom =>
  simp [evaluatePoint, modelCanSemImplyForm]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨subst_in_F σ (·c) ↔ (subst_in_model σ M, w)⊨·c
Tactic:
case atom_prop c =>
  simp [evaluatePoint, modelCanSemImplyForm, evaluate, subst_in_model]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
case neg φ =>
  have IH := substitutionLemma σ φ M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  tauto
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
case and φ1 φ2 =>
  have IH1 := substitutionLemma σ φ1 M w
  have IH2 := substitutionLemma σ φ2 M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  rw [IH1, IH2]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
case box α φ =>
  have IHα := substitutionLemmaRel σ α M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  constructor
  all_goals
    intro hyp v rel
    have IHφ := substitutionLemma σ φ M v
    specialize IHα v
    specialize hyp v
    tauto
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom
Tactic:
simp [evaluatePoint, modelCanSemImplyForm]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨subst_in_F σ (·c) ↔ (subst_in_model σ M, w)⊨·c
Tactic:
simp [evaluatePoint, modelCanSemImplyForm, evaluate, subst_in_model]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
have IH := substitutionLemma σ φ M w
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
⊢ (M, w)⊨subst_in_F σ (~φ) ↔ (subst_in_model σ M, w)⊨(~φ)
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
⊢ ¬evaluate M w (subst_in_F σ φ) ↔ ¬evaluate (subst_in_model σ M) w φ

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
⊢ ¬evaluate M w (subst_in_F σ φ) ↔ ¬evaluate (subst_in_model σ M) w φ
Tactic:
tauto
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
have IH1 := substitutionLemma σ φ1 M w
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
have IH2 := substitutionLemma σ φ2 M w
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (subst_in_F σ φ1) ↔ evaluate (subst_in_model σ M) w φ1
IH2 : evaluate M w (subst_in_F σ φ2) ↔ evaluate (subst_in_model σ M) w φ2
⊢ evaluate M w (subst_in_F σ φ1) ∧ evaluate M w (subst_in_F σ φ2) ↔
    evaluate (subst_in_model σ M) w φ1 ∧ evaluate (subst_in_model σ M) w φ2

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (subst_in_F σ φ1) ↔ evaluate (subst_in_model σ M) w φ1
IH2 : evaluate M w (subst_in_F σ φ2) ↔ evaluate (subst_in_model σ M) w φ2
⊢ evaluate M w (subst_in_F σ φ1) ∧ evaluate M w (subst_in_F σ φ2) ↔
    evaluate (subst_in_model σ M) w φ1 ∧ evaluate (subst_in_model σ M) w φ2
Tactic:
rw [IH1, IH2]
State after:
no goals

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
have IHα := substitutionLemmaRel σ α M w
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
State after:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) ↔
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ

State before:
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) ↔
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
Tactic:
constructor
State after:
case mp
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) →
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ) →
    ∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)

State before:
case mp
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)) →
    ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ) →
    ∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)
Tactic:
all_goals
  intro hyp v rel
  have IHφ := substitutionLemma σ φ M v
  specialize IHα v
  specialize hyp v
  tauto
State after:
no goals

State before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ) →
    ∀ (v : W), relate M (subst_in_P σ α) w v → evaluate M v (subst_in_F σ φ)
Tactic:
intro hyp v rel
State after:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
⊢ evaluate M v (subst_in_F σ φ)

State before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
⊢ evaluate M v (subst_in_F σ φ)
Tactic:
have IHφ := substitutionLemma σ φ M v
State after:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
⊢ evaluate M v (subst_in_F σ φ)

State before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
⊢ evaluate M v (subst_in_F σ φ)
Tactic:
specialize IHα v
State after:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
IHα : relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ evaluate M v (subst_in_F σ φ)

State before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
hyp : ∀ (v : W), relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
IHα : relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ evaluate M v (subst_in_F σ φ)
Tactic:
specialize hyp v
State after:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
IHα : relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
⊢ evaluate M v (subst_in_F σ φ)

State before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
v : W
rel : relate M (subst_in_P σ α) w v
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
IHα : relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
hyp : relate (subst_in_model σ M) α w v → evaluate (subst_in_model σ M) v φ
⊢ evaluate M v (subst_in_F σ φ)
Tactic:
tauto
State after:
no goals