Theorem: repl_in_model_rel_iff (Pdl/Substitution.lean)

State before:
x : ℕ
ψ : Formula
α : Program
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
Tactic:
cases α
State after:
case atom_prog
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : ℕ
⊢ relate M (repl_in_P x ψ (·a✝)) w v ↔ relate (repl_in_model x ψ M) (·a✝) w v

case sequence
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (repl_in_P x ψ (a✝¹;'a✝)) w v ↔ relate (repl_in_model x ψ M) (a✝¹;'a✝) w v

case union
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (repl_in_P x ψ (a✝¹⋓a✝)) w v ↔ relate (repl_in_model x ψ M) (a✝¹⋓a✝) w v

case star
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : Program
⊢ relate M (repl_in_P x ψ (∗a✝)) w v ↔ relate (repl_in_model x ψ M) (∗a✝) w v

case test
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : Formula
⊢ relate M (repl_in_P x ψ (?'a✝)) w v ↔ relate (repl_in_model x ψ M) (?'a✝) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a : ℕ
⊢ relate M (repl_in_P x ψ (·a)) w v ↔ relate (repl_in_model x ψ M) (·a) w v
Tactic:
case atom_prog a =>
  simp [repl_in_model]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v
Tactic:
case sequence α β =>
  have IHα := repl_in_model_rel_iff x ψ α M
  have IHβ := repl_in_model_rel_iff x ψ β M
  simp_all only [repl_in_P, relate]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v
Tactic:
case union α β =>
  have IHα := repl_in_model_rel_iff x ψ α M
  have IHβ := repl_in_model_rel_iff x ψ β M
  simp_all only [repl_in_P, relate]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
⊢ relate M (repl_in_P x ψ (∗α)) w v ↔ relate (repl_in_model x ψ M) (∗α) w v
Tactic:
case star α =>
  have IHα := repl_in_model_rel_iff x ψ α M
  simp_all only [repl_in_P, relate]
  constructor
  all_goals
    apply Relation.ReflTransGen.mono
    intro w v
    rw [IHα w v]
    tauto
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Tactic:
case test φ =>
  have IHφ := repl_in_model_sat_iff x ψ φ M v
  simp only [repl_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
  intro w_is_v
  subst w_is_v
  exact IHφ
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a : ℕ
⊢ relate M (repl_in_P x ψ (·a)) w v ↔ relate (repl_in_model x ψ M) (·a) w v
Tactic:
simp [repl_in_model]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v
Tactic:
have IHα := repl_in_model_rel_iff x ψ α M
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v
Tactic:
have IHβ := repl_in_model_rel_iff x ψ β M
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
IHβ : ∀ (w v : W), relate M (repl_in_P x ψ β) w v ↔ relate (repl_in_model x ψ M) β w v
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
IHβ : ∀ (w v : W), relate M (repl_in_P x ψ β) w v ↔ relate (repl_in_model x ψ M) β w v
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v
Tactic:
simp_all only [repl_in_P, relate]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v
Tactic:
have IHα := repl_in_model_rel_iff x ψ α M
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v
Tactic:
have IHβ := repl_in_model_rel_iff x ψ β M
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
IHβ : ∀ (w v : W), relate M (repl_in_P x ψ β) w v ↔ relate (repl_in_model x ψ M) β w v
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
IHβ : ∀ (w v : W), relate M (repl_in_P x ψ β) w v ↔ relate (repl_in_model x ψ M) β w v
⊢ relate M (repl_in_P x ψ (α⋓β)) w v ↔ relate (repl_in_model x ψ M) (α⋓β) w v
Tactic:
simp_all only [repl_in_P, relate]
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
⊢ relate M (repl_in_P x ψ (∗α)) w v ↔ relate (repl_in_model x ψ M) (∗α) w v
Tactic:
have IHα := repl_in_model_rel_iff x ψ α M
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (∗α)) w v ↔ relate (repl_in_model x ψ M) (∗α) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ relate M (repl_in_P x ψ (∗α)) w v ↔ relate (repl_in_model x ψ M) (∗α) w v
Tactic:
simp_all only [repl_in_P, relate]
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v ↔ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v ↔ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v
Tactic:
constructor
State after:
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v → Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v

State before:
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v → Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v
Tactic:
all_goals
  apply Relation.ReflTransGen.mono
  intro w v
  rw [IHα w v]
  tauto
State after:
no goals

State before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v → Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v
Tactic:
apply Relation.ReflTransGen.mono
State after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ ∀ (a b : W), relate (repl_in_model x ψ M) α a b → relate M (repl_in_P x ψ α) a b

State before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ ∀ (a b : W), relate (repl_in_model x ψ M) α a b → relate M (repl_in_P x ψ α) a b
Tactic:
intro w v
State after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate M (repl_in_P x ψ α) w v

State before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate M (repl_in_P x ψ α) w v
Tactic:
rw [IHα w v]
State after:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate (repl_in_model x ψ M) α w v

State before:
case mpr.a
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
w v : W
⊢ relate (repl_in_model x ψ M) α w v → relate (repl_in_model x ψ M) α w v
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Tactic:
have IHφ := repl_in_model_sat_iff x ψ φ M v
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ relate M (repl_in_P x ψ (?'φ)) w v ↔ relate (repl_in_model x ψ M) (?'φ) w v
Tactic:
simp only [repl_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
⊢ w = v → (evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ)

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
⊢ w = v → (evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ)
Tactic:
intro w_is_v
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
w_is_v : w = v
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) v φ
w_is_v : w = v
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Tactic:
subst w_is_v
State after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IHφ : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ

State before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IHφ : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
Tactic:
exact IHφ
State after:
no goals