internlm/Lean-Github huggingface dataset:
Theorem: repl_in_list_non_occ_eq
Proof 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
Proof 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
Theorem: repl_in_list_non_occ_eq
Proof 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
Proof state after:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F
Theorem: repl_in_list_non_occ_eq
Proof state before:
case right
x : ℕ
ρ φ : Formula
F : List Formula
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc F
Tactic:
simp [voc,vocabOfProgram,vocabOfListFormula] at *
Proof 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
Theorem: repl_in_list_non_occ_eq
Proof 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
Proof 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
Theorem: repl_in_list_non_occ_eq
Proof 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
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, w)⊨φ
Tactic:
cases φ
Proof state after:
case bottom
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ Formula.bottom ↔ (repl_in_model x ψ M, w)⊨Formula.bottom

case atom_prop
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·a✝) ↔ (repl_in_model x ψ M, w)⊨·a✝

case neg
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (~a✝) ↔ (repl_in_model x ψ M, w)⊨(~a✝)

case and
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (a✝¹⋀a✝) ↔ (repl_in_model x ψ M, w)⊨a✝¹⋀a✝

case box
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ : Program
a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (⌈a✝¹⌉a✝) ↔ (repl_in_model x ψ M, w)⊨⌈a✝¹⌉a✝
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ Formula.bottom ↔ (repl_in_model x ψ M, w)⊨Formula.bottom
Tactic:
case bottom =>
  simp [evaluatePoint, modelCanSemImplyForm]
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·c) ↔ (repl_in_model x ψ M, w)⊨·c
Tactic:
case atom_prop c =>
  simp [evaluatePoint, modelCanSemImplyForm, evaluate, repl_in_model]
  aesop
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨repl_in_F x ψ (~φ) ↔ (repl_in_model x ψ M, w)⊨(~φ)
Tactic:
case neg φ =>
  have IH := repl_in_model_sat_iff x ψ φ M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  tauto
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Tactic:
case and φ1 φ2 =>
  have IH1 := repl_in_model_sat_iff x ψ φ1 M w
  have IH2 := repl_in_model_sat_iff x ψ φ2 M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  rw [IH1, IH2]
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨repl_in_F x ψ (⌈α⌉φ) ↔ (repl_in_model x ψ M, w)⊨⌈α⌉φ
Tactic:
case box α φ =>
  have IHα := repl_in_model_rel_iff x ψ α M w
  simp [evaluatePoint, modelCanSemImplyForm] at *
  constructor
  all_goals
    intro hyp v rel
    have IHφ := repl_in_model_sat_iff x ψ φ M v
    specialize IHα v
    specialize hyp v
    tauto
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ Formula.bottom ↔ (repl_in_model x ψ M, w)⊨Formula.bottom
Tactic:
simp [evaluatePoint, modelCanSemImplyForm]
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·c) ↔ (repl_in_model x ψ M, w)⊨·c
Tactic:
simp [evaluatePoint, modelCanSemImplyForm, evaluate, repl_in_model]
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ evaluate M w (if c = x then ψ else ·c) ↔ if c = x then evaluate { val := M.val, Rel := M.Rel } w ψ else M.val w c
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
c : ℕ
⊢ evaluate M w (if c = x then ψ else ·c) ↔ if c = x then evaluate { val := M.val, Rel := M.Rel } w ψ else M.val w c
Tactic:
aesop
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
⊢ (M, w)⊨repl_in_F x ψ (~φ) ↔ (repl_in_model x ψ M, w)⊨(~φ)
Tactic:
have IH := repl_in_model_sat_iff x ψ φ M w
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, w)⊨φ
⊢ (M, w)⊨repl_in_F x ψ (~φ) ↔ (repl_in_model x ψ M, w)⊨(~φ)
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : (M, w)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, w)⊨φ
⊢ (M, w)⊨repl_in_F x ψ (~φ) ↔ (repl_in_model x ψ M, w)⊨(~φ)
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof 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 φ
Theorem: repl_in_model_sat_iff
Proof 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:
tauto
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Tactic:
have IH1 := repl_in_model_sat_iff x ψ φ1 M w
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Tactic:
have IH2 := repl_in_model_sat_iff x ψ φ2 M w
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
IH2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
IH2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
IH2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ∧ evaluate M w (repl_in_F x ψ φ2) ↔
    evaluate (repl_in_model x ψ M) w φ1 ∧ evaluate (repl_in_model x ψ M) w φ2
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : evaluate M w (repl_in_F x ψ φ1) ↔ evaluate (repl_in_model x ψ M) w φ1
IH2 : evaluate M w (repl_in_F x ψ φ2) ↔ evaluate (repl_in_model x ψ M) w φ2
⊢ evaluate M w (repl_in_F x ψ φ1) ∧ evaluate M w (repl_in_F x ψ φ2) ↔
    evaluate (repl_in_model x ψ M) w φ1 ∧ evaluate (repl_in_model x ψ M) w φ2
Tactic:
rw [IH1, IH2]
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨repl_in_F x ψ (⌈α⌉φ) ↔ (repl_in_model x ψ M, w)⊨⌈α⌉φ
Tactic:
have IHα := repl_in_model_rel_iff x ψ α M w
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (M, w)⊨repl_in_F x ψ (⌈α⌉φ) ↔ (repl_in_model x ψ M, w)⊨⌈α⌉φ
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (M, w)⊨repl_in_F x ψ (⌈α⌉φ) ↔ (repl_in_model x ψ M, w)⊨⌈α⌉φ
Tactic:
simp [evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) ↔
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
Theorem: repl_in_model_sat_iff
Proof state before:
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) ↔
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
Tactic:
constructor
Proof state after:
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) →
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ) →
    ∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)
Theorem: repl_in_model_sat_iff
Proof state before:
case mp
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)) →
    ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ

case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ) →
    ∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)
Tactic:
all_goals
  intro hyp v rel
  have IHφ := repl_in_model_sat_iff x ψ φ M v
  specialize IHα v
  specialize hyp v
  tauto
Proof state after:
no goals
Theorem: repl_in_model_sat_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ (∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ) →
    ∀ (v : W), relate M (repl_in_P x ψ α) w v → evaluate M v (repl_in_F x ψ φ)
Tactic:
intro hyp v rel
Proof state after:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
⊢ evaluate M v (repl_in_F x ψ φ)
Theorem: repl_in_model_sat_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
⊢ evaluate M v (repl_in_F x ψ φ)
Tactic:
have IHφ := repl_in_model_sat_iff x ψ φ M v
Proof state after:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ evaluate M v (repl_in_F x ψ φ)
Theorem: repl_in_model_sat_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
⊢ evaluate M v (repl_in_F x ψ φ)
Tactic:
specialize IHα v
Proof state after:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
IHα : relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ evaluate M v (repl_in_F x ψ φ)
Theorem: repl_in_model_sat_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
hyp : ∀ (v : W), relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
IHα : relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
⊢ evaluate M v (repl_in_F x ψ φ)
Tactic:
specialize hyp v
Proof state after:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
IHα : relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
⊢ evaluate M v (repl_in_F x ψ φ)
Theorem: repl_in_model_sat_iff
Proof state before:
case mpr
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
v : W
rel : relate M (repl_in_P x ψ α) w v
IHφ : (M, v)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, v)⊨φ
IHα : relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
hyp : relate (repl_in_model x ψ M) α w v → evaluate (repl_in_model x ψ M) v φ
⊢ evaluate M v (repl_in_F x ψ φ)
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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 α
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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φ
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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]
Proof state after:
no goals
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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]
Proof 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
Theorem: repl_in_model_rel_iff
Proof 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
Proof 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