internlm/Lean-Github huggingface dataset:
Theorem: substitutionLemma
Proof 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
Proof 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 σ φ)
Theorem: substitutionLemma
Proof 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
Proof state after:
no goals
Theorem: substitutionLemma
Proof 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
Proof 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 σ φ)
Theorem: substitutionLemma
Proof 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
Proof 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 σ φ)
Theorem: substitutionLemma
Proof 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
Proof 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 σ φ)
Theorem: substitutionLemma
Proof 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
Proof 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 σ φ)
Theorem: substitutionLemma
Proof 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
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
α : Program
W : Type
M : KripkeModel W
w v : W
⊢ relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
Tactic:
cases α
Proof state after:
case atom_prog
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : ℕ
⊢ relate M (subst_in_P σ (·a✝)) w v ↔ relate (subst_in_model σ M) (·a✝) w v

case sequence
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (subst_in_P σ (a✝¹;'a✝)) w v ↔ relate (subst_in_model σ M) (a✝¹;'a✝) w v

case union
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (subst_in_P σ (a✝¹⋓a✝)) w v ↔ relate (subst_in_model σ M) (a✝¹⋓a✝) w v

case star
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : Program
⊢ relate M (subst_in_P σ (∗a✝)) w v ↔ relate (subst_in_model σ M) (∗a✝) w v

case test
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : Formula
⊢ relate M (subst_in_P σ (?'a✝)) w v ↔ relate (subst_in_model σ M) (?'a✝) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a : ℕ
⊢ relate M (subst_in_P σ (·a)) w v ↔ relate (subst_in_model σ M) (·a) w v
Tactic:
case atom_prog a =>
  simp [subst_in_model]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Tactic:
case sequence α β =>
  have IHα := substitutionLemmaRel σ α M
  have IHβ := substitutionLemmaRel σ β M
  simp_all only [subst_in_P, relate]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Tactic:
case union α β =>
  have IHα := substitutionLemmaRel σ α M
  have IHβ := substitutionLemmaRel σ β M
  simp_all only [subst_in_P, relate]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
⊢ relate M (subst_in_P σ (∗α)) w v ↔ relate (subst_in_model σ M) (∗α) w v
Tactic:
case star α =>
  have IHα := substitutionLemmaRel σ α M
  simp_all only [subst_in_P, relate]
  constructor
  all_goals
    apply Relation.ReflTransGen.mono
    intro w v
    rw [IHα w v]
    tauto
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
Tactic:
case test φ =>
  have IHφ := substitutionLemma σ φ M v
  simp only [subst_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: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a : ℕ
⊢ relate M (subst_in_P σ (·a)) w v ↔ relate (subst_in_model σ M) (·a) w v
Tactic:
simp [subst_in_model]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Tactic:
have IHα := substitutionLemmaRel σ α M
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Tactic:
have IHβ := substitutionLemmaRel σ β M
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
IHβ : ∀ (w v : W), relate M (subst_in_P σ β) w v ↔ relate (subst_in_model σ M) β w v
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
IHβ : ∀ (w v : W), relate M (subst_in_P σ β) w v ↔ relate (subst_in_model σ M) β w v
⊢ relate M (subst_in_P σ (α;'β)) w v ↔ relate (subst_in_model σ M) (α;'β) w v
Tactic:
simp_all only [subst_in_P, relate]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Tactic:
have IHα := substitutionLemmaRel σ α M
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Tactic:
have IHβ := substitutionLemmaRel σ β M
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
IHβ : ∀ (w v : W), relate M (subst_in_P σ β) w v ↔ relate (subst_in_model σ M) β w v
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α β : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
IHβ : ∀ (w v : W), relate M (subst_in_P σ β) w v ↔ relate (subst_in_model σ M) β w v
⊢ relate M (subst_in_P σ (α⋓β)) w v ↔ relate (subst_in_model σ M) (α⋓β) w v
Tactic:
simp_all only [subst_in_P, relate]
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
⊢ relate M (subst_in_P σ (∗α)) w v ↔ relate (subst_in_model σ M) (∗α) w v
Tactic:
have IHα := substitutionLemmaRel σ α M
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (∗α)) w v ↔ relate (subst_in_model σ M) (∗α) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ relate M (subst_in_P σ (∗α)) w v ↔ relate (subst_in_model σ M) (∗α) w v
Tactic:
simp_all only [subst_in_P, relate]
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate M (subst_in_P σ α)) w v ↔ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate M (subst_in_P σ α)) w v ↔ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v
Tactic:
constructor
Proof state after:
case mp
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate M (subst_in_P σ α)) w v → Relation.ReflTransGen (relate (subst_in_model σ M) α) w v

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v → Relation.ReflTransGen (relate M (subst_in_P σ α)) w v
Theorem: substitutionLemmaRel
Proof state before:
case mp
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate M (subst_in_P σ α)) w v → Relation.ReflTransGen (relate (subst_in_model σ M) α) w v

case mpr
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v → Relation.ReflTransGen (relate M (subst_in_P σ α)) w v
Tactic:
all_goals
  apply Relation.ReflTransGen.mono
  intro w v
  rw [IHα w v]
  tauto
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
case mpr
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ Relation.ReflTransGen (relate (subst_in_model σ M) α) w v → Relation.ReflTransGen (relate M (subst_in_P σ α)) w v
Tactic:
apply Relation.ReflTransGen.mono
Proof state after:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ ∀ (a b : W), relate (subst_in_model σ M) α a b → relate M (subst_in_P σ α) a b
Theorem: substitutionLemmaRel
Proof state before:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w v : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ ∀ (a b : W), relate (subst_in_model σ M) α a b → relate M (subst_in_P σ α) a b
Tactic:
intro w v
Proof state after:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
w v : W
⊢ relate (subst_in_model σ M) α w v → relate M (subst_in_P σ α) w v
Theorem: substitutionLemmaRel
Proof state before:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
w v : W
⊢ relate (subst_in_model σ M) α w v → relate M (subst_in_P σ α) w v
Tactic:
rw [IHα w v]
Proof state after:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
w v : W
⊢ relate (subst_in_model σ M) α w v → relate (subst_in_model σ M) α w v
Theorem: substitutionLemmaRel
Proof state before:
case mpr.a
σ : Substitution
W : Type
M : KripkeModel W
w✝ v✝ : W
α : Program
IHα : ∀ (w v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
w v : W
⊢ relate (subst_in_model σ M) α w v → relate (subst_in_model σ M) α w v
Tactic:
tauto
Proof state after:
no goals
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
Tactic:
have IHφ := substitutionLemma σ φ M v
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : (M, v)⊨subst_in_F σ φ ↔ (subst_in_model σ M, v)⊨φ
⊢ relate M (subst_in_P σ (?'φ)) w v ↔ relate (subst_in_model σ M) (?'φ) w v
Tactic:
simp only [subst_in_P, relate, and_congr_right_iff, evaluatePoint, modelCanSemImplyForm] at *
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
⊢ w = v → (evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ)
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
⊢ w = v → (evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ)
Tactic:
intro w_is_v
Proof state after:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
w_is_v : w = v
⊢ evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
Theorem: substitutionLemmaRel
Proof state before:
σ : Substitution
W : Type
M : KripkeModel W
w v : W
φ : Formula
IHφ : evaluate M v (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) v φ
w_is_v : w = v
⊢ evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
Tactic:
subst w_is_v
Proof 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 φ
Theorem: substitutionLemmaRel
Proof 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:
exact IHφ
Proof state after:
no goals
Theorem: truthLemma
Proof state before:
Worlds : Set (Finset Formula)
MG : ModelGraph Worlds
⊢ ∀ (X : ↑Worlds), ∀ P ∈ ↑X, Evaluate (↑MG, X) P
Tactic:
intro X P
Proof state after:
Worlds : Set (Finset Formula)
MG : ModelGraph Worlds
X : ↑Worlds
P : Formula
⊢ P ∈ ↑X → Evaluate (↑MG, X) P
Theorem: truthLemma
Proof state before:
Worlds : Set (Finset Formula)
MG : ModelGraph Worlds
X : ↑Worlds
P : Formula
⊢ P ∈ ↑X → Evaluate (↑MG, X) P
Tactic:
cases' MG with M M_prop
Proof state after:
case mk
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
M_prop :
  (∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X) ∧
    (fun M => ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp) M ∧
      (fun M => ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y) M ∧
        (fun M => ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y) M
⊢ P ∈ ↑X → Evaluate (↑⟨M, M_prop⟩, X) P
Theorem: truthLemma
Proof state before:
case mk
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
M_prop :
  (∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X) ∧
    (fun M => ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp) M ∧
      (fun M => ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y) M ∧
        (fun M => ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y) M
⊢ P ∈ ↑X → Evaluate (↑⟨M, M_prop⟩, X) P
Tactic:
rcases M_prop with ⟨i, ii, iii, iv⟩
Proof state after:
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P
Theorem: truthLemma
Proof state before:
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P
Tactic:
let plus P (X : Worlds) := P ∈ X.val → Evaluate (M, X) P
Proof state after:
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P
Theorem: truthLemma
Proof state before:
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P
Tactic:
let minus P (X : Worlds) := ~P ∈ X.val → ¬Evaluate (M, X) P
Proof state after:
case mk.intro.intro.intro
Worlds : Set (Finset Formula)
X : ↑Worlds
P : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), Saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : Char), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
ii : ∀ (X : { x // x ∈ Worlds }) (pp : Char), (·pp) ∈ ↑X ↔ M.val X pp
iii : ∀ (X Y : { x // x ∈ Worlds }) (P : Formula), M.Rel X Y → □P ∈ ↑X → P ∈ ↑Y
iv : ∀ (X : { x // x ∈ Worlds }) (P : Formula), ~(□P) ∈ ↑X → ∃ Y, M.Rel X Y ∧ ~P ∈ ↑Y
plus : Formula → ↑Worlds → Prop := fun P X => P ∈ ↑X → Evaluate (M, X) P
minus : Formula → ↑Worlds → Prop := fun P X => ~P ∈ ↑X → ¬Evaluate (M, X) P
⊢ P ∈ ↑X → Evaluate (↑⟨M, ⋯⟩, X) P